DOOM SOURCE CODE - SOFTWARE ARCHAEOLOGY- ISABELLE

Description

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 Software archaeology and Analysis on legacy software applications like DOOM . This can also be used to understand and debug legacy software that has not been documented or programmed for a long time.......

Details

USE OF ISABELLE HOL FOR DOOM VERIFICATION AND VALIDATION

IN OTHER WORDS...... IF YOU WRITE SOFTWARE FOR A GAME LIKE DOOM... WRITE AND

ANALYZE THE SOURCE CODE AS IF YOUR VERY LIFE DEPENDED ON IT .......

HENCE THE USE OF SAFETY CRITICAL SOFTWARE DEVELOPMENT METHODS LEARNED FROM CREATING SOFTWARE FOR JET ENGINE FADEC CONTROLLERS AND THEN APPLY IT FOR VIDEO GAMES.....

WHY THE HELL NOT ????

LETS SEE IF WE CAN FIND EXTREMELY SUBTLE SOFTWARE FLAWS WITHIN THE DOOM SOURCE CODE THAT HAVE ELUDED DETECTION OVER THE LAST 27 YEARS... SINCE 1993.....

IN A FINAL SENSE OF GLORY TO HAVE MORE CARNAL KNOWLEDGE FOR THE SOURCE CODE THAN WHAT WAS THOUGHT POSSIBLE.....

Compile with all warnings enabled, and use one or more source code analyzers.

Files

tutorial.pdf

More Isabelle HOL material of importance.

Adobe Portable Document Format - 1.01 MB - 05/21/2020 at 04:15

Preview

a56309601974c4ba5285042321ade45c9899.pdf

USE of machine learning within Iaabelle HOL.

Adobe Portable Document Format - 545.26 kB - 05/21/2020 at 04:15

Preview

A_Learning-Based_Fact_Selector_for_IsabelleHOL.pdf

Additional use of machine learning for ISabelle HOL .

Adobe Portable Document Format - 384.97 kB - 05/21/2020 at 04:15

Preview

formal_game.pdf

A Paper that talks about the use of the Event-B method ( A Different Theorem Prover ) for develop formal methods for video games.... Lessons learned here can be applied with the Isabelle HOL theorem prover......

Adobe Portable Document Format - 287.15 kB - 05/20/2020 at 10:34

Preview

chocolate-doom-3.0.0-win32.zip

Based on SDL it will compile with brio on pretty much any platform, it's the port I hacked to generate these videos. I will utilize both the Isabelle HOL and COQ theorem provers to verify and validate the windows port of doom FIRST. If there are any objections, please respond in the discussions forum......

x-zip-compressed - 2.65 MB - 05/18/2020 at 21:21

Download

Project Logs

Collapse

This Project is Dedicated to all of the Masters of DOOM and ID Software
David Blubaugh • 05/18/2020 at 20:27 • 0 comments

This Project is Dedicated to all of the ORIGINAL Masters of DOOM and ID Software....
Excellent Youtube Video by John Romero on software failures caused by Number Theory within Quake's Development back in 1996.
David Blubaugh • 05/17/2020 at 05:27 • 1 comment

TO ALL WITH ANY INTEREST
PLEASE LOOK TO MINUTE 27:49 out of the 50 minutes and 5 seconds. during the QUICK STORY told by John Romero himself.
This shows a definite need for formal verification and validation for video games development.
The hyperlink is as follows:
https://www.youtube.com/watch?v=KFziBfvAFnM
We might also be extending this project to use the COQ theorem prover as well.
David Blubaugh • 05/17/2020 at 04:19 • 0 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.
"Correctness proofs of distributed systems with Isabelle" by Martin Kleppmann
David Blubaugh • 05/15/2020 at 02:32 • 0 comments

This is an excellent youtube video by Martin Kleppmann.
https://www.youtube.com/watch?v=7w4KC6i9Yac
I will be using this to verify and validate that the source code within DOOM that handles the internet deathmatching capabilities will be verified and validated...
I have added this youtube link for further reference.....
Excellent Youtube video on DOOM Monster AI
David Blubaugh • 05/11/2020 at 08:43 • 0 comments

Excellent Youtube video on DOOM Monster AI
Please watch ............
https://www.youtube.com/watch?v=f3O9P9x1eCE
Excellent Youtube video on DOOM Monster AI
David Blubaugh • 05/11/2020 at 08:40 • 0 comments

Excellent Youtube video on DOOM Monster AI
Please watch ............
https://www.youtube.com/watch?v=f3O9P9x1eCE
Uploaded Masters thesis file that will be used as a corner stone to refactoring the DOOM source code.
David Blubaugh • 05/08/2020 at 05:24 • 0 comments

Uploaded Masters thesis file that will be used as a corner stone to refactoring the DOOM source code. I am currently working with a person from Microsoft Research that will be used as a reference. I strongly this is going to be an interesting project endeavor. This will form as an excellent educational program to develop online courses that will utilize the DOOM source code as a training material for understanding legacy software for people who have not written that source code before, but must understand it for the sake of preventing of being FIRED by his employer.

View all 7 project logs

Build Instructions

Collapse

Instructions use in the development... I do plan to have youtube videos on the subject.

In Development ASAP

Step 2

Discussions

David Blubaugh wrote 05/18/2020 at 05:16

Please provide feedback ??

Are you sure? yes | no

DOOM SOURCE CODE - SOFTWARE ARCHAEOLOGY- ISABELLE

Description

Details