Sökning: "Interactive theorem prover"
Visar resultat 1 - 5 av 7 uppsatser innehållade orden Interactive theorem prover.
1. A Verified QBF Solver
Master-uppsats, Uppsala universitet/Institutionen för informationsteknologiSammanfattning : 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. LÄS MER
2. Simple formally verified compiler in Lean
Kandidat-uppsats, Uppsala universitet/Institutionen för informationsteknologiSammanfattning : 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. LÄS MER
3. Proof-producing resolution of indirect jumps in the binary intermediate representation BIR
Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)Sammanfattning : 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. LÄS MER
4. Verifying Correctness of Contract Decompositions
Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)Sammanfattning : 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. LÄS MER
5. Implementation and Verification of Sorting Algorithms with the Interactive Theorem Prover HOL
Kandidat-uppsats, Uppsala universitet/Institutionen för informationsteknologiSammanfattning : 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. LÄS MER