Essays about: "Interactive theorem prover"
Showing result 1 - 5 of 7 essays containing the words Interactive theorem prover.
-
1. A Verified QBF Solver
University essay from Uppsala universitet/Institutionen för informationsteknologiAbstract : Quantified Boolean Formulas (QBFs) extend propositional logic with universal and existential quantification over Boolean variables. A QBF is satisfiable if and only if there is an assignment of Boolean values to the free variables that makes the formula true, and a QBF solver is a software tool determining if a given QBF is satisfiable. READ MORE
-
2. Simple formally verified compiler in Lean
University essay from Uppsala universitet/Institutionen för informationsteknologiAbstract : Computer checked proofs that a compiler is correct are important for increasing the confidence in programs. This report presents a simple compiler and a proof that the compiler is correct for terminating evaluations using the interactive theorem prover Lean, based on Concrete Semantics: with Isabelle/HOL. READ MORE
-
3. Proof-producing resolution of indirect jumps in the binary intermediate representation BIR
University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)Abstract : HolBA is a binary analysis library that can be used to formally verify binary programs using contracts. It is developed in the interactive theorem prover HOL4 to achieve a high degree of trust in verification, the result of verification is a machine-checked proof demonstrating its correctness. This thesis presents two proof-producing procedures. READ MORE
-
4. Verifying Correctness of Contract Decompositions
University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)Abstract : The importance of verification in safety critical systems is well known. However, due to the complexity of verification, the task of formally verifying large safety-critical systems might prove computationally infeasible in many cases. Compositional verification is a technique aimed at enabling verification of large safety-critical systems. READ MORE
-
5. Implementation and Verification of Sorting Algorithms with the Interactive Theorem Prover HOL
University essay from Uppsala universitet/Institutionen för informationsteknologiAbstract : As the world becomes increasingly reliant on technology and the technology becomes increasingly complex, ensuring software correctness is becoming both increasingly important and difficult. Methods like software testing are rarely enough to guarantee that a program will always work as intended. Formal methods offer attractive alternatives. READ MORE
