CPP 2016 – Author Index 
Contents 
Abstracts 
Authors

A B C D E F K L M P R S T U V W Y
Åman Pohjola, Johannes 
CPP '16: "Bisimulation UpTo Techniques ..."
Bisimulation UpTo Techniques for PsiCalculi
Johannes Åman Pohjola and Joachim Parrow (Uppsala University, Sweden)
Psicalculi is a parametric framework for process calculi similar to popular picalculus extensions such as the explicit fusion calculus, the applied picalculus and the spi calculus. Remarkably, machinechecked proofs of standard algebraic and congruence properties of bisimilarity apply to all calculi within the framework. Bisimulation upto techniques are methods for reducing the size of relations needed in bisimulation proofs. In this paper, we show how these bisimulation proof methods can be adapted to psicalculi. We formalise all our definitions and theorems in Nominal Isabelle, and show examples where the use of up totechniques yields drastically simplified proofs of known results. We also prove new structural laws about the replication operator.
@InProceedings{CPP16p142,
author = {Johannes Åman Pohjola and Joachim Parrow},
title = {Bisimulation UpTo Techniques for PsiCalculi},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {142153},
doi = {10.1145/2854065.2854080},
year = {2016},
}
Publisher's Version
Article Search


Anderson, Thomas 
CPP '16: "Planning for Change in a Formal ..."
Planning for Change in a Formal Verification of the Raft Consensus Protocol
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson (University of Washington, USA)
We present the first formal verification of state machine safety for the Raft consensus protocol, a critical component of many distributed systems. We connected our proof to previous work to establish an endtoend guarantee that our implementation provides linearizable state machine replication. This proof required iteratively discovering and proving 90 system invariants. Our verified implementation is extracted to OCaml and runs on real networks.
The primary challenge we faced during the verification process was proof maintenance, since proving one invariant often required strengthening and updating other parts of our proof. To address this challenge, we propose a methodology of planning for change during verification. Our methodology adapts classical information hiding techniques to the context of proof assistants, factors out common invariantstrengthening patterns into custom induction principles, proves higherorder lemmas that show any property proved about a particular component implies analogous properties about related components, and makes proofs robust to change using structural tactics. We also discuss how our methodology may be applied to systems verification more broadly.
@InProceedings{CPP16p154,
author = {Doug Woos and James R. Wilcox and Steve Anton and Zachary Tatlock and Michael D. Ernst and Thomas Anderson},
title = {Planning for Change in a Formal Verification of the Raft Consensus Protocol},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {154165},
doi = {10.1145/2854065.2854081},
year = {2016},
}
Publisher's Version
Article Search


Anton, Steve 
CPP '16: "Planning for Change in a Formal ..."
Planning for Change in a Formal Verification of the Raft Consensus Protocol
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson (University of Washington, USA)
We present the first formal verification of state machine safety for the Raft consensus protocol, a critical component of many distributed systems. We connected our proof to previous work to establish an endtoend guarantee that our implementation provides linearizable state machine replication. This proof required iteratively discovering and proving 90 system invariants. Our verified implementation is extracted to OCaml and runs on real networks.
The primary challenge we faced during the verification process was proof maintenance, since proving one invariant often required strengthening and updating other parts of our proof. To address this challenge, we propose a methodology of planning for change during verification. Our methodology adapts classical information hiding techniques to the context of proof assistants, factors out common invariantstrengthening patterns into custom induction principles, proves higherorder lemmas that show any property proved about a particular component implies analogous properties about related components, and makes proofs robust to change using structural tactics. We also discuss how our methodology may be applied to systems verification more broadly.
@InProceedings{CPP16p154,
author = {Doug Woos and James R. Wilcox and Steve Anton and Zachary Tatlock and Michael D. Ernst and Thomas Anderson},
title = {Planning for Change in a Formal Verification of the Raft Consensus Protocol},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {154165},
doi = {10.1145/2854065.2854081},
year = {2016},
}
Publisher's Version
Article Search


