Project Abstract

MotivationThe need to build faith and trust in computerized versions of games, especially ones with simple rules like tic-tac-toe, is what inspired this initiative. The game’s right behavior and invulnerability to manipulation or cheating may be guaranteed to participants by thorough modeling and formal proofs of the game’s attributes. Students may learn about formal verification methods, discrete mathematics, and theoretical computer science via this project.BackgroundTic-Tac-Toe is a classic board game where players use symbols to mark specific spaces on a 3×3 grid. The game, also known as “Noughts and Crosses” or “Three in a Row,” has become an industry worth billions of dollars since the 1970s. The game, which originated from ancient Egyptians, has evolved to suit various surfaces and has become popular worldwide. Players must decide who will go first and use an X to mark their moves.Research question?�� How can the VDM and Overture modeling tool be effectively utilized to construct a formal model of tic-tac-toe??�� What techniques can be employed to verify the correctness and consistency of the formal model of tic-tac-toe?Main Approach to the workThis project aims to create a formal model for a tic-tac-toe computer game, ensuring honesty and fairness. The game involves players marking squares on a three-square grid, with winning combinations or grid filling determining the game’s end. Tools like Isabelle/HOL and VDM-SL will be used to document rules, player interactions, and winning requirements. The model will undergo rigorous examination and validation using formal verification techniques, and Isabelle/HOL will provide formal proofs for crucial aspects.Main Findings?�� Develop a formal model of tic-tac-toe using VDM and Overture modeling tool.?�� Identify and define important fairness constraints and properties of the game.?�� Provide proofs for these properties using Isabelle, a proof assistant, to demonstrate the game’s fairness and integrity.

Keywords: Game Theory, Logic, Proofs

 Conference Details

Session: Presentation Stream 16 at Presentation Slot 2

Location: GH001 at Wednesday 8th 09:00 – 12:30

Markers: Arno Pauly, Alec Critten (GTA)

Course: MSc Advanced Software Technology, Masters PG

Future Plans: I’m looking for an industry placement