Files | DOOM SOURCE CODE - SOFTWARE ARCHAEOLOGY- ISABELLE

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

exam-14.zip

Lecture notes on the use of C analysis for the DOOM source code.

x-zip-compressed - 12.25 MB - 05/17/2020 at 10:05

Download

VC.pdf

Verifiable C is a program logic for the C programming language:
foundational higher-order impredicative concurrent separation logic, proved sound with respect to the operational semantics of CompCert C

Adobe Portable Document Format - 712.99 kB - 05/17/2020 at 04:21

Preview

slides.pdf

Basic notation
The syntax of terms and types in HOL is introduced.
Recursion and induction on lists
A prototypical example of recursion and induction on lists: the append and reverse functions are defined and rev(rev xs) = xs is proved. This introduces the proof methods induct and auto and allows students to start with proofs about lists.
Datatypes and recursive functions
A thorough introduction to the definition of datatypes and recursive functions. This generalizes and extends the material of session 1. It starts with a few words on the meta-logic just to explain the notation.
Simplification
The concept of (conditional) term rewriting is introduced and its realization as the proof method simp is explained.
Induction heuristics
Important generalization heuristics for inductive proofs are discussed by way of an example, the correctness proof of an iterative list reversal function.
Propositional logic
Introduces natural deduction proofs for propositional logic and the proof methods rule

Adobe Portable Document Format - 844.43 kB - 05/17/2020 at 04:05

Preview

DOOM-master.zip

Original DOOM source code released by John Carmack himself back in 1997. This will be the first victimized source code base for analysis and verification and validation by Isabelle HOL.

Here it is, at long last. The DOOM source code is released for your
non-profit use. You still need real DOOM data to work with this code.
If you don't actually own a real copy of one of the DOOMs, you should
still be able to find them at software stores.

Many thanks to Bernd Kreimeier for taking the time to clean up the
project and make sure that it actually works. Projects tends to rot if
you leave it alone for a few years, and it takes effort for someone to
deal with it again.

The bad news: this code only compiles and runs on linux. We couldn't
release the dos code because of a copyrighted sound library we used
(wow, was that a mistake -- I write my own sound code now), and I
honestly don't even know what happened to the port that microsoft did
to windows.

Still, the code is quite portab

x-zip-compressed - 460.60 kB - 05/16/2020 at 19:58

Download

82676025.pdf

We present an approach for automatically generating provably
correct abstractions from C source code for that are useful for practical
implementation verification. The abstractions are easier for a human
verification engineer to reason about than the implementation and
increase the productivity of interactive code proof. We guarantee
soundness by automatically generating proofs that the abstractions
are correct.
In particular, we show two key abstractions that are critical for
verifying DOOM C source code: automatically turning potentially
overflowing machine-word arithmetic into ideal integers, and transforming low-level C pointer reasoning into separate abstract heaps.
Previous work carrying out such transformations has either done so
using unverified translations, or required significant proof engineering effort.
We implement these abstractions in an existing proof-producing
specification transformation framework named AutoCorres, developed in Isabelle/HOL, and demonstrate its effec

Adobe Portable Document Format - 261.94 kB - 05/16/2020 at 19:45

Preview

seL4-whitepaper.pdf

Adobe Portable Document Format - 912.26 kB - 05/11/2020 at 08:46

Preview

concrete-semantics.pdf

application/pdf - 1.56 MB - 05/10/2020 at 02:47

Preview

HOLNik.pdf

Adobe Portable Document Format - 937.64 kB - 05/08/2020 at 05:30

Preview

2015-winter-meeting.pdf

Adobe Portable Document Format - 843.37 kB - 05/04/2020 at 07:52

Preview

public_version.pdf

Adobe Portable Document Format - 1.91 MB - 05/04/2020 at 07:33

Preview

Tuch2009_Article_FormalVerificationOfCSystemsCo.pdf

Adobe Portable Document Format - 1.24 MB - 05/04/2020 at 07:31

Preview

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
exam-14.zip Lecture notes on the use of C analysis for the DOOM source code. x-zip-compressed - 12.25 MB - 05/17/2020 at 10:05		Download
VC.pdf Verifiable C is a program logic for the C programming language: foundational higher-order impredicative concurrent separation logic, proved sound with respect to the operational semantics of CompCert C Adobe Portable Document Format - 712.99 kB - 05/17/2020 at 04:21		Preview

slides.pdf Basic notation The syntax of terms and types in HOL is introduced. Recursion and induction on lists A prototypical example of recursion and induction on lists: the append and reverse functions are defined and rev(rev xs) = xs is proved. This introduces the proof methods induct and auto and allows students to start with proofs about lists. Datatypes and recursive functions A thorough introduction to the definition of datatypes and recursive functions. This generalizes and extends the material of session 1. It starts with a few words on the meta-logic just to explain the notation. Simplification The concept of (conditional) term rewriting is introduced and its realization as the proof method simp is explained. Induction heuristics Important generalization heuristics for inductive proofs are discussed by way of an example, the correctness proof of an iterative list reversal function. Propositional logic Introduces natural deduction proofs for propositional logic and the proof methods rule Adobe Portable Document Format - 844.43 kB - 05/17/2020 at 04:05		Preview

DOOM-master.zip Original DOOM source code released by John Carmack himself back in 1997. This will be the first victimized source code base for analysis and verification and validation by Isabelle HOL. Here it is, at long last. The DOOM source code is released for your non-profit use. You still need real DOOM data to work with this code. If you don't actually own a real copy of one of the DOOMs, you should still be able to find them at software stores. Many thanks to Bernd Kreimeier for taking the time to clean up the project and make sure that it actually works. Projects tends to rot if you leave it alone for a few years, and it takes effort for someone to deal with it again. The bad news: this code only compiles and runs on linux. We couldn't release the dos code because of a copyrighted sound library we used (wow, was that a mistake -- I write my own sound code now), and I honestly don't even know what happened to the port that microsoft did to windows. Still, the code is quite portab x-zip-compressed - 460.60 kB - 05/16/2020 at 19:58		Download
82676025.pdf We present an approach for automatically generating provably correct abstractions from C source code for that are useful for practical implementation verification. The abstractions are easier for a human verification engineer to reason about than the implementation and increase the productivity of interactive code proof. We guarantee soundness by automatically generating proofs that the abstractions are correct. In particular, we show two key abstractions that are critical for verifying DOOM C source code: automatically turning potentially overflowing machine-word arithmetic into ideal integers, and transforming low-level C pointer reasoning into separate abstract heaps. Previous work carrying out such transformations has either done so using unverified translations, or required significant proof engineering effort. We implement these abstractions in an existing proof-producing specification transformation framework named AutoCorres, developed in Isabelle/HOL, and demonstrate its effec Adobe Portable Document Format - 261.94 kB - 05/16/2020 at 19:45		Preview

seL4-whitepaper.pdf Adobe Portable Document Format - 912.26 kB - 05/11/2020 at 08:46		Preview

concrete-semantics.pdf application/pdf - 1.56 MB - 05/10/2020 at 02:47		Preview

HOLNik.pdf Adobe Portable Document Format - 937.64 kB - 05/08/2020 at 05:30		Preview

2015-winter-meeting.pdf Adobe Portable Document Format - 843.37 kB - 05/04/2020 at 07:52		Preview

public_version.pdf Adobe Portable Document Format - 1.91 MB - 05/04/2020 at 07:33		Preview

Tuch2009_Article_FormalVerificationOfCSystemsCo.pdf Adobe Portable Document Format - 1.24 MB - 05/04/2020 at 07:31		Preview