Peter Lammich
YOU?
Author Swipe
View article: A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs Open
We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstract semantics of MDPs to a low-level implementation in LLVM …
View article: A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs Open
We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstract semantics of MDPs to a low-level implementation in LLVM …
View article: Efficient Formally Verified Maximal End Component Decomposition for MDPs
Efficient Formally Verified Maximal End Component Decomposition for MDPs Open
Identifying a Markov decision process’s maximal end components is a prerequisite for applying sound probabilistic model checking algorithms. In this paper, we present the first mechanized correctness proof of a maximal end component decomp…
View article: Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting
Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting Open
We present a stepwise refinement approach to develop verified parallel algorithms, down to efficient LLVM code. The resulting algorithms’ performance is competitive with their counterparts implemented in C++. Our approach is backwards comp…
View article: Fast and Verified UNSAT Certificate Checking
Fast and Verified UNSAT Certificate Checking Open
We describe a formally verified checker for unsatisfiability certificates in the LRAT format, which can be run in parallel with the SAT solver, processing the certificate while it is being produced. It is implemented time and memory effici…
View article: WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly
WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly Open
We present WasmRef-Isabelle, a monadic interpreter for WebAssembly written in Isabelle/HOL and proven correct with respect to the WasmCert-Isabelle mechanisation of WebAssembly. WasmRef-Isabelle has been adopted and deployed as a fuzzing o…
View article: Refinement of Parallel Algorithms down to LLVM applied to practically efficient parallel sorting
Refinement of Parallel Algorithms down to LLVM applied to practically efficient parallel sorting Open
We present a stepwise refinement approach to develop verified parallel algorithms, down to efficient LLVM code. The resulting algorithms' performance is competitive with their counterparts implemented in C/C++. Our approach is backwards co…
View article: A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper) Open
IsaSAT is the most advanced verified SAT solver, but it did not yet feature inprocessing (to simplify and strengthen clauses). In order to improve performance, we enriched the base calculus to not only do CDCL but also inprocess clauses. W…
View article: For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM
For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM Open
We present a framework to verify both, functional correctness and (amortized) worst-case complexity of practically efficient algorithms. We implemented a stepwise refinement approach, using the novel concept of resource currencies to natur…
View article: For a Few Dollars More
For a Few Dollars More Open
We present a framework to verify both, functional correctness and worst-case complexity of practically efficient algorithms. We implemented a stepwise refinement approach, using the novel concept of resource currencies to naturally structu…
View article: Bounded-Deducibility Security (Invited Paper)
Bounded-Deducibility Security (Invited Paper) Open
We describe Bounded-Deducibility (BD) security, an expressive framework for the specification and verification of information-flow security. The framework grew by confronting concrete challenges of specifying and verifying fine-grained con…
View article: CoCon: A Conference Management System with Formally Verified Document Confidentiality
CoCon: A Conference Management System with Formally Verified Document Confidentiality Open
We present a case study in formally verified security for realistic systems: the information flow security verification of the functional kernel of a web application, the CoCon conference management system. We use the Isabelle theorem prov…
View article: Efficient Verified (UN)SAT Certificate Checking
Efficient Verified (UN)SAT Certificate Checking Open
SAT solvers decide the satisfiability of Boolean formulas in conjunctive normal form. They are commonly used for software and hardware verification. Modern SAT solvers are highly complex and optimized programs. As a single bug in the solve…
View article: Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study
Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study Open
We verify functional correctness of insertion sort as well as the partition function of quicksort. We use Isabelle/UTP and its denotational semantics for imperative programs as a verification framework. We propose a forward Hoare VCG for o…
View article: Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL
Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL Open
Separation Logic with Time Credits is a well established method to formally verify the correctness and run-time of algorithms, which has been applied to various medium-sized use-cases. Refinement is a technique in program verification that…
View article: Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra
Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra Open
The starting point of this paper is a new, purely functional, simple and efficient data structure combining a search tree and a priority queue, which we call a priority search tree. The salient feature of priority search trees is that they…
View article: A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality Open
We developed a formal framework for conflict-driven clause learning (CDCL) using the Isabelle/HOL proof assistant. Through a chain of refinements, an abstract CDCL calculus is connected first to a more concrete calculus, then to a SAT solv…
View article: A verified SAT solver with watched literals using imperative HOL
A verified SAT solver with watched literals using imperative HOL Open
Based on our earlier formalization of conflict-driven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refi…
View article: Verified Model Checking of Timed Automata -- Artifact
Verified Model Checking of Timed Automata -- Artifact Open
This dataset, corresponding to the TACAS 2018 submission"Verified Model Checking of Timed Automata", contains source code, dependencies and instructions to build the tool described, as well as the benchmarks used to evaluate it.The tool pr…
View article: A Framework for Verifying Depth-First Search Algorithms
A Framework for Verifying Depth-First Search Algorithms Open
Many graph algorithms are based on depth-first search (DFS). The formalizations of such algorithms typically share many common ideas. In this paper, we summarize these ideas into a framework in Isabelle/HOL.Building on the Isabelle Refinem…