David Blubaugh
tutorial.pdfMore Isabelle HOL material of importance.Adobe Portable Document Format - 1.01 MB - 05/21/2020 at 04:15 |
|
|
a56309601974c4ba5285042321ade45c9899.pdfUSE of machine learning within Iaabelle HOL.Adobe Portable Document Format - 545.26 kB - 05/21/2020 at 04:15 |
|
|
A_Learning-Based_Fact_Selector_for_IsabelleHOL.pdfAdditional use of machine learning for ISabelle HOL .Adobe Portable Document Format - 384.97 kB - 05/21/2020 at 04:15 |
|
|
formal_game.pdfA 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 |
|
|
chocolate-doom-3.0.0-win32.zipBased 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 |
|
|
exam-14.zipLecture notes on the use of C analysis for the DOOM source code.x-zip-compressed - 12.25 MB - 05/17/2020 at 10:05 |
|
|
VC.pdfVerifiable 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 |
|
|
slides.pdfBasic notationThe 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 |
|
|
DOOM-master.zipOriginal 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 |
|
|
82676025.pdfWe present an approach for automatically generating provablycorrect 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 |
|
|
|
Adobe Portable Document Format - 912.26 kB - 05/11/2020 at 08:46 |
|
|
|
application/pdf - 1.56 MB - 05/10/2020 at 02:47 |
|
|
|
Adobe Portable Document Format - 937.64 kB - 05/08/2020 at 05:30 |
|
|
|
Adobe Portable Document Format - 843.37 kB - 05/04/2020 at 07:52 |
|
|
|
Adobe Portable Document Format - 1.91 MB - 05/04/2020 at 07:33 |
|
|
|
Adobe Portable Document Format - 1.24 MB - 05/04/2020 at 07:31 |
|
|
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