CPP 2016: THE FIFTH INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS

A
Anderson, Thomas	Planning for Change in a Formal Verification of the Raft Consensus Protocol
Anton, Steve	Planning for Change in a Formal Verification of the Raft Consensus Protocol
B
Bernard, Sophie	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
Bertot, Yves	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
Bickford, Mark	A Nominal Exploration of Intuitionism
Blazy, Sandrine	Formal Verification of Control-flow Graph Flattening
C
Charguéraud, Arthur	Higher-order Representation Predicates in Separation Logic
Cohen, Cyril	Formalization of a Newton series representation of polynomials
Czajka, Łukasz	Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
D
Djalal, Boris	Formalization of a Newton series representation of polynomials
E
Ernst, Michael D.	Planning for Change in a Formal Verification of the Raft Consensus Protocol
F
Felty, Amy	A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
Fulton, Nathan	A Logic of Proofs for Differential Dynamic Logic
K
Kaliszyk, Cezary	Mizar Environment for Isabelle
Kotelnikov, Evgenii	The Vampire and the FOOL
Kovacs, Laura	The Vampire and the FOOL
L
Lammich, Peter	Refinement Based Verification of Imperative Data Structures
Lethin, Richard	A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
Li, Wenda	A Modular, Efficient Formalisation of Real Algebraic Numbers
M
Meister, Benoît	A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
Mountcastle, Paul	A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
P
Parrow, Joachim	Bisimulation Up-to Techniques for Psi-calculi
Paulson, Lawrence C.	A Modular, Efficient Formalisation of Real Algebraic Numbers
Platzer, André	A Logic of Proofs for Differential Dynamic Logic
Pąk, Karol	Mizar Environment for Isabelle
R
Rahli, Vincent	A Nominal Exploration of Intuitionism
Ramananandro, Tahina	A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
Reger, Giles	The Vampire and the FOOL
Rideau, Laurence	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
S
Schneider, Sigurd	Axiomatic Semantics for Compiler Verification
Schäfer, Steven	Axiomatic Semantics for Compiler Verification
Smolka, Gert	Axiomatic Semantics for Compiler Verification
St-Martin, Michel	A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
Strub, Pierre-Yves	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
T
Tatlock, Zachary	Planning for Change in a Formal Verification of the Raft Consensus Protocol
Thiemann, René	Formalizing Jordan Normal Forms in Isabelle/HOL
Trieu, Alix	Formal Verification of Control-flow Graph Flattening
U
Urban, Josef	Mizar Environment for Isabelle
V
van Doorn, Floris	Constructing the Propositional Truncation using Non-recursive HITs
Voronkov, Andrei	The Vampire and the FOOL
W
Wilcox, James R.	Planning for Change in a Formal Verification of the Raft Consensus Protocol
Woos, Doug	Planning for Change in a Formal Verification of the Raft Consensus Protocol
Y
Yamada, Akihisa	Formalizing Jordan Normal Forms in Isabelle/HOL
Å
Åman Pohjola, Johannes	Bisimulation Up-to Techniques for Psi-calculi

Disclaimer | Powered by EasyChair Smart Program