354 papers · page 7 of 18
William Schultz, Ian Dardik, Stavros Tripakis
We present a formal, machine checked TLA+ safety proof of MongoRaftReconfig, a distributed dynamic reconfiguration protocol. MongoRaftReconfig was designed for and implemented in MongoDB, a distributed database whose replication protocol is derived from the Raft consensus algorit…
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino
On in-order processors, without dynamic instruction scheduling, program running times may be significantly reduced by compile-time instruction scheduling. We present here the first effective certified instruction scheduler that operates over superblocks (it may move instructions …
Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt
Build systems are a fundamental part of software construction, but their correctness has received comparatively little attention, relative to more prominent parts of the toolchain. In this paper, we address the correctness of forward build systems, which automatically determine t…
Simon Friis Vindum, Dan Frumin, Lars Birkedal
We present the first formal specification and verification of the fine-grained concurrent multi-producer-multi-consumer queue algorithm from Meta’s C++ library Folly of core infrastructure components. The queue is highly optimized, practical, and used by Meta in production where …
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional lang…
Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar
Proof engineering efforts using interactive theorem proving have yielded several impressive projects in software systems and mathematics. A key obstacle to such efforts is the requirement that the domain expert is also an expert in the low-level details in constructing the proof …
Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin
We introduce a static analysis and two program transformations for Datalog to circumvent performance ssues that arise with the implementation of primitive predicates, notably in the framework of a large scale telecommunication application. To this effect, we introduce a new trace…
Véronique Benzaken, Sarah Cohen-Boulakia, Evelyne Contejean, Chantal Keller, Rébecca Zucchini
In multiple domains, large amounts of data are daily generated and combined to be analyzed. The interpretation of these analyses requires to track back the provenance of combined data with respect to initial, raw data. The correctness of the provenance is crucial in many critical…
Elliot Catt, Michael Norrish
Kolmogorov complexity is an essential tool in the study of algorithmic information theory, and is used in the fields of Artificial Intelligence, cryptography, and coding theory. The formalisation of the theorems of Kolmogorov complexity is also key to proving results in the theor…
Chris Chhak, Andrew Tolmach, Sean Noble Anderson
Hardware-assisted reference monitoring is receiving increasing attention as a way to improve the security of existing software. One example is the PIPE architecture extension, which attaches metadata tags to register and memory values and executes tag-based rules at each machine …
Johan Commelin, Robert Y. Lewis
The ring of Witt vectors W R over a base ring R is an important tool in algebraic number theory and lies at the foundations of modern p-adic Hodge theory. W R has the interesting property that it constructs a ring of characteristic 0 out of a ring of characteristic p > 1, and it …
Martin Desharnais, Stefan Brunthaler
The prevalence of dynamic languages is not commensurate with the security guarantees provided by their execution mechanisms. Consider, for example, the ubiquitous case of JavaScript: it runs everywhere and its complex just-in-time compilers produce code that is fast and, unfortun…
Max W. Haslbeck, René Thiemann
AProVE is a powerful termination prover for various programming languages, including a termination analysis method for imperative programs specified in the LLVM intermediate representation (IR). The method internally works in three steps: first, it transforms LLVM IR code into a …
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson
Session types—a family of type systems for message-passing concurrency—have been subject to many extensions, where each extension comes with a separate proof of type safety. These extensions cannot be readily combined, and their proofs of type safety are generally not machine che…
Jason Z. S. Hu, Jacques Carette
The generality and pervasiveness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not have a standard, working formalization …
Dominik Kirst, Felix Rech
We discuss and compare two Coq mechanisations of Sierpinski's result that the generalised continuum hypothesis (GCH) implies the axiom of choice (AC). The first version shows the result, originally stated in first-order ZF set-theory, for a higher-order set theory convenient to w…
Olivier Laurent
We investigate the possibility of formalizing quantifiers in proof theory while avoiding, as far as possible, the use of true binding structures, α-equivalence or variable renamings. We propose a solution with two kinds of variables in terms and formulas, as originally done by Ge…
Jannis Limperg
In theorem provers based on dependent type theory such as Coq and Lean, induction is a fundamental proof method and induction tactics are omnipresent in proof scripts. Yet the ergonomics of existing induction tactics are not ideal: they do not reliably support inductive predicate…
Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer
The first-order theory of rewriting is a decidable theory for finite left-linear right-ground rewrite systems, implemented in FORT. We present a formally verified variant of the decision procedure for the class of linear variable-separated rewrite systems. This variant supports a…
Andreas Lööw
We report on a new verified Verilog compiler called Lutsig. Lutsig currently targets (a class of) FPGAs and is capable of producing technology mapped netlists for FPGAs. We have connected Lutsig to existing Verilog development tools, and in this paper we show how Lutsig, as a con…