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 18 of 18 for “"interactive theorem prover"”.
-
An Interactive Theorem Prover for First-Order Dynamic Logic
… and applications in program veri cation, a theorem prover named KIV (Karlsruhe Interactive Veri er) Theorem Prover has already been developed. But a high degree of automation and its complexity make it di cult to use it for educational purposes. My research work is motivated towards the …
-
Translating timed I/O automata specifications for theorem proving in PVs
… and continuous evolution. In order to employ an interactive theorem prover in deducing properties of a timed input/output automaton, its state-transition based description has to be translated to the language of the theorem prover. This thesis describes a tool for translating from TIOA, the …
-
L-Fuzzy Relations in Coq
… reasoning and program execution using Coq, an interactive theorem prover based on Higher-Order Logic (HOL) with dependent types. This implementation can be used to specify and develop correct software based on L-fuzzy relations such as fuzzy controllers. We give an overview of lattices, L-fuzzy …
-
Approximation Algorithms using Allegories and Coq
… of allegories. The programming language and interactive theorem prover Coq is used for the implementation purposes. This language is based on Higher-Order Logic (HOL) with dependent types which support both reasoning and program execution. In addition to the abstract theory, we provide the …
-
Modal and Relevance Logics for Qualitative Spatial Reasoning
… used the functional programming language and interactive theorem prover Coq to implement the definitions and natural deduction rules in order to provide an interactive system for reasoning in the logic.
-
Interactions of (co)monads in Agda
… interaction laws of monads and comonads in the interactive theorem prover Agda. Effectful computations are modeled as monads, while comonads model computation-running machines. Interaction laws describe how computations may be uniformly run to yield values. We study monads and comonads on an …
-
Formalisation and execution of Linear Algebra: theorems and algorithms
… of Linear Algebra algorithms in Isabelle/HOL, an interactive theorem prover. The work is based on the HOL Multivariate Analysis library, whose matrix representation has been refined to datatypes that admit a representation in functional programming languages. This enables the generation of …
-
Qualitative Spatial Reasoning With Super-Intuitionistic Logics
… by formalising them in Isabelle-HOL, an interactive theorem-prover based on classical higher-order logic. A partial decidability result is given for an extension of intuitionistic second-order propositional logics, together with an account of its mechanisation.
-
On the Constructive Content of Proofs
… A generalization of Higman's Lemma is Kruskal's Theorem. We present a constructive proof of Kruskal's Theorem that is completely formalized in a theory of inductive definitions. As a practical part, we show that these methods can be carried out in an interactive theorem prover. Both approaches to …
-
Verification of DMAC Device Driver Operations in HOL4
… DMA device driver code in HOL4, which is an interactive theorem prover (ITP) used for machine-checked verification. This thesis verifies parts of Intel's IXGBE X550 device driver, which is a complex, 10 Gbit Network Interface Card (NIC). This verification takes the first significant step …
-
Specification and verification of sequential machines in rule-based hardware languages
… they design machines, and we encode them in an interactive theorem prover. For this, we address three challenges: (1) We build an expressive framework in which we can express both synthesizable designs and abstract specifications, and we connect and navigate between them in the proof assistant. …
-
A mechanized Theory of Aspects
… core calculi, entirely mechanized in the interactive theorem prover Isabelle/HOL. The emphasis of the work is placed on two different fields. Fundamental questions of modularity, type soundness and subtyping form the first such field. Technical considerations such as binders, variable …
-
Machine-aided analysis of vote privacy using computationally complete symbolic attacker
… we mechanized the CCSA technique in Coq, an interactive theorem-prover [BC04, PdAC+17] developed using the specification language Gallina. We demonstrate the effectiveness of our mechanization with the verification of authentication and secrecy guarantees of the Authenticated Die Hellman key …
-
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. …
-
Toward Bridging the Semantic Gap Between x86-64 Software Binaries and Abstract Languages for Formal Verification and Security
… operational semantics embedded within an Interactive Theorem Prover (ITP) (a 4-fold increase over prior work). The second contribution of this dissertation presents a largely automated methodology for generating formally proven equivalence theorems between decompiled x86-64 machine code …
-
Interactive theorem provers: issues faced as a user and tackled as a developer
Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a …
-
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 …
-
Formal Tools for Specifying Financial Smart Contracts
Financial smart contracts routinely manage billions of US dollars worth of digital assets, and as a consequence bugs in smart contracts can be extremely costly. Because of this, much work has been done in formal verification of smart contracts to prove a contract correct with regards to its …