Let’s Use An Automated Theorem Prover To Verify Video Games; I Swear This Is More Fun Than It Sounds
Rusty R. Hall | Mon 25 Jan 1:30 p.m.–2:15 p.m.
Presented by
-
Jon Manning
@desplesda
http://desplesda.net
Jon Manning is the cofounder of independent game development studio Secret Lab. He's working on the critically acclaimed award-winning adventure game Night in the Woods, which includes his interactive dialogue system Yarn Spinner. He's written a whole bunch of books for O'Reilly about iOS development and game development. Jon holds a PhD about jerks on the internet.
Jon Manning
@desplesda
http://desplesda.net
Abstract
Automated theorem provers allow you to describe a set of logical assertions and constraints, and then discover inconsistencies and impossibilities in that system. This makes them incredibly useful for testing large, complicated and intricately interlocking systems. Sounds like a video game.
In this talk, we’ll use Z3, an open source theorem prover from Microsoft Research, to describe and diagnose problems in an RPG, and automatically discover problems like softlocks and impossible situations. We’ll unpick some of the impressively dense jargon that often surrounds this field, and learn how to apply this theory to practical effect. By the end of this talk, you’ll be ready to apply formal logic to game systems, how to create an abstract model of a complex game, and how to find and fix bugs that you didn’t know you had. You'll also be ready to apply these learnings to non-game systems, too!
Automated theorem provers allow you to describe a set of logical assertions and constraints, and then discover inconsistencies and impossibilities in that system. This makes them incredibly useful for testing large, complicated and intricately interlocking systems. Sounds like a video game. In this talk, we’ll use Z3, an open source theorem prover from Microsoft Research, to describe and diagnose problems in an RPG, and automatically discover problems like softlocks and impossible situations. We’ll unpick some of the impressively dense jargon that often surrounds this field, and learn how to apply this theory to practical effect. By the end of this talk, you’ll be ready to apply formal logic to game systems, how to create an abstract model of a complex game, and how to find and fix bugs that you didn’t know you had. You'll also be ready to apply these learnings to non-game systems, too!