CPP '19: "A Coq Mechanised Formal Semantics ..."
A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra
Véronique Benzaken and Évelyne Contejean
(University of Paris-Sud, France; LRI, France; CNRS, France)
In this article, we provide a Coq mechanised, executable, formal semantics for a realistic fragment of SQL consisting of "select [distinct] from where group by having" queries with null values, functions, aggregates, quantifiers and nested potentially correlated sub-queries. Relying on the Coq extraction mechanism to Ocaml, we further produce a Coq certified semantic analyser for a SQL compiler. We then relate this fragment to a Coq formalised (extended) relational algebra that enjoys a bag semantics hence recovering all well-known algebraic equivalences upon which are based most of compilation optimisations. By doing so, we provide the first formally mechanised proof of the equivalence of SQL and extended relational algebra.
@InProceedings{CPP19p249,
author = {Véronique Benzaken and Évelyne Contejean},
title = {A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {249--261},
doi = {10.1145/3293880.3294107},
year = {2019},
}
Publisher's Version
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by low-level buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement.
@InProceedings{CPP19p234,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {234--248},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
CPP '19: "A Verified Prover Based on ..."
A Verified Prover Based on Ordered Resolution
Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel
(DTU, Denmark; Vrije Universiteit Amsterdam, Netherlands; ETH Zurich, Switzerland)
The superposition calculus, which underlies first-order theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional first-order ordered resolution prover and establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract nondeterministic specification, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for first-order logic.
@InProceedings{CPP19p152,
author = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel},
title = {A Verified Prover Based on Ordered Resolution},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {152--165},
doi = {10.1145/3293880.3294100},
year = {2019},
}
Publisher's Version
CPP '19: "Formalizing the Metatheory ..."
Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk)
Jasmin Christian Blanchette
(Vrije Universiteit Amsterdam, Netherlands)
IsaFoL (Isabelle Formalization of Logic) is an undertaking that aims at developing formal theories about logics, proof systems, and automatic provers, using Isabelle/HOL. At the heart of the project is the conviction that proof assistants have become mature enough to actually help researchers in automated reasoning when they develop new calculi and tools. In this paper, I describe and reflect on three verification subprojects to which I contributed: a first-order resolution prover, an imperative SAT solver, and generalized term orders for λ-free higher-order logic.
@InProceedings{CPP19p1,
author = {Jasmin Christian Blanchette},
title = {Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3293880.3294087},
year = {2019},
}
Publisher's Version
CPP '19: "Formal Verification of a Program ..."
Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
Sandrine Blazy and Rémi Hutin
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France)
The insertion of expressions mixing arithmetic operators and bitwise boolean operators is a widespread protection of sensitive data in source programs. This recent advanced obfuscation technique is one of the less studied among program obfuscations even if it is commonly found in binary code. In this paper, we formally verify in Coq this data obfuscation. It operates over a generic notion of mixed boolean-arithmetic expressions and on properties of bitwise operators operating over machine integers. Our obfuscation performs two kinds of program transformations: rewriting of expressions and insertion of modular inverses. To facilitate its proof of correctness, we define boolean semantic tables, a data structure inspired from truth tables.
Our obfuscation is integrated into the CompCert formally verified compiler where it operates over Clight programs. The automatic extraction of our program obfuscator into OCaml yields a program with competitive results.
@InProceedings{CPP19p196,
author = {Sandrine Blazy and Rémi Hutin},
title = {Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {196--208},
doi = {10.1145/3293880.3294103},
year = {2019},
}
Publisher's Version
Info
CPP '19: "A Proof-Theoretic Approach ..."
A Proof-Theoretic Approach to Certifying Skolemization
Kaustuv Chaudhuri, Matteo Manighetti, and Dale Miller
(Inria, France; LIX, France; École Polytechnique, France)
When presented with a formula to prove, most theorem provers for classical first-order logic process that formula following several steps, one of which is commonly called skolemization. That process eliminates quantifier alternation within formulas by extending the language of the underlying logic with new Skolem functions and by instantiating certain quantifiers with terms built using Skolem functions. In this paper, we address the problem of checking (i.e., certifying) proof evidence that involves Skolem terms. Our goal is to do such certification without using the mathematical concepts of model-theoretic semantics (i.e., preservation of satisfiability) and choice principles (i.e., epsilon terms). Instead, our proof checking kernel is an implementation of Gentzen's sequent calculus, which directly supports quantifier alternation by using eigenvariables. We shall describe deskolemization as a mapping from client-side terms, used in proofs generated by theorem provers, into kernel-side terms, used within our proof checking kernel. This mapping which associates skolemized terms to eigenvariables relies on using outer skolemization. We also point out that the removal of Skolem terms from a proof is influenced by the polarities given to propositional connectives.
@InProceedings{CPP19p78,
author = {Kaustuv Chaudhuri and Matteo Manighetti and Dale Miller},
title = {A Proof-Theoretic Approach to Certifying Skolemization},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {78--90},
doi = {10.1145/3293880.3294094},
year = {2019},
}
Publisher's Version
CPP '19: "A Coq Mechanised Formal Semantics ..."
A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra
Véronique Benzaken and Évelyne Contejean
(University of Paris-Sud, France; LRI, France; CNRS, France)
In this article, we provide a Coq mechanised, executable, formal semantics for a realistic fragment of SQL consisting of "select [distinct] from where group by having" queries with null values, functions, aggregates, quantifiers and nested potentially correlated sub-queries. Relying on the Coq extraction mechanism to Ocaml, we further produce a Coq certified semantic analyser for a SQL compiler. We then relate this fragment to a Coq formalised (extended) relational algebra that enjoys a bag semantics hence recovering all well-known algebraic equivalences upon which are based most of compilation optimisations. By doing so, we provide the first formally mechanised proof of the equivalence of SQL and extended relational algebra.
@InProceedings{CPP19p249,
author = {Véronique Benzaken and Évelyne Contejean},
title = {A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {249--261},
doi = {10.1145/3293880.3294107},
year = {2019},
}
Publisher's Version
CPP '19: "A Verified Protocol Buffer ..."
A Verified Protocol Buffer Compiler
Qianchuan Ye and Benjamin Delaware
(Purdue University, USA)
The code responsible for serializing and deserializing untrusted external data is a vital component of any software that communicates with the outside world, as any bugs in these components can compromise the entire system. This is particularly true for verified systems which rely on trusted code to process external data, as any defects in the parsing code can invalidate any formal proofs about the system. One way to reduce the trusted code base of these systems is to use interface generators like Protocol Buffer and ASN.1 to generate serializers and deserializers from data descriptors. Of course, these generators are not immune to bugs.
In this work, we formally verify a compiler for a realistic subset of the popular Protocol Buffer serialization format using the Coq proof assistant, proving once and for all the correctness of every generated serializer and deserializer. One of the challenges we had to overcome was the extreme flexibility of the Protocol Buffer format: the same source data can be encoded in an infinite number of ways, and the deserializer must faithfully recover the original source value from each. We have validated our verified system using the official conformance tests.
@InProceedings{CPP19p222,
author = {Qianchuan Ye and Benjamin Delaware},
title = {A Verified Protocol Buffer Compiler},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {222--233},
doi = {10.1145/3293880.3294105},
year = {2019},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '19: "Verified Solving and Asymptotics ..."
Verified Solving and Asymptotics of Linear Recurrences
Manuel Eberl
(TU Munich, Germany)
Linear recurrences with constant coefficients are an interesting class of recurrence equations that can be solved explicitly. The most famous example are certainly the Fibonacci numbers with the equation f(n) = f(n−1) + f(n−2) and the quite non-obvious closed form
1√5
(ϕn − (−ϕ)−n)
where ϕ is the golden ratio.
This work builds on existing tools in Isabelle – such as formal power series and polynomial factorisation algorithms – to develop a theory of these recurrences and derive a fully executable solver for them that can be exported to programming languages like Haskell.
Based on this development, I also provide an efficient method to prove ‘Big-O’ asymptotics of a solution automatically without explicitly finding the closed-form solution first.
@InProceedings{CPP19p27,
author = {Manuel Eberl},
title = {Verified Solving and Asymptotics of Linear Recurrences},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {27--37},
doi = {10.1145/3293880.3294090},
year = {2019},
}
Publisher's Version
Info
CPP '19: "A Verified Ground Confluence ..."
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp
(University of Innsbruck, Austria; Allgemeines Rechenzentrum Innsbruck, Austria)
It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variable-separated rewrite systems. To this end, we formalize procedures for ground tree transducers and so-called RRn relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the first-order theory of ground rewriting for linear, variable-separated rewrite systems. It forms the basis for a formalized confluence checker for left-linear, right-ground systems.
@InProceedings{CPP19p132,
author = {Bertram Felgenhauer and Aart Middeldorp and T. V. H. Prathamesh and Franziska Rapp},
title = {A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {132--143},
doi = {10.1145/3293880.3294098},
year = {2019},
}
Publisher's Version
CPP '19: "A Linear Logical Framework ..."
A Linear Logical Framework in Hybrid (Invited Talk)
Amy P. Felty
(University of Ottawa, Canada)
We present a linear logical framework implemented within the Hybrid system [Felty and Momigliano 2012]. Hybrid is designed to support the use of higher-order abstract syntax for representing and reasoning about formal systems, implemented in the Coq Proof Assistant. In this work, we extend the system with a linear specification logic, which provides infrastructure for reasoning directly about object languages with linear features.
We developed this framework in order to address the challenges of reasoning about the type system of a quantum lambda calculus. In particular, we started by considering the Proto-Quipper language [Ross 2015], which contains the core of Quipper [Green et al. 2013; Selinger and Val- iron 2006]. Quipper is a new quantum programming language under active development with a linear type system. We have completed a formal proof of type soundness for Proto-Quipper [Mahmoud and Felty 2018b]. Our current work includes extending this work to other properties of Proto-Quipper as well as reasoning about other quantum programming languages [Mahmoud and Felty 2018a]. It also includes reasoning about other object languages with linear features in areas such as meta-theory of low-level abstract machine code, proof theory of focused linear sequent calculi, and modeling biological processes as transition systems and proving properties about them [Despeyroux et al. 2018].
@InProceedings{CPP19p14,
author = {Amy P. Felty},
title = {A Linear Logical Framework in Hybrid (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {14--14},
doi = {10.1145/3293880.3294088},
year = {2019},
}
Publisher's Version
CPP '19: "Certified Undecidability of ..."
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
Yannick Forster and Dominique Larchey-Wendling
(Saarland University, Germany; University of Lorraine, France; CNRS, France; LORIA, France)
We formally prove the undecidability of entailment in intuitionistic linear logic in Coq. We reduce the Post correspondence problem (PCP) via binary stack machines and Minsky machines to intuitionistic linear logic. The reductions rely on several technically involved formalisations, amongst them a binary stack machine simulator for PCP, a verified low-level compiler for instruction-based languages and a soundness proof for intuitionistic linear logic with respect to trivial phase semantics. We exploit the computability of all functions definable in constructive type theory and thus do not have to rely on a concrete model of computation, enabling the reduction proofs to focus on correctness properties.
@InProceedings{CPP19p104,
author = {Yannick Forster and Dominique Larchey-Wendling},
title = {Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {104--117},
doi = {10.1145/3293880.3294096},
year = {2019},
}
Publisher's Version
Info
CPP '19: "Call-By-Push-Value in Coq: ..."
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark
(Saarland University, Germany)
Call-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) CBPV, define its equational theory, and verify adequacy for the standard set/algebra denotational semantics. Furthermore, we prove normalisation of the standard reduction, confluence of strong reduction, strong normalisation using Kripke logical relations, and soundness of the equational theory using logical equivalence. We adapt and verify the known translations from CBV and CBN into CBPV for strong reduction. This yields, for instance, proofs of strong normalisation and confluence for the full λ-calculus with sums and products. Thanks to the automation provided by Coq and the Autosubst 2 framework, there is little formalisation overhead compared to detailed paper proofs.
@InProceedings{CPP19p118,
author = {Yannick Forster and Steven Schäfer and Simon Spies and Kathrin Stark},
title = {Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {118--131},
doi = {10.1145/3293880.3294097},
year = {2019},
}
Publisher's Version
Info
CPP '19: "On Synthetic Undecidability ..."
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Yannick Forster, Dominik Kirst, and Gert Smolka
(Saarland University, Germany)
We formalise the computational undecidability of validity, satisfiability, and provability of first-order formulas following a synthetic approach based on the computation native to Coq's constructive type theory. Concretely, we consider Tarski and Kripke semantics as well as classical and intuitionistic natural deduction systems and provide compact many-one reductions from the Post correspondence problem (PCP). Moreover, developing a basic framework for synthetic computability theory in Coq, we formalise standard results concerning decidability, enumerability, and reducibility without reference to a concrete model of computation. For instance, we prove the equivalence of Post's theorem with Markov's principle and provide a convenient technique for establishing the enumerability of inductive predicates such as the considered proof systems and PCP.
@InProceedings{CPP19p38,
author = {Yannick Forster and Dominik Kirst and Gert Smolka},
title = {On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {38--51},
doi = {10.1145/3293880.3294091},
year = {2019},
}
Publisher's Version
Info
CPP '19: "Dynamic Class Initialization ..."
Dynamic Class Initialization Semantics: A Jinja Extension
Susannah Mansky and Elsa L. Gunter
(University of Illinois at Urbana-Champaign, USA)
The Java Virtual Machine (JVM) postpones running class initialization methods until their classes are first referenced, such as by a new or static instruction. This process is called dynamic class initialization. Jinja is a semantic framework for Java and JVM developed in the theorem prover Isabelle that includes several semantics: Java-level big-step and small-step semantics, JVM-level small-step semantics, and an intermediate compilation step, J1, between these two levels. In this paper, we extend Jinja to include support for static instructions and dynamic class initialization. We also extend and re-prove related proofs, including Java-level type safety, equivalence between Java-level big-step and small-step semantics, and the correctness of a compilation from the Java level to the JVM level through J1. This work is based on the Java SE 8 specification.
@InProceedings{CPP19p209,
author = {Susannah Mansky and Elsa L. Gunter},
title = {Dynamic Class Initialization Semantics: A Jinja Extension},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {209--221},
doi = {10.1145/3293880.3294104},
year = {2019},
}
Publisher's Version
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by low-level buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement.
@InProceedings{CPP19p234,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {234--248},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
CPP '19: "Formal Verification of a Program ..."
Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
Sandrine Blazy and Rémi Hutin
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France)
The insertion of expressions mixing arithmetic operators and bitwise boolean operators is a widespread protection of sensitive data in source programs. This recent advanced obfuscation technique is one of the less studied among program obfuscations even if it is commonly found in binary code. In this paper, we formally verify in Coq this data obfuscation. It operates over a generic notion of mixed boolean-arithmetic expressions and on properties of bitwise operators operating over machine integers. Our obfuscation performs two kinds of program transformations: rewriting of expressions and insertion of modular inverses. To facilitate its proof of correctness, we define boolean semantic tables, a data structure inspired from truth tables.
Our obfuscation is integrated into the CompCert formally verified compiler where it operates over Clight programs. The automatic extraction of our program obfuscator into OCaml yields a program with competitive results.
@InProceedings{CPP19p196,
author = {Sandrine Blazy and Rémi Hutin},
title = {Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {196--208},
doi = {10.1145/3293880.3294103},
year = {2019},
}
Publisher's Version
Info
CPP '19: "Smooth Manifolds and Types ..."
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
Fabian Immler and Bohua Zhan
(Carnegie Mellon University, USA; Institute of Software at Chinese Academy of Sciences, China)
We formalize the definition and basic properties of smooth manifolds in Isabelle/HOL. Concepts covered include partition of unity, tangent and cotangent spaces, and the fundamental theorem for line integrals. We also construct some concrete manifolds such as spheres and projective spaces. The formalization makes extensive use of the existing libraries for topology and analysis. The existing library for linear algebra is not flexible enough for our needs. We therefore set up the first systematic and large scale application of ``types to sets''. It allows us to automatically transform the existing (type based) library of linear algebra to one with explicit carrier sets.
@InProceedings{CPP19p65,
author = {Fabian Immler and Bohua Zhan},
title = {Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {65--77},
doi = {10.1145/3293880.3294093},
year = {2019},
}
Publisher's Version
CPP '19: "Autosubst 2: Reasoning with ..."
Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions
Kathrin Stark, Steven Schäfer, and Jonas Kaiser
(Saarland University, Germany)
Formalising metatheory in the Coq proof assistant is tedious as reasoning with binders without native support requires a lot of uninteresting technicalities. To relieve users from so-produced boilerplate, the Autosubst framework automates working with de Bruijn terms: For each annotated inductive type, Autosubst generates a corresponding instantiation operation for parallel substitutions and a decision procedure for assumption-free substitution lemmas. However, Autosubst is implemented in Ltac, Coq's tactic language, and thus suffers from Ltac's limitations. In particular, Autosubst is restricted to Coq and unscoped, non-mutual inductive types with a single sort of variables. In this paper, we present a new version of Autosubst that overcomes these restrictions. Autosubst 2 is an external code generator, which translates second-order HOAS specifications into potentially mutual inductive term sorts. We extend the equational theory of Autosubst to the case of mutual inductive sorts by combining the application of multiple parallel substitutions into exactly one instantiation operation for each sort, i.e. we parallelise substitutions to vector substitutions. The resulting equational theory is both simpler and more expressive than that of the original Autosubst framework and allows us to present an even more elegant proof of part A of the POPLMark challenge.
@InProceedings{CPP19p166,
author = {Kathrin Stark and Steven Schäfer and Jonas Kaiser},
title = {Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {166--180},
doi = {10.1145/3293880.3294101},
year = {2019},
}
Publisher's Version
Info
CPP '19: "On Synthetic Undecidability ..."
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Yannick Forster, Dominik Kirst, and Gert Smolka
(Saarland University, Germany)
We formalise the computational undecidability of validity, satisfiability, and provability of first-order formulas following a synthetic approach based on the computation native to Coq's constructive type theory. Concretely, we consider Tarski and Kripke semantics as well as classical and intuitionistic natural deduction systems and provide compact many-one reductions from the Post correspondence problem (PCP). Moreover, developing a basic framework for synthetic computability theory in Coq, we formalise standard results concerning decidability, enumerability, and reducibility without reference to a concrete model of computation. For instance, we prove the equivalence of Post's theorem with Markov's principle and provide a convenient technique for establishing the enumerability of inductive predicates such as the considered proof systems and PCP.
@InProceedings{CPP19p38,
author = {Yannick Forster and Dominik Kirst and Gert Smolka},
title = {On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {38--51},
doi = {10.1145/3293880.3294091},
year = {2019},
}
Publisher's Version
Info
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by low-level buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement.
@InProceedings{CPP19p234,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {234--248},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
CPP '19: "Certified Undecidability of ..."
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
Yannick Forster and Dominique Larchey-Wendling
(Saarland University, Germany; University of Lorraine, France; CNRS, France; LORIA, France)
We formally prove the undecidability of entailment in intuitionistic linear logic in Coq. We reduce the Post correspondence problem (PCP) via binary stack machines and Minsky machines to intuitionistic linear logic. The reductions rely on several technically involved formalisations, amongst them a binary stack machine simulator for PCP, a verified low-level compiler for instruction-based languages and a soundness proof for intuitionistic linear logic with respect to trivial phase semantics. We exploit the computability of all functions definable in constructive type theory and thus do not have to rely on a concrete model of computation, enabling the reduction proofs to focus on correctness properties.
@InProceedings{CPP19p104,
author = {Yannick Forster and Dominique Larchey-Wendling},
title = {Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {104--117},
doi = {10.1145/3293880.3294096},
year = {2019},
}
Publisher's Version
Info
CPP '19: "A Formal Proof of Hensel's ..."
A Formal Proof of Hensel's Lemma over the p-adic Integers
Robert Y. Lewis
(Vrije Universiteit Amsterdam, Netherlands)
The field of p-adic numbers ℚp and the ring of p-adic integers ℤp are essential constructions of modern number theory. Hensel’s lemma, described by Gouvêa as the “most important algebraic property of the p-adic numbers,” shows the existence of roots of polynomials over ℤp provided an initial seed point. The theorem can be proved for the p-adics with significantly weaker hypotheses than for general rings. We construct ℚp and ℤp in the Lean proof assistant, with various associated algebraic properties, and formally prove a strong form of Hensel’s lemma. The proof lies at the intersection of algebraic and analytic reasoning and demonstrates how the Lean mathematical library handles such a heterogeneous topic.
@InProceedings{CPP19p15,
author = {Robert Y. Lewis},
title = {A Formal Proof of Hensel's Lemma over the p-adic Integers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {15--26},
doi = {10.1145/3293880.3294089},
year = {2019},
}
Publisher's Version
CPP '19: "Counting Polynomial Roots ..."
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
Wenda Li and Lawrence C. Paulson
(University of Cambridge, UK)
Many problems in computer algebra and numerical analysis can be reduced to counting or approximating the real roots of a polynomial within an interval. Existing verified root-counting procedures in major proof assistants are mainly based on the classical Sturm theorem, which only counts distinct roots.
In this paper, we have strengthened the root-counting ability in Isabelle/HOL by first formally proving the Budan-Fourier theorem. Subsequently, based on Descartes' rule of signs and Taylor shift, we have provided a verified procedure to efficiently over-approximate the number of real roots within an interval, counting multiplicity. For counting multiple roots exactly, we have extended our previous formalisation of Sturm's theorem. Finally, we combine verified components in the developments above to improve our previous certified complex-root-counting procedures based on Cauchy indices. We believe those verified routines will be crucial for certifying programs and building tactics.
@InProceedings{CPP19p52,
author = {Wenda Li and Lawrence C. Paulson},
title = {Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {52--64},
doi = {10.1145/3293880.3294092},
year = {2019},
}
Publisher's Version
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by low-level buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement.
@InProceedings{CPP19p234,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {234--248},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by low-level buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement.
@InProceedings{CPP19p234,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {234--248},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
CPP '19: "Certified ACKBO ..."
Certified ACKBO
Alexander Lochmann and Christian Sternagel
(University of Innsbruck, Austria)
Term rewriting in the presence of associative and commutative function symbols constitutes a highly expressive model of computation, which is for example well suited to reason about parallel computations. However, it is well known that the standard notion of termination does not apply any more: any term rewrite system containing a commutativity rule is nonterminating. Thus, instead of adding AC-rules to a rewrite system, we switch to the notion of AC-termination. AC-termination can for example be shown using AC-compatible reduction orders. One specific example of such an order is ACKBO. We present our Isabelle/HOL formalization of the ACKBO order. On an abstract level this gives us a mechanized proof of the fact that ACKBO is indeed an AC-compatible reduction order. Moreover, we integrated corresponding check functions into the verified certifier CeTA. This has the more practical consequence of enabling the machine certification of AC-termination proofs generated by automated termination tools.
@InProceedings{CPP19p144,
author = {Alexander Lochmann and Christian Sternagel},
title = {Certified ACKBO},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {144--151},
doi = {10.1145/3293880.3294099},
year = {2019},
}
Publisher's Version
CPP '19: "A Proof-Theoretic Approach ..."
A Proof-Theoretic Approach to Certifying Skolemization
Kaustuv Chaudhuri, Matteo Manighetti, and Dale Miller
(Inria, France; LIX, France; École Polytechnique, France)
When presented with a formula to prove, most theorem provers for classical first-order logic process that formula following several steps, one of which is commonly called skolemization. That process eliminates quantifier alternation within formulas by extending the language of the underlying logic with new Skolem functions and by instantiating certain quantifiers with terms built using Skolem functions. In this paper, we address the problem of checking (i.e., certifying) proof evidence that involves Skolem terms. Our goal is to do such certification without using the mathematical concepts of model-theoretic semantics (i.e., preservation of satisfiability) and choice principles (i.e., epsilon terms). Instead, our proof checking kernel is an implementation of Gentzen's sequent calculus, which directly supports quantifier alternation by using eigenvariables. We shall describe deskolemization as a mapping from client-side terms, used in proofs generated by theorem provers, into kernel-side terms, used within our proof checking kernel. This mapping which associates skolemized terms to eigenvariables relies on using outer skolemization. We also point out that the removal of Skolem terms from a proof is influenced by the polarities given to propositional connectives.
@InProceedings{CPP19p78,
author = {Kaustuv Chaudhuri and Matteo Manighetti and Dale Miller},
title = {A Proof-Theoretic Approach to Certifying Skolemization},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {78--90},
doi = {10.1145/3293880.3294094},
year = {2019},
}
Publisher's Version
CPP '19: "Dynamic Class Initialization ..."
Dynamic Class Initialization Semantics: A Jinja Extension
Susannah Mansky and Elsa L. Gunter
(University of Illinois at Urbana-Champaign, USA)
The Java Virtual Machine (JVM) postpones running class initialization methods until their classes are first referenced, such as by a new or static instruction. This process is called dynamic class initialization. Jinja is a semantic framework for Java and JVM developed in the theorem prover Isabelle that includes several semantics: Java-level big-step and small-step semantics, JVM-level small-step semantics, and an intermediate compilation step, J1, between these two levels. In this paper, we extend Jinja to include support for static instructions and dynamic class initialization. We also extend and re-prove related proofs, including Java-level type safety, equivalence between Java-level big-step and small-step semantics, and the correctness of a compilation from the Java level to the JVM level through J1. This work is based on the Java SE 8 specification.
@InProceedings{CPP19p209,
author = {Susannah Mansky and Elsa L. Gunter},
title = {Dynamic Class Initialization Semantics: A Jinja Extension},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {209--221},
doi = {10.1145/3293880.3294104},
year = {2019},
}
Publisher's Version
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by low-level buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement.
@InProceedings{CPP19p234,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {234--248},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
CPP '19: "A Verified Ground Confluence ..."
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp
(University of Innsbruck, Austria; Allgemeines Rechenzentrum Innsbruck, Austria)
It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variable-separated rewrite systems. To this end, we formalize procedures for ground tree transducers and so-called RRn relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the first-order theory of ground rewriting for linear, variable-separated rewrite systems. It forms the basis for a formalized confluence checker for left-linear, right-ground systems.
@InProceedings{CPP19p132,
author = {Bertram Felgenhauer and Aart Middeldorp and T. V. H. Prathamesh and Franziska Rapp},
title = {A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {132--143},
doi = {10.1145/3293880.3294098},
year = {2019},
}
Publisher's Version
CPP '19: "A Proof-Theoretic Approach ..."
A Proof-Theoretic Approach to Certifying Skolemization
Kaustuv Chaudhuri, Matteo Manighetti, and Dale Miller
(Inria, France; LIX, France; École Polytechnique, France)
When presented with a formula to prove, most theorem provers for classical first-order logic process that formula following several steps, one of which is commonly called skolemization. That process eliminates quantifier alternation within formulas by extending the language of the underlying logic with new Skolem functions and by instantiating certain quantifiers with terms built using Skolem functions. In this paper, we address the problem of checking (i.e., certifying) proof evidence that involves Skolem terms. Our goal is to do such certification without using the mathematical concepts of model-theoretic semantics (i.e., preservation of satisfiability) and choice principles (i.e., epsilon terms). Instead, our proof checking kernel is an implementation of Gentzen's sequent calculus, which directly supports quantifier alternation by using eigenvariables. We shall describe deskolemization as a mapping from client-side terms, used in proofs generated by theorem provers, into kernel-side terms, used within our proof checking kernel. This mapping which associates skolemized terms to eigenvariables relies on using outer skolemization. We also point out that the removal of Skolem terms from a proof is influenced by the polarities given to propositional connectives.
@InProceedings{CPP19p78,
author = {Kaustuv Chaudhuri and Matteo Manighetti and Dale Miller},
title = {A Proof-Theoretic Approach to Certifying Skolemization},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {78--90},
doi = {10.1145/3293880.3294094},
year = {2019},
}
Publisher's Version
CPP '19: "Counting Polynomial Roots ..."
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
Wenda Li and Lawrence C. Paulson
(University of Cambridge, UK)
Many problems in computer algebra and numerical analysis can be reduced to counting or approximating the real roots of a polynomial within an interval. Existing verified root-counting procedures in major proof assistants are mainly based on the classical Sturm theorem, which only counts distinct roots.
In this paper, we have strengthened the root-counting ability in Isabelle/HOL by first formally proving the Budan-Fourier theorem. Subsequently, based on Descartes' rule of signs and Taylor shift, we have provided a verified procedure to efficiently over-approximate the number of real roots within an interval, counting multiplicity. For counting multiple roots exactly, we have extended our previous formalisation of Sturm's theorem. Finally, we combine verified components in the developments above to improve our previous certified complex-root-counting procedures based on Cauchy indices. We believe those verified routines will be crucial for certifying programs and building tactics.
@InProceedings{CPP19p52,
author = {Wenda Li and Lawrence C. Paulson},
title = {Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {52--64},
doi = {10.1145/3293880.3294092},
year = {2019},
}
Publisher's Version
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by low-level buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement.
@InProceedings{CPP19p234,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {234--248},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
CPP '19: "A Verified Ground Confluence ..."
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp
(University of Innsbruck, Austria; Allgemeines Rechenzentrum Innsbruck, Austria)
It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variable-separated rewrite systems. To this end, we formalize procedures for ground tree transducers and so-called RRn relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the first-order theory of ground rewriting for linear, variable-separated rewrite systems. It forms the basis for a formalized confluence checker for left-linear, right-ground systems.
@InProceedings{CPP19p132,
author = {Bertram Felgenhauer and Aart Middeldorp and T. V. H. Prathamesh and Franziska Rapp},
title = {A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {132--143},
doi = {10.1145/3293880.3294098},
year = {2019},
}
Publisher's Version
CPP '19: "A Verified Ground Confluence ..."
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp
(University of Innsbruck, Austria; Allgemeines Rechenzentrum Innsbruck, Austria)
It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variable-separated rewrite systems. To this end, we formalize procedures for ground tree transducers and so-called RRn relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the first-order theory of ground rewriting for linear, variable-separated rewrite systems. It forms the basis for a formalized confluence checker for left-linear, right-ground systems.
@InProceedings{CPP19p132,
author = {Bertram Felgenhauer and Aart Middeldorp and T. V. H. Prathamesh and Franziska Rapp},
title = {A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {132--143},
doi = {10.1145/3293880.3294098},
year = {2019},
}
Publisher's Version
CPP '19: "Formally Verified Big Step ..."
Formally Verified Big Step Semantics out of x86-64 Binaries
Ian Roessle, Freek Verbeek, and Binoy Ravindran
(Virginia Tech, USA)
This paper presents a methodology for generating formally proven equivalence theorems between decompiled x86-64 machine code and big step semantics. These proofs are built on top of two additional contributions. First, a robust and tested formal x86-64 machine model containing small step semantics for 1625 instructions. Second, a decompilation-into-logic methodology supporting both x86-64 assembly and machine code at large scale. This work enables black-box binary verification, i.e., formal verification of a binary where source code is unavailable. As such, it can be applied to safety-critical systems that consist of legacy components, or components whose source code is unavailable due to proprietary reasons. The methodology minimizes the trusted code base by leveraging machine-learned semantics to build a formal machine model. We apply the methodology to several case studies, including binaries that heavily rely on the SSE2 floating-point instruction set, and binaries that are obtained by compiling code that is obtained by inlining assembly into C code.
@InProceedings{CPP19p181,
author = {Ian Roessle and Freek Verbeek and Binoy Ravindran},
title = {Formally Verified Big Step Semantics out of x86-64 Binaries},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {181--195},
doi = {10.1145/3293880.3294102},
year = {2019},
}
Publisher's Version
CPP '19: "Formally Verified Big Step ..."
Formally Verified Big Step Semantics out of x86-64 Binaries
Ian Roessle, Freek Verbeek, and Binoy Ravindran
(Virginia Tech, USA)
This paper presents a methodology for generating formally proven equivalence theorems between decompiled x86-64 machine code and big step semantics. These proofs are built on top of two additional contributions. First, a robust and tested formal x86-64 machine model containing small step semantics for 1625 instructions. Second, a decompilation-into-logic methodology supporting both x86-64 assembly and machine code at large scale. This work enables black-box binary verification, i.e., formal verification of a binary where source code is unavailable. As such, it can be applied to safety-critical systems that consist of legacy components, or components whose source code is unavailable due to proprietary reasons. The methodology minimizes the trusted code base by leveraging machine-learned semantics to build a formal machine model. We apply the methodology to several case studies, including binaries that heavily rely on the SSE2 floating-point instruction set, and binaries that are obtained by compiling code that is obtained by inlining assembly into C code.
@InProceedings{CPP19p181,
author = {Ian Roessle and Freek Verbeek and Binoy Ravindran},
title = {Formally Verified Big Step Semantics out of x86-64 Binaries},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {181--195},
doi = {10.1145/3293880.3294102},
year = {2019},
}
Publisher's Version
CPP '19: "Call-By-Push-Value in Coq: ..."
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark
(Saarland University, Germany)
Call-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) CBPV, define its equational theory, and verify adequacy for the standard set/algebra denotational semantics. Furthermore, we prove normalisation of the standard reduction, confluence of strong reduction, strong normalisation using Kripke logical relations, and soundness of the equational theory using logical equivalence. We adapt and verify the known translations from CBV and CBN into CBPV for strong reduction. This yields, for instance, proofs of strong normalisation and confluence for the full λ-calculus with sums and products. Thanks to the automation provided by Coq and the Autosubst 2 framework, there is little formalisation overhead compared to detailed paper proofs.
@InProceedings{CPP19p118,
author = {Yannick Forster and Steven Schäfer and Simon Spies and Kathrin Stark},
title = {Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {118--131},
doi = {10.1145/3293880.3294097},
year = {2019},
}
Publisher's Version
Info
CPP '19: "Autosubst 2: Reasoning with ..."
Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions
Kathrin Stark, Steven Schäfer, and Jonas Kaiser
(Saarland University, Germany)
Formalising metatheory in the Coq proof assistant is tedious as reasoning with binders without native support requires a lot of uninteresting technicalities. To relieve users from so-produced boilerplate, the Autosubst framework automates working with de Bruijn terms: For each annotated inductive type, Autosubst generates a corresponding instantiation operation for parallel substitutions and a decision procedure for assumption-free substitution lemmas. However, Autosubst is implemented in Ltac, Coq's tactic language, and thus suffers from Ltac's limitations. In particular, Autosubst is restricted to Coq and unscoped, non-mutual inductive types with a single sort of variables. In this paper, we present a new version of Autosubst that overcomes these restrictions. Autosubst 2 is an external code generator, which translates second-order HOAS specifications into potentially mutual inductive term sorts. We extend the equational theory of Autosubst to the case of mutual inductive sorts by combining the application of multiple parallel substitutions into exactly one instantiation operation for each sort, i.e. we parallelise substitutions to vector substitutions. The resulting equational theory is both simpler and more expressive than that of the original Autosubst framework and allows us to present an even more elegant proof of part A of the POPLMark challenge.
@InProceedings{CPP19p166,
author = {Kathrin Stark and Steven Schäfer and Jonas Kaiser},
title = {Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {166--180},
doi = {10.1145/3293880.3294101},
year = {2019},
}
Publisher's Version
Info
CPP '19: "A Verified Prover Based on ..."
A Verified Prover Based on Ordered Resolution
Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel
(DTU, Denmark; Vrije Universiteit Amsterdam, Netherlands; ETH Zurich, Switzerland)
The superposition calculus, which underlies first-order theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional first-order ordered resolution prover and establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract nondeterministic specification, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for first-order logic.
@InProceedings{CPP19p152,
author = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel},
title = {A Verified Prover Based on Ordered Resolution},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {152--165},
doi = {10.1145/3293880.3294100},
year = {2019},
}
Publisher's Version
CPP '19: "On Synthetic Undecidability ..."
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Yannick Forster, Dominik Kirst, and Gert Smolka
(Saarland University, Germany)
We formalise the computational undecidability of validity, satisfiability, and provability of first-order formulas following a synthetic approach based on the computation native to Coq's constructive type theory. Concretely, we consider Tarski and Kripke semantics as well as classical and intuitionistic natural deduction systems and provide compact many-one reductions from the Post correspondence problem (PCP). Moreover, developing a basic framework for synthetic computability theory in Coq, we formalise standard results concerning decidability, enumerability, and reducibility without reference to a concrete model of computation. For instance, we prove the equivalence of Post's theorem with Markov's principle and provide a convenient technique for establishing the enumerability of inductive predicates such as the considered proof systems and PCP.
@InProceedings{CPP19p38,
author = {Yannick Forster and Dominik Kirst and Gert Smolka},
title = {On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {38--51},
doi = {10.1145/3293880.3294091},
year = {2019},
}
Publisher's Version
Info
CPP '19: "Eliminating Reflection from ..."
Eliminating Reflection from Type Theory
Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France)
Type theories with equality reflection, such as extensional type theory (ETT), are convenient theories in which to formalise mathematics, as they make it possible to consider provably equal terms as convertible. Although type-checking is undecidable in this context, variants of ETT have been implemented, for example in NuPRL and more recently in Andromeda.
The actual objects that can be checked are not proof-terms, but derivations of proof-terms. This suggests that any derivation of ETT can be translated into a typecheckable proof term of intensional type theory (ITT).
However, this result, investigated categorically by Hofmann in 1995, and 10 years later more syntactically by Oury, has never given rise to an effective translation.
In this paper, we provide the first effective syntactical translation from ETT to ITT with uniqueness of identity proofs and functional extensionality. This translation has been defined and proven correct in Coq and yields an executable plugin that translates a derivation in ETT into an actual Coq typing judgment. Additionally, we show how this result is extended in the context of homotopy type theory to a two-level type theory.
@InProceedings{CPP19p91,
author = {Théo Winterhalter and Matthieu Sozeau and Nicolas Tabareau},
title = {Eliminating Reflection from Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {91--103},
doi = {10.1145/3293880.3294095},
year = {2019},
}
Publisher's Version
CPP '19: "Call-By-Push-Value in Coq: ..."
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark
(Saarland University, Germany)
Call-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) CBPV, define its equational theory, and verify adequacy for the standard set/algebra denotational semantics. Furthermore, we prove normalisation of the standard reduction, confluence of strong reduction, strong normalisation using Kripke logical relations, and soundness of the equational theory using logical equivalence. We adapt and verify the known translations from CBV and CBN into CBPV for strong reduction. This yields, for instance, proofs of strong normalisation and confluence for the full λ-calculus with sums and products. Thanks to the automation provided by Coq and the Autosubst 2 framework, there is little formalisation overhead compared to detailed paper proofs.
@InProceedings{CPP19p118,
author = {Yannick Forster and Steven Schäfer and Simon Spies and Kathrin Stark},
title = {Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {118--131},
doi = {10.1145/3293880.3294097},
year = {2019},
}
Publisher's Version
Info
CPP '19: "Call-By-Push-Value in Coq: ..."
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark
(Saarland University, Germany)
Call-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) CBPV, define its equational theory, and verify adequacy for the standard set/algebra denotational semantics. Furthermore, we prove normalisation of the standard reduction, confluence of strong reduction, strong normalisation using Kripke logical relations, and soundness of the equational theory using logical equivalence. We adapt and verify the known translations from CBV and CBN into CBPV for strong reduction. This yields, for instance, proofs of strong normalisation and confluence for the full λ-calculus with sums and products. Thanks to the automation provided by Coq and the Autosubst 2 framework, there is little formalisation overhead compared to detailed paper proofs.
@InProceedings{CPP19p118,
author = {Yannick Forster and Steven Schäfer and Simon Spies and Kathrin Stark},
title = {Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {118--131},
doi = {10.1145/3293880.3294097},
year = {2019},
}
Publisher's Version
Info
CPP '19: "Autosubst 2: Reasoning with ..."
Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions
Kathrin Stark, Steven Schäfer, and Jonas Kaiser
(Saarland University, Germany)
Formalising metatheory in the Coq proof assistant is tedious as reasoning with binders without native support requires a lot of uninteresting technicalities. To relieve users from so-produced boilerplate, the Autosubst framework automates working with de Bruijn terms: For each annotated inductive type, Autosubst generates a corresponding instantiation operation for parallel substitutions and a decision procedure for assumption-free substitution lemmas. However, Autosubst is implemented in Ltac, Coq's tactic language, and thus suffers from Ltac's limitations. In particular, Autosubst is restricted to Coq and unscoped, non-mutual inductive types with a single sort of variables. In this paper, we present a new version of Autosubst that overcomes these restrictions. Autosubst 2 is an external code generator, which translates second-order HOAS specifications into potentially mutual inductive term sorts. We extend the equational theory of Autosubst to the case of mutual inductive sorts by combining the application of multiple parallel substitutions into exactly one instantiation operation for each sort, i.e. we parallelise substitutions to vector substitutions. The resulting equational theory is both simpler and more expressive than that of the original Autosubst framework and allows us to present an even more elegant proof of part A of the POPLMark challenge.
@InProceedings{CPP19p166,
author = {Kathrin Stark and Steven Schäfer and Jonas Kaiser},
title = {Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {166--180},
doi = {10.1145/3293880.3294101},
year = {2019},
}
Publisher's Version
Info
CPP '19: "Certified ACKBO ..."
Certified ACKBO
Alexander Lochmann and Christian Sternagel
(University of Innsbruck, Austria)
Term rewriting in the presence of associative and commutative function symbols constitutes a highly expressive model of computation, which is for example well suited to reason about parallel computations. However, it is well known that the standard notion of termination does not apply any more: any term rewrite system containing a commutativity rule is nonterminating. Thus, instead of adding AC-rules to a rewrite system, we switch to the notion of AC-termination. AC-termination can for example be shown using AC-compatible reduction orders. One specific example of such an order is ACKBO. We present our Isabelle/HOL formalization of the ACKBO order. On an abstract level this gives us a mechanized proof of the fact that ACKBO is indeed an AC-compatible reduction order. Moreover, we integrated corresponding check functions into the verified certifier CeTA. This has the more practical consequence of enabling the machine certification of AC-termination proofs generated by automated termination tools.
@InProceedings{CPP19p144,
author = {Alexander Lochmann and Christian Sternagel},
title = {Certified ACKBO},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {144--151},
doi = {10.1145/3293880.3294099},
year = {2019},
}
Publisher's Version
CPP '19: "Eliminating Reflection from ..."
Eliminating Reflection from Type Theory
Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France)
Type theories with equality reflection, such as extensional type theory (ETT), are convenient theories in which to formalise mathematics, as they make it possible to consider provably equal terms as convertible. Although type-checking is undecidable in this context, variants of ETT have been implemented, for example in NuPRL and more recently in Andromeda.
The actual objects that can be checked are not proof-terms, but derivations of proof-terms. This suggests that any derivation of ETT can be translated into a typecheckable proof term of intensional type theory (ITT).
However, this result, investigated categorically by Hofmann in 1995, and 10 years later more syntactically by Oury, has never given rise to an effective translation.
In this paper, we provide the first effective syntactical translation from ETT to ITT with uniqueness of identity proofs and functional extensionality. This translation has been defined and proven correct in Coq and yields an executable plugin that translates a derivation in ETT into an actual Coq typing judgment. Additionally, we show how this result is extended in the context of homotopy type theory to a two-level type theory.
@InProceedings{CPP19p91,
author = {Théo Winterhalter and Matthieu Sozeau and Nicolas Tabareau},
title = {Eliminating Reflection from Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {91--103},
doi = {10.1145/3293880.3294095},
year = {2019},
}
Publisher's Version
CPP '19: "A Verified Prover Based on ..."
A Verified Prover Based on Ordered Resolution
Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel
(DTU, Denmark; Vrije Universiteit Amsterdam, Netherlands; ETH Zurich, Switzerland)
The superposition calculus, which underlies first-order theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional first-order ordered resolution prover and establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract nondeterministic specification, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for first-order logic.
@InProceedings{CPP19p152,
author = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel},
title = {A Verified Prover Based on Ordered Resolution},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {152--165},
doi = {10.1145/3293880.3294100},
year = {2019},
}
Publisher's Version
CPP '19: "Formally Verified Big Step ..."
Formally Verified Big Step Semantics out of x86-64 Binaries
Ian Roessle, Freek Verbeek, and Binoy Ravindran
(Virginia Tech, USA)
This paper presents a methodology for generating formally proven equivalence theorems between decompiled x86-64 machine code and big step semantics. These proofs are built on top of two additional contributions. First, a robust and tested formal x86-64 machine model containing small step semantics for 1625 instructions. Second, a decompilation-into-logic methodology supporting both x86-64 assembly and machine code at large scale. This work enables black-box binary verification, i.e., formal verification of a binary where source code is unavailable. As such, it can be applied to safety-critical systems that consist of legacy components, or components whose source code is unavailable due to proprietary reasons. The methodology minimizes the trusted code base by leveraging machine-learned semantics to build a formal machine model. We apply the methodology to several case studies, including binaries that heavily rely on the SSE2 floating-point instruction set, and binaries that are obtained by compiling code that is obtained by inlining assembly into C code.
@InProceedings{CPP19p181,
author = {Ian Roessle and Freek Verbeek and Binoy Ravindran},
title = {Formally Verified Big Step Semantics out of x86-64 Binaries},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {181--195},
doi = {10.1145/3293880.3294102},
year = {2019},
}
Publisher's Version
CPP '19: "Eliminating Reflection from ..."
Eliminating Reflection from Type Theory
Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France)
Type theories with equality reflection, such as extensional type theory (ETT), are convenient theories in which to formalise mathematics, as they make it possible to consider provably equal terms as convertible. Although type-checking is undecidable in this context, variants of ETT have been implemented, for example in NuPRL and more recently in Andromeda.
The actual objects that can be checked are not proof-terms, but derivations of proof-terms. This suggests that any derivation of ETT can be translated into a typecheckable proof term of intensional type theory (ITT).
However, this result, investigated categorically by Hofmann in 1995, and 10 years later more syntactically by Oury, has never given rise to an effective translation.
In this paper, we provide the first effective syntactical translation from ETT to ITT with uniqueness of identity proofs and functional extensionality. This translation has been defined and proven correct in Coq and yields an executable plugin that translates a derivation in ETT into an actual Coq typing judgment. Additionally, we show how this result is extended in the context of homotopy type theory to a two-level type theory.
@InProceedings{CPP19p91,
author = {Théo Winterhalter and Matthieu Sozeau and Nicolas Tabareau},
title = {Eliminating Reflection from Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {91--103},
doi = {10.1145/3293880.3294095},
year = {2019},
}
Publisher's Version
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by low-level buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement.
@InProceedings{CPP19p234,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {234--248},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
CPP '19: "A Verified Protocol Buffer ..."
A Verified Protocol Buffer Compiler
Qianchuan Ye and Benjamin Delaware
(Purdue University, USA)
The code responsible for serializing and deserializing untrusted external data is a vital component of any software that communicates with the outside world, as any bugs in these components can compromise the entire system. This is particularly true for verified systems which rely on trusted code to process external data, as any defects in the parsing code can invalidate any formal proofs about the system. One way to reduce the trusted code base of these systems is to use interface generators like Protocol Buffer and ASN.1 to generate serializers and deserializers from data descriptors. Of course, these generators are not immune to bugs.
In this work, we formally verify a compiler for a realistic subset of the popular Protocol Buffer serialization format using the Coq proof assistant, proving once and for all the correctness of every generated serializer and deserializer. One of the challenges we had to overcome was the extreme flexibility of the Protocol Buffer format: the same source data can be encoded in an infinite number of ways, and the deserializer must faithfully recover the original source value from each. We have validated our verified system using the official conformance tests.
@InProceedings{CPP19p222,
author = {Qianchuan Ye and Benjamin Delaware},
title = {A Verified Protocol Buffer Compiler},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {222--233},
doi = {10.1145/3293880.3294105},
year = {2019},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by low-level buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement.
@InProceedings{CPP19p234,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {234--248},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
CPP '19: "Smooth Manifolds and Types ..."
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
Fabian Immler and Bohua Zhan
(Carnegie Mellon University, USA; Institute of Software at Chinese Academy of Sciences, China)
We formalize the definition and basic properties of smooth manifolds in Isabelle/HOL. Concepts covered include partition of unity, tangent and cotangent spaces, and the fundamental theorem for line integrals. We also construct some concrete manifolds such as spheres and projective spaces. The formalization makes extensive use of the existing libraries for topology and analysis. The existing library for linear algebra is not flexible enough for our needs. We therefore set up the first systematic and large scale application of ``types to sets''. It allows us to automatically transform the existing (type based) library of linear algebra to one with explicit carrier sets.
@InProceedings{CPP19p65,
author = {Fabian Immler and Bohua Zhan},
title = {Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {65--77},
doi = {10.1145/3293880.3294093},
year = {2019},
}
Publisher's Version