Let’s Use An Automated Theorem Prover To Verify Video Games; I Promise This Is Applicable To You
Clarendon Room E | Tue 14 Mar 11:40 a.m.–12:25 p.m.
Presented by
-
Jon Manning is the co-founder of Secret Lab, an independent game development studio working on Leonardo’s Moon Ship, the hugely popular narrative tool Yarn Spinner, and for their work on the BAFTA- and IGF-winning Night in the Woods. Jon is also the co-author of a number of books on Unity, Swift, and machine learning, and holds a PhD about jerks on the internet.
-
Paris Buttfield-Addison
@parisba
https://paris.id.au
Dr Paris Buttfield-Addison is co-founder of Secret Lab (https://secretlab.games), a game development studio based in beautiful Hobart, Tasmania, Australia. Secret Lab builds games and game development tools, including the BAFTA- and IGF-winning Night in the Woods, the wildly popular Yarn Spinner (https://yarnspinner.dev), an open source narrative game development framework, and the award-winning ABC Play School and Qantas Joey Playbox iPad games. Paris formerly worked as a software engineer, and later product manager for Meebo, which was acquired by Google in 2012. He has a degree in medieval history, a PhD in Computing, and writes technical books (around 30 so far) on machine learning, programming, and game development for O’Reilly Media. He can be found on the Fediverse at http://cloudisland.nz/@parisba and online at http://paris.id.au
Paris Buttfield-Addison
@parisba
https://paris.id.au
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 a popular computer role-playing game, 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 effects. By the end of this talk, you’ll be ready to apply formal logic to complex interlocking systems, how to create an abstract model of your systems, and how to find and fix bugs that you didn’t know you had.
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 a popular computer role-playing game, 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 effects. By the end of this talk, you’ll be ready to apply formal logic to complex interlocking systems, how to create an abstract model of your systems, and how to find and fix bugs that you didn’t know you had.