9 citations · 22 across the 10 of their papers we have counts for
6 papers · 1 filter
A Verified Implementation of B+-Trees in Isabelle/HOL
Niels Mündler, Tobias Nipkow
In this paper we present the verification of an imperative implementation of the ubiquitous B+-tree data structure in the interactive theorem prover Isabelle/HOL. The implementatio…
Isabelle's Metalogic: Formalization and Proof Checker
Tobias Nipkow, Simon Roßkopf
Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogi…
Verified Approximation Algorithms
Robin Eßmann, Tobias Nipkow, Simon Robillard +1
We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, set cover, center selection, load balanci…
A Verified Decision Procedure for Orders in Isabelle/HOL
Lukas Stevens, Tobias Nipkow
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 pro…
From LCF to Isabelle/HOL
Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel
Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today's powerful systems. Here, we focus on Isabelle/HOL and its di…
Interactive verification of Markov chains: Two distributed protocol case studies
Johannes Hölzl, Tobias Nipkow
Probabilistic model checkers like PRISM only check probabilistic systems of a fixed size. To guarantee the desired properties for an arbitrary size, mathematical analysis is necess…