Related papers: Hybrid Systems Verification with Isabelle/HOL: Sim…

We introduce a new approach to analyze distributed hybrid systems by a generalization of rely-guarantee reasoning. First, we give a system for deductive verification of class invariants and method contracts in object-oriented distributed…

We present the first verified implementation of a decision procedure for the quantifier-free theory of partial and linear orders. We formalise the procedure in Isabelle/HOL and provide a specification that is made executable using…

The Isabelle/PIDE platform addresses the question whether proof assistants of the LCF family are suitable as technological basis for educational tools. The traditionally strong logical foundations of systems like HOL, Coq, or Isabelle have…

Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, they did not have a systematic way to encode their expertise. To address this…

Combining higher-order abstract syntax and (co)induction in a logical framework is well known to be problematic. Previous work described the implementation of a tool called Hybrid, within Isabelle HOL, which aims to address many of these…

A hybrid model involves the cooperation of an interpretable model and a complex black box. At inference, any input of the hybrid model is assigned to either its interpretable or complex component based on a gating mechanism. The advantages…

Many proof assistant libraries contain formalizations of the same mathematical concepts. The concepts are often introduced (defined) in different ways, but the properties that they have, and are in turn formalized, are the same. For the…

We argue that the implementation and verification of compilers for functional programming languages are greatly simplified by employing a higher-order representation of syntax known as Higher-Order Abstract Syntax or HOAS. The underlying…

We present a proof procedure for univariate real polynomial problems in Isabelle/HOL. The core mathematics of our procedure is based on univariate cylindrical algebraic decomposition. We follow the approach of untrusted certificates,…

In the hardware design process, hardware components are usually described in a hardware description language. Most of the hardware description languages, such as Verilog and VHDL, do not have mathematical foundation and hence are not fit…

This paper presents a formalisation of pGCL in Isabelle/HOL. Using a shallow embedding, we demonstrate close integration with existing automation support. We demonstrate the facility with which the model can be extended to incorporate…

Assurance cases are often required to certify critical systems. The use of formal methods in assurance can improve automation, increase confidence, and overcome errant reasoning. However, assurance cases can never be fully formalised, as…

Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL), a framework for combining reasoning principles from distinct…

Using Isabelle/HOL, we verify the state-of-the-art decision procedure for multi-level syllogistic with singleton (MLSS for short), which is a quantifier-free fragment of set theory. We formalise its syntax and semantics as well as a sound…

This is an overview of the Isabelle technology behind the Archive of Formal Proofs (AFP). Interactive development and quasi-interactive build jobs impose significant demands of scalability on the logic (usually Isabelle/HOL), on Isabelle/ML…

This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in…

Interactive theorem provers are complex systems that require sophisticated platform efforts - and hence systems programming environments - to manage effectively. The Isabelle platform exemplifies this with its Isabelle/Scala systems…

Mission-time Linear Temporal Logic (MLTL) is rapidly increasing in popularity as a specification logic, e.g., for runtime verification and model checking, driving a need for a trustworthy tool base for analyzing MLTL. In this work, we…

Hybrid systems are characterized by the hybrid evolution of their state: A part of the state changes discretely, the other part changes continuously over time. Typically, modern control applications belong to this class of systems, where a…

The model-checking problem for hybrid systems is a well known challenge in the scientific community. Most of the existing approaches and tools are limited to safety properties only, or operates by transforming the hybrid system to be…