Bernard, Sophie 
CPP '16: "Formal Proofs of Transcendence ..."
Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials
Sophie Bernard, Yves Bertot, Laurence Rideau, and PierreYves Strub (Inria, France; IMDEA Software Institute, Spain)
We describe the formalisation in Coq of a proof that the numbers `e` and `pi` are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreover, some of the elements of our formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of `pi` relies extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials.
@InProceedings{CPP16p76,
author = {Sophie Bernard and Yves Bertot and Laurence Rideau and PierreYves Strub},
title = {Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {7687},
doi = {10.1145/2854065.2854072},
year = {2016},
}
Publisher's Version
Article Search


Bertot, Yves 
CPP '16: "Formal Proofs of Transcendence ..."
Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials
Sophie Bernard, Yves Bertot, Laurence Rideau, and PierreYves Strub (Inria, France; IMDEA Software Institute, Spain)
We describe the formalisation in Coq of a proof that the numbers `e` and `pi` are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreover, some of the elements of our formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of `pi` relies extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials.
@InProceedings{CPP16p76,
author = {Sophie Bernard and Yves Bertot and Laurence Rideau and PierreYves Strub},
title = {Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {7687},
doi = {10.1145/2854065.2854072},
year = {2016},
}
Publisher's Version
Article Search


Bickford, Mark 
CPP '16: "A Nominal Exploration of Intuitionism ..."
A Nominal Exploration of Intuitionism
Vincent Rahli and Mark Bickford (University of Luxembourg, Luxembourg; Cornell University, USA)
This papers extends the Nuprl proof assistant (a system representative
of the class of extensional type theories a la MartinLof) with
named exceptions and handlers, as well as a nominal
fresh operator. Using these new features, we prove a version
of Brouwer's Continuity Principle for numbers. We also provide a
simpler proof of a weaker version of this principle that only uses
diverging terms. We prove these two principles in Nuprl's metatheory
using our formalization of Nuprl in Coq and show how we can reflect
these metatheoretical results in the Nuprl theory as derivation
rules. We also show that these additions preserve Nuprl's key
metatheoretical properties, in particular consistency and the
congruence of Howe's computational equivalence relation. Using
continuity and the fan theorem we prove important results of
Intuitionistic Mathematics: Brouwer's continuity theorem and bar
induction on monotone bars.
@InProceedings{CPP16p130,
author = {Vincent Rahli and Mark Bickford},
title = {A Nominal Exploration of Intuitionism},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {130141},
doi = {10.1145/2854065.2854077},
year = {2016},
}
Publisher's Version
Article Search


Blazy, Sandrine 
CPP '16: "Formal Verification of ControlFlow ..."
Formal Verification of ControlFlow Graph Flattening
Sandrine Blazy and Alix Trieu (IRISA, France; Université Rennes 1, France; ENS Rennes, France)
Code obfuscation is emerging as a key asset in security by obscurity. It aims at hiding sensitive information in programs so that they become more difficult to understand and reverse engineer. Since the results on the impossibility of perfect and universal obfuscation, many obfuscation techniques have been proposed in the literature, ranging from simple variable encoding to hiding the controlflow of a program. In this paper, we formally verify in Coq an advanced code obfuscation called controlflow graph flattening, that is used in stateoftheart program obfuscators. Our controlflow graph flattening is a program transformation operating over C programs, that is integrated into the CompCert formally verified compiler. The semantics preservation proof of our program obfuscator relies on a simulation proof performed on a realistic language, the Clight language of CompCert. The automatic extraction of our program obfuscator into OCaml yields a program with competitive results.
@InProceedings{CPP16p176,
author = {Sandrine Blazy and Alix Trieu},
title = {Formal Verification of ControlFlow Graph Flattening},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {176187},
doi = {10.1145/2854065.2854082},
year = {2016},
}
Publisher's Version
Article Search
Info


Charguéraud, Arthur 
CPP '16: "HigherOrder Representation ..."
HigherOrder Representation Predicates in Separation Logic
Arthur Charguéraud (Inria, France)
In Separation Logic, representation predicates are used to describe mutable data structures, by establishing a relationship between the entry point of the structure, the piece of heap over which this structure spans, and the logical model associated with the structure. When a data structure is polymorphic, such as in the case of a container, its representation predicate needs to be parameterized not just by the type of the items stored in the structure, but also by the representation predicates associated with these items. Such higherorder representation predicates can be used in particular to control whether containers should own their items. In this paper, we present, through a collection of practical examples, solutions to the challenges associated with reasoning about accesses into data structures that own their elements.
@InProceedings{CPP16p3,
author = {Arthur Charguéraud},
title = {HigherOrder Representation Predicates in Separation Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {314},
doi = {10.1145/2854065.2854068},
year = {2016},
}
Publisher's Version
Article Search


Cohen, Cyril 
CPP '16: "Formalization of a Newton ..."
Formalization of a Newton Series Representation of Polynomials
Cyril Cohen and Boris Djalal (Inria, France)
We formalize an algorithm to change the representation of a poly nomial to a Newton power series. This provides a way to compute efficiently polynomials whose roots are the sums or products of roots of other polynomials, and hence provides a base component of efficient computation for algebraic numbers. In order to achieve this, we formalize a notion of truncated power series and develop an abstract theory of poles of fractions.
@InProceedings{CPP16p100,
author = {Cyril Cohen and Boris Djalal},
title = {Formalization of a Newton Series Representation of Polynomials},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {100109},
doi = {10.1145/2854065.2854075},
year = {2016},
}
Publisher's Version
Article Search
Info


Czajka, Łukasz 
CPP '16: "Improving Automation in Interactive ..."
Improving Automation in Interactive Theorem Provers by Efficient Encoding of LambdaAbstractions
Łukasz Czajka (University of Innsbruck, Austria)
Hammers are tools for employing external automated theorem provers (ATPs) to improve automation in formal proof assistants. Strong automation can greatly ease the task of developing formal proofs. An essential component of any hammer is the translation of the logic of a proof assistant to the format of an ATP. For malisms of stateoftheart ATPs are usually firstorder, so some method for eliminating lambdaabstractions is needed. We present an experimental comparison of several combinatory abstraction al gorithms for HOL(y)Hammer – a hammer for HOL Light. The al gorithms are compared on problems involving nontrivial lambda abstractions selected from the HOL Light core library and a library for multivariate analysis. We succeeded in developing algorithms which outperform both lambdalifting and the simple Scho ̈nfinkel’s algorithm used in Sledgehammer for Isabelle/HOL. This increases the ATPs’ success rate on translated problems, thus enhancing au tomation in proof assistants.
@InProceedings{CPP16p49,
author = {Łukasz Czajka},
title = {Improving Automation in Interactive Theorem Provers by Efficient Encoding of LambdaAbstractions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {4957},
doi = {10.1145/2854065.2854069},
year = {2016},
}
Publisher's Version
Article Search


De Moura, Leonardo 
CPP '16KEY: "Dependent Type Practice (Invited ..."
Dependent Type Practice (Invited Talk)
Leonardo de Moura (Microsoft Research, USA)
Dependent type theory is a powerful and expressive language for writing mathematical expressions and proofs, but careful design, engineering, and hard work are needed to put the theory into practice. In this talk, I will discuss some of the ideas and techniques that have been used in the design of the Lean theorem prover, a new proof system based on dependent type theory that aims to make the theorem proving process more natural, convenient, and efficient.
@InProceedings{CPP16p2,
author = {Leonardo de Moura},
title = {Dependent Type Practice (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {22},
doi = {10.1145/2854065.2858809},
year = {2016},
}
Publisher's Version
Article Search


Djalal, Boris 
CPP '16: "Formalization of a Newton ..."
Formalization of a Newton Series Representation of Polynomials
Cyril Cohen and Boris Djalal (Inria, France)
We formalize an algorithm to change the representation of a poly nomial to a Newton power series. This provides a way to compute efficiently polynomials whose roots are the sums or products of roots of other polynomials, and hence provides a base component of efficient computation for algebraic numbers. In order to achieve this, we formalize a notion of truncated power series and develop an abstract theory of poles of fractions.
@InProceedings{CPP16p100,
author = {Cyril Cohen and Boris Djalal},
title = {Formalization of a Newton Series Representation of Polynomials},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {100109},
doi = {10.1145/2854065.2854075},
year = {2016},
}
Publisher's Version
Article Search
Info


Doorn, Floris van 
CPP '16: "Constructing the Propositional ..."
Constructing the Propositional Truncation using Nonrecursive HITs
Floris van Doorn (Carnegie Mellon University, USA)
In homotopy type theory, we construct the propositional truncation as a colimit, using only nonrecursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to nonrecursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all the results in a new proof assistant, Lean.
@InProceedings{CPP16p122,
author = {Floris van Doorn},
title = {Constructing the Propositional Truncation using Nonrecursive HITs},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {122129},
doi = {10.1145/2854065.2854076},
year = {2016},
}
Publisher's Version
Article Search


Ernst, Michael D. 
CPP '16: "Planning for Change in a Formal ..."
Planning for Change in a Formal Verification of the Raft Consensus Protocol
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson (University of Washington, USA)
We present the first formal verification of state machine safety for the Raft consensus protocol, a critical component of many distributed systems. We connected our proof to previous work to establish an endtoend guarantee that our implementation provides linearizable state machine replication. This proof required iteratively discovering and proving 90 system invariants. Our verified implementation is extracted to OCaml and runs on real networks.
The primary challenge we faced during the verification process was proof maintenance, since proving one invariant often required strengthening and updating other parts of our proof. To address this challenge, we propose a methodology of planning for change during verification. Our methodology adapts classical information hiding techniques to the context of proof assistants, factors out common invariantstrengthening patterns into custom induction principles, proves higherorder lemmas that show any property proved about a particular component implies analogous properties about related components, and makes proofs robust to change using structural tactics. We also discuss how our methodology may be applied to systems verification more broadly.
@InProceedings{CPP16p154,
author = {Doug Woos and James R. Wilcox and Steve Anton and Zachary Tatlock and Michael D. Ernst and Thomas Anderson},
title = {Planning for Change in a Formal Verification of the Raft Consensus Protocol},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {154165},
doi = {10.1145/2854065.2854081},
year = {2016},
}
Publisher's Version
Article Search


Felty, Amy P. 
CPP '16: "A Verified Algorithm for Detecting ..."
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
Michel StMartin and Amy P. Felty (University of Ottawa, Canada)
We describe the formalization of a correctness proof for a conflict
detection algorithm for XACML (eXtensible Access Control Markup
Language). XACML is a standardized declarative access control
policy language that is increasingly used in industry. In practice it is
common for rule sets to grow large, and contain unintended errors,
often due to conflicting rules. A conflict occurs in a policy when one
rule permits a request and another denies that same request. Such
errors can lead to serious risks involving both allowing access to an
unauthorized user as well as denying access to someone who needs
it. Removing conflicts is thus an important aspect of debugging
policies, and the use of a verified algorithm provides the highest
assurance in a domain where security is important. In this paper,
we focus on several complex XACML constructs, including time
ranges and integer intervals, as well as ways to combine any number
of functions using the boolean operators and, or, and not. The latter
are the most complex, and add significant expressive power to the
language. We propose an algorithm to find conflicts and then use
the Coq Proof Assistant to prove the algorithm correct. We develop
a library of tactics to help automate the proof.
@InProceedings{CPP16p166,
author = {Michel StMartin and Amy P. Felty},
title = {A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {166175},
doi = {10.1145/2854065.2854079},
year = {2016},
}
Publisher's Version
Article Search


Friedman, Harvey M. 
CPP '16KEY: "Perspectives on Formal Verification ..."
Perspectives on Formal Verification (Invited Talk)
Harvey M. Friedman (Ohio State University, USA)
I will discuss the importance, uses, and future directions of formal verification from the point of view of a mathematical foundationalist. These include issues of certainty, proof structure, and (finitary) completeness and decidability.
@InProceedings{CPP16p1,
author = {Harvey M. Friedman},
title = {Perspectives on Formal Verification (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {11},
doi = {10.1145/2854065.2858808},
year = {2016},
}
Publisher's Version
Article Search


Fulton, Nathan 
CPP '16: "A Logic of Proofs for Differential ..."
A Logic of Proofs for Differential Dynamic Logic: Toward Independently Checkable Proof Certificates for Dynamic Logics
Nathan Fulton and André Platzer (Carnegie Mellon University, USA)
Differential dynamic logic is a logic for specifying and verifying safety, liveness, and other properties about models of cyberphysical systems. Theorem provers based on differential dynamic logic have been used to verify safety properties for models of selfdriving cars and collision avoidance protocols for aircraft. Unfortunately, these theorem provers do not have explicit proof terms, which makes the implementation of a number of important features unnecessarily complicated without soundnesscritical and extralogical extensions to the theorem prover. Examples include: an unambiguous separation between proof checking and proof search, the ability to extract program traces corresponding to counterexamples, and synthesis of surelylive deterministic programs from liveness proofs for nondeterministic programs. This paper presents a differential dynamic logic with such an explicit representation of proofs. The resulting logic extends both the syntax and semantics of differential dynamic logic with proof terms  syntactic representations of logical deductions. To support axiomatic theorem proving, the logic allows equivalence rewriting deep within formulas and supports both uniform renaming and uniform substitutions.
@InProceedings{CPP16p110,
author = {Nathan Fulton and André Platzer},
title = {A Logic of Proofs for Differential Dynamic Logic: Toward Independently Checkable Proof Certificates for Dynamic Logics},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {110121},
doi = {10.1145/2854065.2854078},
year = {2016},
}
Publisher's Version
Article Search


Kaliszyk, Cezary 
CPP '16: "Towards a Mizar Environment ..."
Towards a Mizar Environment for Isabelle: Foundations and Language
Cezary Kaliszyk, Karol Pąk, and Josef Urban (University of Innsbruck, Austria; University of Białystok, Poland; Czech Technical University in Prague, Czech Republic)
In this paper we explore the possibility of emulating the Mizar environment as close as possible inside the Isabelle logical framework. We introduce adaptations to the Isabelle/FOL object logic that correspond to the logic of Mizar, as well as Isar inner syntax notations that correspond to these of the Mizar language. We show how Isabelle types can be used to differentiate between the syntactic categories of the Mizar language, such as sets and Mizar types including modes and attributes, and show how they interact with the basic constructs of the TarskiGrothendieck set theory. We discuss Mizar definitions and provide simple abbreviations that allow the introduction of Mizar predicates, functions, attributes and modes using the Isabelle/Pure language elements for introducing definitions and theorems. We finally consider the definite and indefinite description operators in Mizar and their use to introduce definitions by “means” and “equals”. We demonstrate the usability of the environment on a sample Mizarstyle formalization, with cluster inferences and “by” steps performed manually.
@InProceedings{CPP16p58,
author = {Cezary Kaliszyk and Karol Pąk and Josef Urban},
title = {Towards a Mizar Environment for Isabelle: Foundations and Language},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {5865},
doi = {10.1145/2854065.2854070},
year = {2016},
}
Publisher's Version
Article Search


Kotelnikov, Evgenii 
CPP '16: "The Vampire and the FOOL ..."
The Vampire and the FOOL
Evgenii Kotelnikov, Laura Kovács, Giles Reger, and Andrei Voronkov (Chalmers University of Technology, Sweden; University of Manchester, UK; EasyChair, UK)
This paper presents new features recently implemented in the theorem prover Vampire, namely support for firstorder logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also contains ifthenelse and letin expressions. We argue that presented extensions facilitate reasoningbased program analysis, both by increasing the expressivity of firstorder reasoners and by gains in efficiency.
@InProceedings{CPP16p37,
author = {Evgenii Kotelnikov and Laura Kovács and Giles Reger and Andrei Voronkov},
title = {The Vampire and the FOOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {3748},
doi = {10.1145/2854065.2854071},
year = {2016},
}
Publisher's Version
Article Search
Info


Kovács, Laura 
CPP '16: "The Vampire and the FOOL ..."
The Vampire and the FOOL
Evgenii Kotelnikov, Laura Kovács, Giles Reger, and Andrei Voronkov (Chalmers University of Technology, Sweden; University of Manchester, UK; EasyChair, UK)
This paper presents new features recently implemented in the theorem prover Vampire, namely support for firstorder logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also contains ifthenelse and letin expressions. We argue that presented extensions facilitate reasoningbased program analysis, both by increasing the expressivity of firstorder reasoners and by gains in efficiency.
@InProceedings{CPP16p37,
author = {Evgenii Kotelnikov and Laura Kovács and Giles Reger and Andrei Voronkov},
title = {The Vampire and the FOOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {3748},
doi = {10.1145/2854065.2854071},
year = {2016},
}
Publisher's Version
Article Search
Info


Lammich, Peter 
CPP '16: "Refinement Based Verification ..."
Refinement Based Verification of Imperative Data Structures
Peter Lammich (TU München, Germany)
In this paper we present a stepwise refinement based topdown approach to verified imperative data structures. Our approach is modular in the sense that already verified data structures can be used for construction of more complex data structures. Moreover, our data structures can be used as building blocks for the verification of algorithms. Our tool chain supports refinement down to executable code in various programming languages, and is fully implemented in Isabelle/HOL, such that its trusted code base is only the inference kernel and the code generator of Isabelle/HOL. As a case study, we verify an indexed heap data structure, and use it to generate an efficient verified implementation of Dijkstra's algorithm.
@InProceedings{CPP16p27,
author = {Peter Lammich},
title = {Refinement Based Verification of Imperative Data Structures},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {2736},
doi = {10.1145/2854065.2854067},
year = {2016},
}
Publisher's Version
Article Search


Lethin, Richard 
CPP '16: "A Unified Coq Framework for ..."
A Unified Coq Framework for Verifying C Programs with FloatingPoint Computations
Tahina Ramananandro, Paul Mountcastle, Benoît Meister, and Richard Lethin (Reservoir Labs, USA)
We provide concrete evidence that floatingpoint computations in C programs can be verified in a homogeneous verification setting based on Coq only, by evaluating the practicality of the combination of the formal semantics of CompCert Clight and the Flocq formal specification of IEEE 754 floatingpoint arithmetic for the verification of properties of floatingpoint computations in C programs. To this end, we develop a framework to automatically compute realnumber expressions of C floatingpoint computations with rounding error terms along with their correctness proofs. We apply our framework to the complete analysis of an energyefficient C implementation of a radar image processing algorithm, for which we provide a certified bound on the total noise introduced by floatingpoint rounding errors and energyefficient approximations of square root and sine.
@InProceedings{CPP16p15,
author = {Tahina Ramananandro and Paul Mountcastle and Benoît Meister and Richard Lethin},
title = {A Unified Coq Framework for Verifying C Programs with FloatingPoint Computations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1526},
doi = {10.1145/2854065.2854066},
year = {2016},
}
Publisher's Version
Article Search


Li, Wenda 
CPP '16: "A Modular, Efficient Formalisation ..."
A Modular, Efficient Formalisation of Real Algebraic Numbers
Wenda Li and Lawrence C. Paulson (University of Cambridge, UK)
This paper presents a construction of the real algebraic numbers with executable arithmetic operations in Isabelle/HOL. Instead of verified resultants, arithmetic operations on real algebraic numbers are based on a decision procedure to decide the sign of a bivariate polynomial (with rational coefficients) at a real algebraic point. The modular design allows the safe use of fast external code. This work can be the basis for decision procedures that rely on real algebraic numbers.
@InProceedings{CPP16p66,
author = {Wenda Li and Lawrence C. Paulson},
title = {A Modular, Efficient Formalisation of Real Algebraic Numbers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {6675},
doi = {10.1145/2854065.2854074},
year = {2016},
}
Publisher's Version
Article Search


Meister, Benoît 
CPP '16: "A Unified Coq Framework for ..."
A Unified Coq Framework for Verifying C Programs with FloatingPoint Computations
Tahina Ramananandro, Paul Mountcastle, Benoît Meister, and Richard Lethin (Reservoir Labs, USA)
We provide concrete evidence that floatingpoint computations in C programs can be verified in a homogeneous verification setting based on Coq only, by evaluating the practicality of the combination of the formal semantics of CompCert Clight and the Flocq formal specification of IEEE 754 floatingpoint arithmetic for the verification of properties of floatingpoint computations in C programs. To this end, we develop a framework to automatically compute realnumber expressions of C floatingpoint computations with rounding error terms along with their correctness proofs. We apply our framework to the complete analysis of an energyefficient C implementation of a radar image processing algorithm, for which we provide a certified bound on the total noise introduced by floatingpoint rounding errors and energyefficient approximations of square root and sine.
@InProceedings{CPP16p15,
author = {Tahina Ramananandro and Paul Mountcastle and Benoît Meister and Richard Lethin},
title = {A Unified Coq Framework for Verifying C Programs with FloatingPoint Computations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1526},
doi = {10.1145/2854065.2854066},
year = {2016},
}
Publisher's Version
Article Search


Mountcastle, Paul 
CPP '16: "A Unified Coq Framework for ..."
A Unified Coq Framework for Verifying C Programs with FloatingPoint Computations
Tahina Ramananandro, Paul Mountcastle, Benoît Meister, and Richard Lethin (Reservoir Labs, USA)
We provide concrete evidence that floatingpoint computations in C programs can be verified in a homogeneous verification setting based on Coq only, by evaluating the practicality of the combination of the formal semantics of CompCert Clight and the Flocq formal specification of IEEE 754 floatingpoint arithmetic for the verification of properties of floatingpoint computations in C programs. To this end, we develop a framework to automatically compute realnumber expressions of C floatingpoint computations with rounding error terms along with their correctness proofs. We apply our framework to the complete analysis of an energyefficient C implementation of a radar image processing algorithm, for which we provide a certified bound on the total noise introduced by floatingpoint rounding errors and energyefficient approximations of square root and sine.
@InProceedings{CPP16p15,
author = {Tahina Ramananandro and Paul Mountcastle and Benoît Meister and Richard Lethin},
title = {A Unified Coq Framework for Verifying C Programs with FloatingPoint Computations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1526},
doi = {10.1145/2854065.2854066},
year = {2016},
}
Publisher's Version
Article Search


Pąk, Karol 
CPP '16: "Towards a Mizar Environment ..."
Towards a Mizar Environment for Isabelle: Foundations and Language
Cezary Kaliszyk, Karol Pąk, and Josef Urban (University of Innsbruck, Austria; University of Białystok, Poland; Czech Technical University in Prague, Czech Republic)
In this paper we explore the possibility of emulating the Mizar environment as close as possible inside the Isabelle logical framework. We introduce adaptations to the Isabelle/FOL object logic that correspond to the logic of Mizar, as well as Isar inner syntax notations that correspond to these of the Mizar language. We show how Isabelle types can be used to differentiate between the syntactic categories of the Mizar language, such as sets and Mizar types including modes and attributes, and show how they interact with the basic constructs of the TarskiGrothendieck set theory. We discuss Mizar definitions and provide simple abbreviations that allow the introduction of Mizar predicates, functions, attributes and modes using the Isabelle/Pure language elements for introducing definitions and theorems. We finally consider the definite and indefinite description operators in Mizar and their use to introduce definitions by “means” and “equals”. We demonstrate the usability of the environment on a sample Mizarstyle formalization, with cluster inferences and “by” steps performed manually.
@InProceedings{CPP16p58,
author = {Cezary Kaliszyk and Karol Pąk and Josef Urban},
title = {Towards a Mizar Environment for Isabelle: Foundations and Language},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {5865},
doi = {10.1145/2854065.2854070},
year = {2016},
}
Publisher's Version
Article Search


Parrow, Joachim 
CPP '16: "Bisimulation UpTo Techniques ..."
Bisimulation UpTo Techniques for PsiCalculi
Johannes Åman Pohjola and Joachim Parrow (Uppsala University, Sweden)
Psicalculi is a parametric framework for process calculi similar to popular picalculus extensions such as the explicit fusion calculus, the applied picalculus and the spi calculus. Remarkably, machinechecked proofs of standard algebraic and congruence properties of bisimilarity apply to all calculi within the framework. Bisimulation upto techniques are methods for reducing the size of relations needed in bisimulation proofs. In this paper, we show how these bisimulation proof methods can be adapted to psicalculi. We formalise all our definitions and theorems in Nominal Isabelle, and show examples where the use of up totechniques yields drastically simplified proofs of known results. We also prove new structural laws about the replication operator.
@InProceedings{CPP16p142,
author = {Johannes Åman Pohjola and Joachim Parrow},
title = {Bisimulation UpTo Techniques for PsiCalculi},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {142153},
doi = {10.1145/2854065.2854080},
year = {2016},
}
Publisher's Version
Article Search


Paulson, Lawrence C. 
CPP '16: "A Modular, Efficient Formalisation ..."
A Modular, Efficient Formalisation of Real Algebraic Numbers
Wenda Li and Lawrence C. Paulson (University of Cambridge, UK)
This paper presents a construction of the real algebraic numbers with executable arithmetic operations in Isabelle/HOL. Instead of verified resultants, arithmetic operations on real algebraic numbers are based on a decision procedure to decide the sign of a bivariate polynomial (with rational coefficients) at a real algebraic point. The modular design allows the safe use of fast external code. This work can be the basis for decision procedures that rely on real algebraic numbers.
@InProceedings{CPP16p66,
author = {Wenda Li and Lawrence C. Paulson},
title = {A Modular, Efficient Formalisation of Real Algebraic Numbers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {6675},
doi = {10.1145/2854065.2854074},
year = {2016},
}
Publisher's Version
Article Search


Platzer, André 
CPP '16: "A Logic of Proofs for Differential ..."
A Logic of Proofs for Differential Dynamic Logic: Toward Independently Checkable Proof Certificates for Dynamic Logics
Nathan Fulton and André Platzer (Carnegie Mellon University, USA)
Differential dynamic logic is a logic for specifying and verifying safety, liveness, and other properties about models of cyberphysical systems. Theorem provers based on differential dynamic logic have been used to verify safety properties for models of selfdriving cars and collision avoidance protocols for aircraft. Unfortunately, these theorem provers do not have explicit proof terms, which makes the implementation of a number of important features unnecessarily complicated without soundnesscritical and extralogical extensions to the theorem prover. Examples include: an unambiguous separation between proof checking and proof search, the ability to extract program traces corresponding to counterexamples, and synthesis of surelylive deterministic programs from liveness proofs for nondeterministic programs. This paper presents a differential dynamic logic with such an explicit representation of proofs. The resulting logic extends both the syntax and semantics of differential dynamic logic with proof terms  syntactic representations of logical deductions. To support axiomatic theorem proving, the logic allows equivalence rewriting deep within formulas and supports both uniform renaming and uniform substitutions.
@InProceedings{CPP16p110,
author = {Nathan Fulton and André Platzer},
title = {A Logic of Proofs for Differential Dynamic Logic: Toward Independently Checkable Proof Certificates for Dynamic Logics},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {110121},
doi = {10.1145/2854065.2854078},
year = {2016},
}
Publisher's Version
Article Search


Rahli, Vincent 
CPP '16: "A Nominal Exploration of Intuitionism ..."
A Nominal Exploration of Intuitionism
Vincent Rahli and Mark Bickford (University of Luxembourg, Luxembourg; Cornell University, USA)
This papers extends the Nuprl proof assistant (a system representative
of the class of extensional type theories a la MartinLof) with
named exceptions and handlers, as well as a nominal
fresh operator. Using these new features, we prove a version
of Brouwer's Continuity Principle for numbers. We also provide a
simpler proof of a weaker version of this principle that only uses
diverging terms. We prove these two principles in Nuprl's metatheory
using our formalization of Nuprl in Coq and show how we can reflect
these metatheoretical results in the Nuprl theory as derivation
rules. We also show that these additions preserve Nuprl's key
metatheoretical properties, in particular consistency and the
congruence of Howe's computational equivalence relation. Using
continuity and the fan theorem we prove important results of
Intuitionistic Mathematics: Brouwer's continuity theorem and bar
induction on monotone bars.
@InProceedings{CPP16p130,
author = {Vincent Rahli and Mark Bickford},
title = {A Nominal Exploration of Intuitionism},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {130141},
doi = {10.1145/2854065.2854077},
year = {2016},
}
Publisher's Version
Article Search


Ramananandro, Tahina 
CPP '16: "A Unified Coq Framework for ..."
A Unified Coq Framework for Verifying C Programs with FloatingPoint Computations
Tahina Ramananandro, Paul Mountcastle, Benoît Meister, and Richard Lethin (Reservoir Labs, USA)
We provide concrete evidence that floatingpoint computations in C programs can be verified in a homogeneous verification setting based on Coq only, by evaluating the practicality of the combination of the formal semantics of CompCert Clight and the Flocq formal specification of IEEE 754 floatingpoint arithmetic for the verification of properties of floatingpoint computations in C programs. To this end, we develop a framework to automatically compute realnumber expressions of C floatingpoint computations with rounding error terms along with their correctness proofs. We apply our framework to the complete analysis of an energyefficient C implementation of a radar image processing algorithm, for which we provide a certified bound on the total noise introduced by floatingpoint rounding errors and energyefficient approximations of square root and sine.
@InProceedings{CPP16p15,
author = {Tahina Ramananandro and Paul Mountcastle and Benoît Meister and Richard Lethin},
title = {A Unified Coq Framework for Verifying C Programs with FloatingPoint Computations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1526},
doi = {10.1145/2854065.2854066},
year = {2016},
}
Publisher's Version
Article Search


Reger, Giles 
CPP '16: "The Vampire and the FOOL ..."
The Vampire and the FOOL
Evgenii Kotelnikov, Laura Kovács, Giles Reger, and Andrei Voronkov (Chalmers University of Technology, Sweden; University of Manchester, UK; EasyChair, UK)
This paper presents new features recently implemented in the theorem prover Vampire, namely support for firstorder logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also contains ifthenelse and letin expressions. We argue that presented extensions facilitate reasoningbased program analysis, both by increasing the expressivity of firstorder reasoners and by gains in efficiency.
@InProceedings{CPP16p37,
author = {Evgenii Kotelnikov and Laura Kovács and Giles Reger and Andrei Voronkov},
title = {The Vampire and the FOOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {3748},
doi = {10.1145/2854065.2854071},
year = {2016},
}
Publisher's Version
Article Search
Info


Rideau, Laurence 
CPP '16: "Formal Proofs of Transcendence ..."
Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials
Sophie Bernard, Yves Bertot, Laurence Rideau, and PierreYves Strub (Inria, France; IMDEA Software Institute, Spain)
We describe the formalisation in Coq of a proof that the numbers `e` and `pi` are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreover, some of the elements of our formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of `pi` relies extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials.
@InProceedings{CPP16p76,
author = {Sophie Bernard and Yves Bertot and Laurence Rideau and PierreYves Strub},
title = {Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {7687},
doi = {10.1145/2854065.2854072},
year = {2016},
}
Publisher's Version
Article Search


Schäfer, Steven 
CPP '16: "Axiomatic Semantics for Compiler ..."
Axiomatic Semantics for Compiler Verification
Steven Schäfer, Sigurd Schneider, and Gert Smolka (Saarland University, Germany)
Based on constructive type theory, we study two idealized imperative languages GC and IC and verify the correctness of a compiler from GC to IC. GC is a guarded command language with underspecified execution order defined with an axiomatic semantics. IC is a deterministic lowlevel language with linear sequential composition and lexically scoped gotos defined with a smallstep semantics. We characterize IC with an axiomatic semantics and prove that the compiler from GC to IC preserves specifications. The axiomatic semantics we consider model total correctness and map programs to continuous predicate transformers. We define the axiomatic semantics of GC and IC with elementary inductive predicates and show that the predicate transformer described by a program can be obtained compositionally by recursion on the syntax of the program using a fixed point operator for loops and continuations. We also show that two IC programs are contextually equivalent if and only if their predicate transformers are equivalent.
@InProceedings{CPP16p188,
author = {Steven Schäfer and Sigurd Schneider and Gert Smolka},
title = {Axiomatic Semantics for Compiler Verification},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {188196},
doi = {10.1145/2854065.2854083},
year = {2016},
}
Publisher's Version
Article Search


Schneider, Sigurd 
CPP '16: "Axiomatic Semantics for Compiler ..."
Axiomatic Semantics for Compiler Verification
Steven Schäfer, Sigurd Schneider, and Gert Smolka (Saarland University, Germany)
Based on constructive type theory, we study two idealized imperative languages GC and IC and verify the correctness of a compiler from GC to IC. GC is a guarded command language with underspecified execution order defined with an axiomatic semantics. IC is a deterministic lowlevel language with linear sequential composition and lexically scoped gotos defined with a smallstep semantics. We characterize IC with an axiomatic semantics and prove that the compiler from GC to IC preserves specifications. The axiomatic semantics we consider model total correctness and map programs to continuous predicate transformers. We define the axiomatic semantics of GC and IC with elementary inductive predicates and show that the predicate transformer described by a program can be obtained compositionally by recursion on the syntax of the program using a fixed point operator for loops and continuations. We also show that two IC programs are contextually equivalent if and only if their predicate transformers are equivalent.
@InProceedings{CPP16p188,
author = {Steven Schäfer and Sigurd Schneider and Gert Smolka},
title = {Axiomatic Semantics for Compiler Verification},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {188196},
doi = {10.1145/2854065.2854083},
year = {2016},
}
Publisher's Version
Article Search


Smolka, Gert 
CPP '16: "Axiomatic Semantics for Compiler ..."
Axiomatic Semantics for Compiler Verification
Steven Schäfer, Sigurd Schneider, and Gert Smolka (Saarland University, Germany)
Based on constructive type theory, we study two idealized imperative languages GC and IC and verify the correctness of a compiler from GC to IC. GC is a guarded command language with underspecified execution order defined with an axiomatic semantics. IC is a deterministic lowlevel language with linear sequential composition and lexically scoped gotos defined with a smallstep semantics. We characterize IC with an axiomatic semantics and prove that the compiler from GC to IC preserves specifications. The axiomatic semantics we consider model total correctness and map programs to continuous predicate transformers. We define the axiomatic semantics of GC and IC with elementary inductive predicates and show that the predicate transformer described by a program can be obtained compositionally by recursion on the syntax of the program using a fixed point operator for loops and continuations. We also show that two IC programs are contextually equivalent if and only if their predicate transformers are equivalent.
@InProceedings{CPP16p188,
author = {Steven Schäfer and Sigurd Schneider and Gert Smolka},
title = {Axiomatic Semantics for Compiler Verification},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {188196},
doi = {10.1145/2854065.2854083},
year = {2016},
}
Publisher's Version
Article Search


StMartin, Michel 
CPP '16: "A Verified Algorithm for Detecting ..."
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
Michel StMartin and Amy P. Felty (University of Ottawa, Canada)
We describe the formalization of a correctness proof for a conflict
detection algorithm for XACML (eXtensible Access Control Markup
Language). XACML is a standardized declarative access control
policy language that is increasingly used in industry. In practice it is
common for rule sets to grow large, and contain unintended errors,
often due to conflicting rules. A conflict occurs in a policy when one
rule permits a request and another denies that same request. Such
errors can lead to serious risks involving both allowing access to an
unauthorized user as well as denying access to someone who needs
it. Removing conflicts is thus an important aspect of debugging
policies, and the use of a verified algorithm provides the highest
assurance in a domain where security is important. In this paper,
we focus on several complex XACML constructs, including time
ranges and integer intervals, as well as ways to combine any number
of functions using the boolean operators and, or, and not. The latter
are the most complex, and add significant expressive power to the
language. We propose an algorithm to find conflicts and then use
the Coq Proof Assistant to prove the algorithm correct. We develop
a library of tactics to help automate the proof.
@InProceedings{CPP16p166,
author = {Michel StMartin and Amy P. Felty},
title = {A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {166175},
doi = {10.1145/2854065.2854079},
year = {2016},
}
Publisher's Version
Article Search


Strub, PierreYves 
CPP '16: "Formal Proofs of Transcendence ..."
Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials
Sophie Bernard, Yves Bertot, Laurence Rideau, and PierreYves Strub (Inria, France; IMDEA Software Institute, Spain)
We describe the formalisation in Coq of a proof that the numbers `e` and `pi` are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreover, some of the elements of our formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of `pi` relies extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials.
@InProceedings{CPP16p76,
author = {Sophie Bernard and Yves Bertot and Laurence Rideau and PierreYves Strub},
title = {Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {7687},
doi = {10.1145/2854065.2854072},
year = {2016},
}
Publisher's Version
Article Search


Tatlock, Zachary 
CPP '16: "Planning for Change in a Formal ..."
Planning for Change in a Formal Verification of the Raft Consensus Protocol
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson (University of Washington, USA)
We present the first formal verification of state machine safety for the Raft consensus protocol, a critical component of many distributed systems. We connected our proof to previous work to establish an endtoend guarantee that our implementation provides linearizable state machine replication. This proof required iteratively discovering and proving 90 system invariants. Our verified implementation is extracted to OCaml and runs on real networks.
The primary challenge we faced during the verification process was proof maintenance, since proving one invariant often required strengthening and updating other parts of our proof. To address this challenge, we propose a methodology of planning for change during verification. Our methodology adapts classical information hiding techniques to the context of proof assistants, factors out common invariantstrengthening patterns into custom induction principles, proves higherorder lemmas that show any property proved about a particular component implies analogous properties about related components, and makes proofs robust to change using structural tactics. We also discuss how our methodology may be applied to systems verification more broadly.
@InProceedings{CPP16p154,
author = {Doug Woos and James R. Wilcox and Steve Anton and Zachary Tatlock and Michael D. Ernst and Thomas Anderson},
title = {Planning for Change in a Formal Verification of the Raft Consensus Protocol},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {154165},
doi = {10.1145/2854065.2854081},
year = {2016},
}
Publisher's Version
Article Search


Thiemann, René 
CPP '16: "Formalizing Jordan Normal ..."
Formalizing Jordan Normal Forms in Isabelle/HOL
René Thiemann and Akihisa Yamada (University of Innsbruck, Austria)
In automated complexity analysis of term rewriting, estimating the
growth rate of the values in the kth power of a matrix A – for fixed
A and increasing k – is of fundamental interest. This growth rate
can be exactly characterized via A’s Jordan normal form (JNF). We
formalize this result in our library IsaFoR and our certifier CeTA,
and thereby improve the support for certifying polynomial bounds
derived by (untrusted) complexity analysis tools.
To this end, we develop a new library for matrices that allows us
to conveniently work with block matrices. Besides the mentioned
complexity result, we formalize GramSchmidt’s orthogonalization
algorithm and the Schur decomposition in order to prove existence
of JNFs. We also provide a uniqueness result for JNFs which allows
us to compute Jordan blocks for individual eigenvalues. In order to
determine eigenvalues automatically, we moreover formalize Yun’s
squarefree factorization algorithm.
@InProceedings{CPP16p88,
author = {René Thiemann and Akihisa Yamada},
title = {Formalizing Jordan Normal Forms in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {8899},
doi = {10.1145/2854065.2854073},
year = {2016},
}
Publisher's Version
Article Search


Trieu, Alix 
CPP '16: "Formal Verification of ControlFlow ..."
Formal Verification of ControlFlow Graph Flattening
Sandrine Blazy and Alix Trieu (IRISA, France; Université Rennes 1, France; ENS Rennes, France)
Code obfuscation is emerging as a key asset in security by obscurity. It aims at hiding sensitive information in programs so that they become more difficult to understand and reverse engineer. Since the results on the impossibility of perfect and universal obfuscation, many obfuscation techniques have been proposed in the literature, ranging from simple variable encoding to hiding the controlflow of a program. In this paper, we formally verify in Coq an advanced code obfuscation called controlflow graph flattening, that is used in stateoftheart program obfuscators. Our controlflow graph flattening is a program transformation operating over C programs, that is integrated into the CompCert formally verified compiler. The semantics preservation proof of our program obfuscator relies on a simulation proof performed on a realistic language, the Clight language of CompCert. The automatic extraction of our program obfuscator into OCaml yields a program with competitive results.
@InProceedings{CPP16p176,
author = {Sandrine Blazy and Alix Trieu},
title = {Formal Verification of ControlFlow Graph Flattening},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {176187},
doi = {10.1145/2854065.2854082},
year = {2016},
}
Publisher's Version
Article Search
Info


Urban, Josef 
CPP '16: "Towards a Mizar Environment ..."
Towards a Mizar Environment for Isabelle: Foundations and Language
Cezary Kaliszyk, Karol Pąk, and Josef Urban (University of Innsbruck, Austria; University of Białystok, Poland; Czech Technical University in Prague, Czech Republic)
In this paper we explore the possibility of emulating the Mizar environment as close as possible inside the Isabelle logical framework. We introduce adaptations to the Isabelle/FOL object logic that correspond to the logic of Mizar, as well as Isar inner syntax notations that correspond to these of the Mizar language. We show how Isabelle types can be used to differentiate between the syntactic categories of the Mizar language, such as sets and Mizar types including modes and attributes, and show how they interact with the basic constructs of the TarskiGrothendieck set theory. We discuss Mizar definitions and provide simple abbreviations that allow the introduction of Mizar predicates, functions, attributes and modes using the Isabelle/Pure language elements for introducing definitions and theorems. We finally consider the definite and indefinite description operators in Mizar and their use to introduce definitions by “means” and “equals”. We demonstrate the usability of the environment on a sample Mizarstyle formalization, with cluster inferences and “by” steps performed manually.
@InProceedings{CPP16p58,
author = {Cezary Kaliszyk and Karol Pąk and Josef Urban},
title = {Towards a Mizar Environment for Isabelle: Foundations and Language},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {5865},
doi = {10.1145/2854065.2854070},
year = {2016},
}
Publisher's Version
Article Search


Voronkov, Andrei 
CPP '16: "The Vampire and the FOOL ..."
The Vampire and the FOOL
Evgenii Kotelnikov, Laura Kovács, Giles Reger, and Andrei Voronkov (Chalmers University of Technology, Sweden; University of Manchester, UK; EasyChair, UK)
This paper presents new features recently implemented in the theorem prover Vampire, namely support for firstorder logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also contains ifthenelse and letin expressions. We argue that presented extensions facilitate reasoningbased program analysis, both by increasing the expressivity of firstorder reasoners and by gains in efficiency.
@InProceedings{CPP16p37,
author = {Evgenii Kotelnikov and Laura Kovács and Giles Reger and Andrei Voronkov},
title = {The Vampire and the FOOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {3748},
doi = {10.1145/2854065.2854071},
year = {2016},
}
Publisher's Version
Article Search
Info


Wilcox, James R. 
CPP '16: "Planning for Change in a Formal ..."
Planning for Change in a Formal Verification of the Raft Consensus Protocol
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson (University of Washington, USA)
We present the first formal verification of state machine safety for the Raft consensus protocol, a critical component of many distributed systems. We connected our proof to previous work to establish an endtoend guarantee that our implementation provides linearizable state machine replication. This proof required iteratively discovering and proving 90 system invariants. Our verified implementation is extracted to OCaml and runs on real networks.
The primary challenge we faced during the verification process was proof maintenance, since proving one invariant often required strengthening and updating other parts of our proof. To address this challenge, we propose a methodology of planning for change during verification. Our methodology adapts classical information hiding techniques to the context of proof assistants, factors out common invariantstrengthening patterns into custom induction principles, proves higherorder lemmas that show any property proved about a particular component implies analogous properties about related components, and makes proofs robust to change using structural tactics. We also discuss how our methodology may be applied to systems verification more broadly.
@InProceedings{CPP16p154,
author = {Doug Woos and James R. Wilcox and Steve Anton and Zachary Tatlock and Michael D. Ernst and Thomas Anderson},
title = {Planning for Change in a Formal Verification of the Raft Consensus Protocol},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {154165},
doi = {10.1145/2854065.2854081},
year = {2016},
}
Publisher's Version
Article Search


Woos, Doug 
CPP '16: "Planning for Change in a Formal ..."
Planning for Change in a Formal Verification of the Raft Consensus Protocol
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson (University of Washington, USA)
We present the first formal verification of state machine safety for the Raft consensus protocol, a critical component of many distributed systems. We connected our proof to previous work to establish an endtoend guarantee that our implementation provides linearizable state machine replication. This proof required iteratively discovering and proving 90 system invariants. Our verified implementation is extracted to OCaml and runs on real networks.
The primary challenge we faced during the verification process was proof maintenance, since proving one invariant often required strengthening and updating other parts of our proof. To address this challenge, we propose a methodology of planning for change during verification. Our methodology adapts classical information hiding techniques to the context of proof assistants, factors out common invariantstrengthening patterns into custom induction principles, proves higherorder lemmas that show any property proved about a particular component implies analogous properties about related components, and makes proofs robust to change using structural tactics. We also discuss how our methodology may be applied to systems verification more broadly.
@InProceedings{CPP16p154,
author = {Doug Woos and James R. Wilcox and Steve Anton and Zachary Tatlock and Michael D. Ernst and Thomas Anderson},
title = {Planning for Change in a Formal Verification of the Raft Consensus Protocol},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {154165},
doi = {10.1145/2854065.2854081},
year = {2016},
}
Publisher's Version
Article Search


Yamada, Akihisa 
CPP '16: "Formalizing Jordan Normal ..."
Formalizing Jordan Normal Forms in Isabelle/HOL
René Thiemann and Akihisa Yamada (University of Innsbruck, Austria)
In automated complexity analysis of term rewriting, estimating the
growth rate of the values in the kth power of a matrix A – for fixed
A and increasing k – is of fundamental interest. This growth rate
can be exactly characterized via A’s Jordan normal form (JNF). We
formalize this result in our library IsaFoR and our certifier CeTA,
and thereby improve the support for certifying polynomial bounds
derived by (untrusted) complexity analysis tools.
To this end, we develop a new library for matrices that allows us
to conveniently work with block matrices. Besides the mentioned
complexity result, we formalize GramSchmidt’s orthogonalization
algorithm and the Schur decomposition in order to prove existence
of JNFs. We also provide a uniqueness result for JNFs which allows
us to compute Jordan blocks for individual eigenvalues. In order to
determine eigenvalues automatically, we moreover formalize Yun’s
squarefree factorization algorithm.
@InProceedings{CPP16p88,
author = {René Thiemann and Akihisa Yamada},
title = {Formalizing Jordan Normal Forms in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {8899},
doi = {10.1145/2854065.2854073},
year = {2016},
}
Publisher's Version
Article Search

46 authors
proc time: 0.29