Related papers: Isabelle's Metalogic: Formalization and Proof Chec…
There is an ecosystem of VDM libraries and extensions that includes a translation and proof environment for VDM in Isabelle. Translation works for a large subset of VDM-SL and further constructs are being added on demand. A key impediment…
The Students' Proof Assistant (SPA) aims to both teach how to use a proof assistant like Isabelle and also to teach how reliable proof assistants are built. Technically it is a miniature proof assistant inside the Isabelle proof assistant.…
This thesis concerns the development of a framework that facilitates the design and analysis of formal systems. Specifically, this framework provides a specification language which supports the concise and direct description of formal…
In this paper, we present a proof theory for attack trees. Attack trees are a well established and useful model for the construction of attacks on systems since they allow a stepwise exploration of high level attacks in application…
We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic…
We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with first-class type constructors, first-class polymorphism, or…
This paper presents IsaBIL, a binary analysis framework in Isabelle/HOL that is based on the widely used Binary Analysis Platform (BAP). Specifically, in IsaBIL, we formalise BAP's intermediate language, called BIL and integrate it with…
The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adequately. In the case of Isabelle, an export of the library…
Representation determines how we can reason about a specific problem. Sometimes one representation helps us find a proof more easily than others. Most current automated reasoning tools focus on reasoning within one representation. There is,…
This thesis develops a framework for formalizing reasoning about specifications of systems written in LF. This formalization centers around the development of a reasoning logic that can express the sorts of properties which arise in…
We consider the problem of how to verify the security of probabilistic oblivious algorithms formally and systematically. Unfortunately, prior program logics fail to support a number of complexities that feature in the semantics and…
Simulation and formal verification are important complementary techniques necessary in high assurance model-based systems development. In order to support coherent results, it is necessary to provide unifying semantics and automation for…
We define a fragment of metric first-order temporal logic formulas that guarantees the finiteness of their table representations. We extend our fragment's definition to cover the temporal dual operators trigger and release and show that our…
Education in the practical applications of logic and proving such as the formal specification and verification of computer programs is substantially hampered by the fact that most time and effort that is invested in proving is actually…
Simulink is a widely used model-based development environment for embedded systems. Stateflow is a component of Simulink for modeling event-driven control via hierarchical state machines and flow charts. However, Stateflow lacks an official…
Informal logic is a method of argument analysis which is complementary to that of formal logic, providing for the pragmatic treatment of features of argumentation which cannot be reduced to logical form. The central claim of this paper is…
Many facts possess symmetrical counterparts that often require a separate formal proof, depending on the nature of the involved symmetry. We introduce a method in Isabelle/HOL which produces such a symmetrical fact for the list datatype and…
We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using…
Program logics are a powerful formal method in the context of program verification. Can we develop a counterpart of program logics in the context of language verification? This paper proposes language logics, which allow for statements of…
We present a formalisation of finite Markov decision processes with rewards in the Isabelle theorem prover. We focus on the foundations required for dynamic programming and the use of reinforcement learning agents over such processes. In…