Sökning: "Interactive theorem proving"
Hittade 5 uppsatser innehållade orden Interactive theorem proving.
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. Oracle Integration of Floating-Point Solvers with Isabelle
Master-uppsats, Uppsala universitet/Institutionen för informationsteknologiSammanfattning : Interactivity is both a blessing and a curse in theorem proving; withgreat power comes great time consumption and labor. It is therefore crucial to increase proof automation in interactive proof assistants. 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. Provably Sound and Secure Automatic Proving and Generation of Verification Conditions
Master-uppsats, KTH/Teoretisk datalogi, TCSSammanfattning : Formal verification of programs can be done with the aid of an interactive theorem prover. The program to be verified is represented in an intermediate language representation inside the interactive theorem prover, after which statements and their proofs can be constructed. This is a process that can be automated to a high degree. LÄS MER