Let’s Use An Automated Theorem Prover To Verify Video Games; I Swear This Is More Fun Than It Sounds

Jon Manning demonstrates how to use the Z3 automated theorem prover to model RPG mechanics and automatically detect bugs like softlocks.

Jon Manning lca2021.linux.org.au/schedule/presentation/54/ 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! linux.conf.au is a conference about the Linux operating system, and all aspects of the thriving ecosystem of Free and Open Source Software that has grown up around it. Run since 1999, in a different Australian or New Zealand city each year, by a team of local volunteers, LCA invites more than 500 people to learn from the people who shape the future of Open Source. For more information on the conference see linux.conf.au/ Produced by Next Day Video Australia: nextdayvideo.com.au #linux.conf.au #linux #foss #opensource Mon Jan 25 13:30:00 2021 at Rusty R. Hall