Testing Super Mario Using a Behavior Model Autonomously – Finding Real Bugs

A behavior model combined with autonomous testing was used to find real bugs in a Super Mario game implementation. The approach uses bidirectional testing where the model validates every frame and discrepancies reveal bugs in either the game or the model. Several engine bugs were uncovered, including a teleport bug caused by overlapping collision boxes in Level 4.