| |
Å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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|
| |
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},
}
|