Global ETD Search
Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.
Results
Showing 1 to 12 of 12 for “"interactive theorem proving"”.
-
User interaction widgets for interactive theorem proving
Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of …
-
Building trustworthy smart contracts using interactive theorem proving
… apply to the real bytecode executed on-chain. Interactive theorem proving can provide the foundation for developing provably correct smart contracts. Due to the immutable nature of smart contracts and their potential to manage highly valuable assets and tokens representing power, techniques to …
-
Automated proof checking in introductory discrete mathematics classes
… and probability concepts using Coq, an interactive theorem proving language.
-
Towards justifying computer algebra algorithms in Isabelle/HOL
As verification efforts using interactive theorem proving grow, we are in need of certified algorithms in computer algebra to tackle problems over the real numbers. This is important because uncertified procedures can drastically increase the size of the trust base and under- mine the overall …
-
Formal verification of biologically inspired computing models
… To verify cP systems, both model checking and interactive theorem proving are considered in this thesis. By using formal tools including PAT3, ProB, and Coq, several cP systems were verified including two NPC solutions proposed in this study. These are: ΠSSP - a cP system that solves the subset …
-
Low-Level Static Analysis for Memory Usage and Control Flow Recovery
… of noninterference. However, soundly proving memory usage requires operating on the assembly level due to the semantic gap between high-level languages and the code that processors actually execute. Automated methods, such as model checking, would not be able to handle many interesting …
-
A Tool for Producing Verified, Explainable Proofs
Mathematicians are reluctant to use interactive theorem provers. In this thesis I argue that this is because proof assistants don't emphasise explanations of proofs; and that in order to produce good explanations, the system must create proofs in a manner that mimics how humans would create proofs. …
-
Formalizing Clifford algebras and related constructions in the Lean theorem prover
… primarily by engineers and physicists, while theorem proving software has its background originally in computer science departments. This thesis brings the former into the language of the latter, in the more abstract setting of Clifford algebras. It does so via the theorem proving language …
-
Verified collection-based regression test selection via an extended Jinja semantics
… framework for Java and JVM developed in the theorem prover Isabelle that includes several semantics: Java-level big-step and small-step semantics, JVM-level small-step semantics, and an intermediate compilation step, J1, between these two levels. Regression Test Selection (RTS) algorithms …
-
Reasoning Using Higher-Order Abstract Syntax in a Higher-Order Logic Proof Environment: Improvements to Hybrid and a Case Study
We present a series of improvements to the Hybrid system, a formal theory implemented in Isabelle/HOL to support specifying and reasoning about formal systems using higher-order abstract syntax (HOAS). We modify Hybrid's type of terms, which is built definitionally in terms of de Bruijn indices, to …
-
Specifying and verifying program transformations with PTRANS
Software developers, compiler designers, and formal methods researchers all stand to benefit from improved tools for compiler design and verification. Program correctness for compiled languages depends fundamentally on compiler correctness, and compiler optimizations are usually not formally …