Close

We might also be extending this project to use the COQ theorem prover as well.

A project log for DOOM SOURCE CODE - SOFTWARE ARCHAEOLOGY- ISABELLE

Doom Video Game Source code being analyzed by the Isabelle HOL automated theorem prover. This is done to help develop an on-line course on

david-blubaughDavid Blubaugh 05/17/2020 at 04:190 Comments

We are in the process of evaluating the COQ theorem prover to determine if the Verified Software Toolchain from the COQ theorem prover can be extended to C programs such as DOOM by Id Software.   

Discussions