Related papers: Algebraic Principles for Rely-Guarantee Style Conc…
This paper presents an overview of the verification framework ALICE in its current version 0.7. It is based on the generic theorem prover Isabelle [Pau03a]. Within ALICE a software or hardware component is specified as a state-full…
We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which…
Numerical methods based on interval arithmetic are efficient means to reliably solve nonlinear systems of equations. Algorithm bc3revise is an interval method that tightens variables' domains by enforcing a property called box consistency.…
We formalise the basics of the double-pushout approach to graph transformation in the proof assistant Isabelle/HOL and provide associated machine-checked proofs. Specifically, we formalise graphs, graph morphisms and rules, and a definition…
Abella is an interactive system for reasoning about aspects of object languages that have been formally presented through recursive rules based on syntactic structure. Abella utilizes a two-level logic approach to specification and…
When faced with the question of how to represent properties in a formal proof system any user has to make design decisions. We have proved three of the theorems from Maskin's 2004 survey article on Auction Theory using the Isabelle/HOL…
A Forensic Lucid intensional programming language has been proposed for intensional cyberforensic analysis. In large part, the language is based on various predecessor and codecessor Lucid dialects bound by the higher-order intensional…
We formalize in the proof assistant Isabelle essential basic notions and results in financial mathematics. We provide generic formal definitions of concepts such as markets, portfolios, derivative products, arbitrages or fair prices, and we…
The purpose of this paper is to explore the question "to what extent could we produce formal, machine-verifiable, proofs in real algebraic geometry?" The question has been asked before but as yet the leading algorithms for answering such…
A protocol-independent secrecy theorem is established and applied to several non-trivial protocols. In particular, it is applied to protocols proposed for protecting the computation results of free-roaming mobile agents doing comparison…
We introduce a new methodology based on refinement for testing the functional correctness of hardware and low-level software. Our methodology overcomes several major drawbacks of the de facto testing methodologies used in industry: (1) it…
Software is now ubiquitous and involved in complex interactions with the human users and the physical world in so-called cyber-physical systems where the management of time is a major issue. Separation of concerns is a key asset in the…
$\alpha$Check is a light-weight property-based testing tool built on top of $\alpha$Prolog, a logic programming language based on nominal logic. $\alpha$Prolog is particularly suited to the validation of the meta-theory of formal systems,…
We propose an approach for searching for counterexamples of statements about algebraic structures with a medium-sized signature using the Isabelle proof assistant in an efficient, parallel manner. We contribute a Python client Isabelle…
We report on the mechanization of (preference-based) conditional normative reasoning. Our focus is on Aqvist's system E for conditional obligation, and its extensions. Our mechanization is achieved via a shallow semantical embedding in…
We introduce Refinement Reflection, a new framework for building SMT-based deductive verifiers. The key idea is to reflect the code implementing a user-defined function into the function's (output) refinement type. As a consequence, at uses…
Algebraic specifications of data types provide a natural basis for testing data types implementations. In this framework, the conformance relation is based on the satisfaction of axioms. This makes it possible to formally state the…
This book can be seen either as a text on theorem proving that uses techniques from general algebra, or else as a text on general algebra illustrated and made concrete by practical exercises in theorem proving. The book considers several…
The reflection principle is the statement that if a sentence is provable then it is true. Reflection principles have been studied for first-order theories, but they also play an important role in propositional proof complexity. In this…
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…