CPP 2016 – Author Index

A B C D E F K L M P R S T U V W Y

	Åman Pohjola, Johannes	CPP '16: "Bisimulation Up-To Techniques ..." Bisimulation Up-To Techniques for Psi-Calculi Johannes Åman Pohjola and Joachim Parrow (Uppsala University, Sweden) @InProceedings{CPP16p161, author = {Johannes Åman Pohjola and Joachim Parrow}, title = {Bisimulation Up-To Techniques for Psi-Calculi}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {161-160}, doi = {}, year = {2016}, } Article: cpp16main-mainid22-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p173, 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 = {173-172}, doi = {}, year = {2016}, } Article: cpp16main-mainid7-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p173, 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 = {173-172}, doi = {}, year = {2016}, } Article: cpp16main-mainid7-p (type: Full Paper (12 Pages)) doi:
	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 Pierre-Yves Strub (Inria, France; IMDEA Software Institute, Spain) @InProceedings{CPP16p89, author = {Sophie Bernard and Yves Bertot and Laurence Rideau and Pierre-Yves Strub}, title = {Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {89-88}, doi = {}, year = {2016}, } Article: cpp16main-mainid5-p (type: Full Paper (12 Pages)) doi:
	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 Pierre-Yves Strub (Inria, France; IMDEA Software Institute, Spain) @InProceedings{CPP16p89, author = {Sophie Bernard and Yves Bertot and Laurence Rideau and Pierre-Yves Strub}, title = {Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {89-88}, doi = {}, year = {2016}, } Article: cpp16main-mainid5-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p149, author = {Vincent Rahli and Mark Bickford}, title = {A Nominal Exploration of Intuitionism}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {149-148}, doi = {}, year = {2016}, } Article: cpp16main-mainid11-p (type: Full Paper (12 Pages)) doi:
	Blazy, Sandrine	CPP '16: "Formal Verification of Control-Flow ..." Formal Verification of Control-Flow Graph Flattening Sandrine Blazy and Alix Trieu (IRISA, France; Université Rennes 1, France; ENS Rennes, France) @InProceedings{CPP16p197, author = {Sandrine Blazy and Alix Trieu}, title = {Formal Verification of Control-Flow Graph Flattening}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {197-196}, doi = {}, year = {2016}, } Article: cpp16main-mainid19-p (type: Full Paper (12 Pages)) doi:
	Charguéraud, Arthur	CPP '16: "Higher-Order Representation ..." Higher-Order Representation Predicates in Separation Logic Arthur Charguéraud (Inria, France) @InProceedings{CPP16p5, author = {Arthur Charguéraud}, title = {Higher-Order Representation Predicates in Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {5-4}, doi = {}, year = {2016}, } Article: cpp16main-mainid21-p (type: Full Paper (12 Pages)) doi:
	Cohen, Cyril	CPP '16: "Formalization of a Newton ..." Formalization of a Newton Series Representation of Polynomials Cyril Cohen and Boris Djalal (Inria, France) @InProceedings{CPP16p113, author = {Cyril Cohen and Boris Djalal}, title = {Formalization of a Newton Series Representation of Polynomials}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {113-112}, doi = {}, year = {2016}, } Article: cpp16main-mainid9-p (type: Full Paper (12 Pages)) doi:
	Czajka, Łukasz	CPP '16: "Improving Automation in Interactive ..." Improving Automation in Interactive Theorem Provers by Efficient Encoding of Lambda-Abstractions Łukasz Czajka (University of Innsbruck, Austria) @InProceedings{CPP16p53, author = {Łukasz Czajka}, title = {Improving Automation in Interactive Theorem Provers by Efficient Encoding of Lambda-Abstractions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {53-52}, doi = {}, year = {2016}, } Article: cpp16main-mainid29-p (type: Full Paper (12 Pages)) doi:
	De Moura, Leonardo	CPP '16: "Dependent Type Practice (Invited ..." Dependent Type Practice (Invited Talk) Leonardo de Moura (Microsoft Research, USA) @InProceedings{CPP16p3, author = {Leonardo de Moura}, title = {Dependent Type Practice (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {3-2}, doi = {}, year = {2016}, } Article: cpp16key-key2-p (type: Invited Talk (2 Pages)) doi:
	Djalal, Boris	CPP '16: "Formalization of a Newton ..." Formalization of a Newton Series Representation of Polynomials Cyril Cohen and Boris Djalal (Inria, France) @InProceedings{CPP16p113, author = {Cyril Cohen and Boris Djalal}, title = {Formalization of a Newton Series Representation of Polynomials}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {113-112}, doi = {}, year = {2016}, } Article: cpp16main-mainid9-p (type: Full Paper (12 Pages)) doi:
	Doorn, Floris van	CPP '16: "Constructing the Propositional ..." Constructing the Propositional Truncation using Non-recursive HITs Floris van Doorn (Carnegie Mellon University, USA) @InProceedings{CPP16p137, author = {Floris van Doorn}, title = {Constructing the Propositional Truncation using Non-recursive HITs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {137-136}, doi = {}, year = {2016}, } Article: cpp16main-mainid42-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p173, 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 = {173-172}, doi = {}, year = {2016}, } Article: cpp16main-mainid7-p (type: Full Paper (12 Pages)) doi:
	Felty, Amy P.	CPP '16: "A Verified Algorithm for Detecting ..." A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules Michel St-Martin and Amy P. Felty (University of Ottawa, Canada) @InProceedings{CPP16p185, author = {Michel St-Martin and Amy P. Felty}, title = {A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {185-184}, doi = {}, year = {2016}, } Article: cpp16main-mainid14-p (type: Full Paper (12 Pages)) doi:
	Friedman, Harvey M.	CPP '16: "Perspectives on Formal Verification ..." Perspectives on Formal Verification (Invited Talk) Harvey M. Friedman (Ohio State University, USA) @InProceedings{CPP16p1, author = {Harvey M. Friedman}, title = {Perspectives on Formal Verification (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1-0}, doi = {}, year = {2016}, } Article: cpp16key-key1-p (type: Invited Talk (2 Pages)) doi:
	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) @InProceedings{CPP16p125, 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 = {125-124}, doi = {}, year = {2016}, } Article: cpp16main-mainid40-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p65, 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 = {65-64}, doi = {}, year = {2016}, } Article: cpp16main-mainid31-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p41, 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 = {41-40}, doi = {}, year = {2016}, } Article: cpp16main-mainid28-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p41, 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 = {41-40}, doi = {}, year = {2016}, } Article: cpp16main-mainid28-p (type: Full Paper (12 Pages)) doi:
	Lammich, Peter	CPP '16: "Refinement Based Verification ..." Refinement Based Verification of Imperative Data Structures Peter Lammich (TU München, Germany) @InProceedings{CPP16p29, author = {Peter Lammich}, title = {Refinement Based Verification of Imperative Data Structures}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {29-28}, doi = {}, year = {2016}, } Article: cpp16main-mainid3-p (type: Full Paper (12 Pages)) doi:
	Lethin, Richard	CPP '16: "A Unified Coq Framework for ..." A Unified Coq Framework for Verifying C Programs with Floating-Point Computations Tahina Ramananandro, Paul Mountcastle, Benoît Meister, and Richard Lethin (Reservoir Labs, USA) @InProceedings{CPP16p17, author = {Tahina Ramananandro and Paul Mountcastle and Benoît Meister and Richard Lethin}, title = {A Unified Coq Framework for Verifying C Programs with Floating-Point Computations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {17-16}, doi = {}, year = {2016}, } Article: cpp16main-mainid15-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p77, author = {Wenda Li and Lawrence C. Paulson}, title = {A Modular, Efficient Formalisation of Real Algebraic Numbers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {77-76}, doi = {}, year = {2016}, } Article: cpp16main-mainid8-p (type: Full Paper (12 Pages)) doi:
	Meister, Benoît	CPP '16: "A Unified Coq Framework for ..." A Unified Coq Framework for Verifying C Programs with Floating-Point Computations Tahina Ramananandro, Paul Mountcastle, Benoît Meister, and Richard Lethin (Reservoir Labs, USA) @InProceedings{CPP16p17, author = {Tahina Ramananandro and Paul Mountcastle and Benoît Meister and Richard Lethin}, title = {A Unified Coq Framework for Verifying C Programs with Floating-Point Computations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {17-16}, doi = {}, year = {2016}, } Article: cpp16main-mainid15-p (type: Full Paper (12 Pages)) doi:
	Mountcastle, Paul	CPP '16: "A Unified Coq Framework for ..." A Unified Coq Framework for Verifying C Programs with Floating-Point Computations Tahina Ramananandro, Paul Mountcastle, Benoît Meister, and Richard Lethin (Reservoir Labs, USA) @InProceedings{CPP16p17, author = {Tahina Ramananandro and Paul Mountcastle and Benoît Meister and Richard Lethin}, title = {A Unified Coq Framework for Verifying C Programs with Floating-Point Computations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {17-16}, doi = {}, year = {2016}, } Article: cpp16main-mainid15-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p65, 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 = {65-64}, doi = {}, year = {2016}, } Article: cpp16main-mainid31-p (type: Full Paper (12 Pages)) doi:
	Parrow, Joachim	CPP '16: "Bisimulation Up-To Techniques ..." Bisimulation Up-To Techniques for Psi-Calculi Johannes Åman Pohjola and Joachim Parrow (Uppsala University, Sweden) @InProceedings{CPP16p161, author = {Johannes Åman Pohjola and Joachim Parrow}, title = {Bisimulation Up-To Techniques for Psi-Calculi}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {161-160}, doi = {}, year = {2016}, } Article: cpp16main-mainid22-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p77, author = {Wenda Li and Lawrence C. Paulson}, title = {A Modular, Efficient Formalisation of Real Algebraic Numbers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {77-76}, doi = {}, year = {2016}, } Article: cpp16main-mainid8-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p125, 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 = {125-124}, doi = {}, year = {2016}, } Article: cpp16main-mainid40-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p149, author = {Vincent Rahli and Mark Bickford}, title = {A Nominal Exploration of Intuitionism}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {149-148}, doi = {}, year = {2016}, } Article: cpp16main-mainid11-p (type: Full Paper (12 Pages)) doi:
	Ramananandro, Tahina	CPP '16: "A Unified Coq Framework for ..." A Unified Coq Framework for Verifying C Programs with Floating-Point Computations Tahina Ramananandro, Paul Mountcastle, Benoît Meister, and Richard Lethin (Reservoir Labs, USA) @InProceedings{CPP16p17, author = {Tahina Ramananandro and Paul Mountcastle and Benoît Meister and Richard Lethin}, title = {A Unified Coq Framework for Verifying C Programs with Floating-Point Computations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {17-16}, doi = {}, year = {2016}, } Article: cpp16main-mainid15-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p41, 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 = {41-40}, doi = {}, year = {2016}, } Article: cpp16main-mainid28-p (type: Full Paper (12 Pages)) doi:
	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 Pierre-Yves Strub (Inria, France; IMDEA Software Institute, Spain) @InProceedings{CPP16p89, author = {Sophie Bernard and Yves Bertot and Laurence Rideau and Pierre-Yves Strub}, title = {Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {89-88}, doi = {}, year = {2016}, } Article: cpp16main-mainid5-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p209, author = {Steven Schäfer and Sigurd Schneider and Gert Smolka}, title = {Axiomatic Semantics for Compiler Verification}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {209-208}, doi = {}, year = {2016}, } Article: cpp16main-mainid10-p (type: Full Paper (12 Pages)) doi:
	Schneider, Sigurd	CPP '16: "Axiomatic Semantics for Compiler ..." Axiomatic Semantics for Compiler Verification Steven Schäfer, Sigurd Schneider, and Gert Smolka (Saarland University, Germany) @InProceedings{CPP16p209, author = {Steven Schäfer and Sigurd Schneider and Gert Smolka}, title = {Axiomatic Semantics for Compiler Verification}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {209-208}, doi = {}, year = {2016}, } Article: cpp16main-mainid10-p (type: Full Paper (12 Pages)) doi:
	Smolka, Gert	CPP '16: "Axiomatic Semantics for Compiler ..." Axiomatic Semantics for Compiler Verification Steven Schäfer, Sigurd Schneider, and Gert Smolka (Saarland University, Germany) @InProceedings{CPP16p209, author = {Steven Schäfer and Sigurd Schneider and Gert Smolka}, title = {Axiomatic Semantics for Compiler Verification}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {209-208}, doi = {}, year = {2016}, } Article: cpp16main-mainid10-p (type: Full Paper (12 Pages)) doi:
	St-Martin, Michel	CPP '16: "A Verified Algorithm for Detecting ..." A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules Michel St-Martin and Amy P. Felty (University of Ottawa, Canada) @InProceedings{CPP16p185, author = {Michel St-Martin and Amy P. Felty}, title = {A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {185-184}, doi = {}, year = {2016}, } Article: cpp16main-mainid14-p (type: Full Paper (12 Pages)) doi:
	Strub, Pierre-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 Pierre-Yves Strub (Inria, France; IMDEA Software Institute, Spain) @InProceedings{CPP16p89, author = {Sophie Bernard and Yves Bertot and Laurence Rideau and Pierre-Yves Strub}, title = {Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {89-88}, doi = {}, year = {2016}, } Article: cpp16main-mainid5-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p173, 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 = {173-172}, doi = {}, year = {2016}, } Article: cpp16main-mainid7-p (type: Full Paper (12 Pages)) doi:
	Thiemann, René	CPP '16: "Formalizing Jordan Normal ..." Formalizing Jordan Normal Forms in Isabelle/HOL René Thiemann and Akihisa Yamada (University of Innsbruck, Austria) @InProceedings{CPP16p101, author = {René Thiemann and Akihisa Yamada}, title = {Formalizing Jordan Normal Forms in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {101-100}, doi = {}, year = {2016}, } Article: cpp16main-mainid35-p (type: Full Paper (12 Pages)) doi:
	Trieu, Alix	CPP '16: "Formal Verification of Control-Flow ..." Formal Verification of Control-Flow Graph Flattening Sandrine Blazy and Alix Trieu (IRISA, France; Université Rennes 1, France; ENS Rennes, France) @InProceedings{CPP16p197, author = {Sandrine Blazy and Alix Trieu}, title = {Formal Verification of Control-Flow Graph Flattening}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {197-196}, doi = {}, year = {2016}, } Article: cpp16main-mainid19-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p65, 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 = {65-64}, doi = {}, year = {2016}, } Article: cpp16main-mainid31-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p41, 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 = {41-40}, doi = {}, year = {2016}, } Article: cpp16main-mainid28-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p173, 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 = {173-172}, doi = {}, year = {2016}, } Article: cpp16main-mainid7-p (type: Full Paper (12 Pages)) doi:
	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) @InProceedings{CPP16p173, 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 = {173-172}, doi = {}, year = {2016}, } Article: cpp16main-mainid7-p (type: Full Paper (12 Pages)) doi:
	Yamada, Akihisa	CPP '16: "Formalizing Jordan Normal ..." Formalizing Jordan Normal Forms in Isabelle/HOL René Thiemann and Akihisa Yamada (University of Innsbruck, Austria) @InProceedings{CPP16p101, author = {René Thiemann and Akihisa Yamada}, title = {Formalizing Jordan Normal Forms in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {101-100}, doi = {}, year = {2016}, } Article: cpp16main-mainid35-p (type: Full Paper (12 Pages)) doi:

46 authors

proc time: 0.05