Related papers: Mechanization of LAGC Semantics in Isabelle
LTL3 is a multi-valued variant of Linear-time Temporal Logic for runtime verification applications. The semantic descriptions of LTL3 in previous work are given only in terms of the relationship to conventional LTL. Our approach, by…
Model execution allows us to prototype and analyse software engineering models by stepping through their possible behaviours, using techniques like animation and simulation. On the other hand, deductive verification allows us to construct…
Mechanized verification of liveness properties for infinite programs with effects and nondeterminism is challenging. Existing temporal reasoning frameworks operate at the level of models such as traces and automata. Reasoning happens at a…
We present a formalization of basics related to infinite words in the generic proof assistant Isabelle/HOL. Furthermore, we present a formalization of purely morphic and morphic languages. Finally, we present a formalized definition of…
The "Concrete Semantics" book gives an introduction to imperative programming languages accompanied by an Isabelle/HOL formalization. In this paper we discuss a re-formalization of the book using the Coq proof assistant. In order to achieve…
Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full detail. We present soundness and completeness proofs of a…
Isabelle is a generic theorem prover, designed for interactive reasoning in a variety of formal theories. At present it provides useful proof procedures for Constructive Type Theory, various first-order logics, Zermelo-Fraenkel set theory,…
Proof assistants are important tools for teaching logic. We support this claim by discussing three formalizations in Isabelle/HOL used in a recent course on automated reasoning. The first is a formalization of System W (a system of…
Formalised libraries of combinatorial mathematics have rapidly expanded over the last five years, but few use one of the most important tools: probability. How can often intuitive probabilistic arguments on the existence of combinatorial…
The design and implementation of precise static analyzers for significant fragments of modern imperative languages like C, C++, Java and Python is a challenging problem. In this paper, we consider a core imperative language that has several…
Formal verification provides strong guarantees of correctness of software, which are especially important in safety or security critical systems. Hoare logic is a widely used formalism for rigorous verification of software against…
The context of this work is cooperative scheduling, a concurrency paradigm, where task execution is not arbitrarily preempted. Instead, language constructs exist that let a task voluntarily yield the right to execute to another task. The…
We present a semi-automated framework to construct and reason about programs in a deeply-embedded while-language. The while-language we consider is a simple computation model that can simulate (and be simulated by) Turing Machines with a…
Lambek Grammars (LG) are a computational modelling of natural language, based on non-commutative compositional types. It has been widely studied, especially for languages where the syntax plays a major role (like English). The goal of this…
Description Logics (DLs) are a family of languages used for the representation and reasoning on the knowledge of an application domain, in a structured and formal manner. In order to achieve this objective, several provers, such as RACER…
Concurrent revisions is a concurrency control model designed to guarantee determinacy, meaning that the outcomes of programs are uniquely determined. This paper describes an Isabelle/HOL formalization of the model's operational semantics…
Automatically generating formal specifications including loop invariants, preconditions, and postconditions for legacy code is critical for program understanding, reuse and verification. However, the inherent complexity of control and data…
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…
Software tools of Automated Reasoning are too sophisticated for general use in mathematics education and respective reasoning, while Lucas-Interpretation provides a general concept for integrating such tools into educational software with…
We present a lattice of distributed program specifications, whose ordering represents implementability/refinement. Specifications are modelled by families of subsets of relative execution traces, which encode the local orderings of state…