default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDCPP 2016: Saint Petersburg, FL, USA
- Jeremy Avigad, Adam Chlipala:
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016. ACM 2016, ISBN 978-1-4503-4127-1
Keynotes
- Harvey M. Friedman:
Perspectives on formal verification (invited talk). 1 - Leonardo Mendonça de Moura:
Dependent type practice (invited talk). 2
Verifying Imperative Programs
- Arthur Charguéraud:
Higher-order representation predicates in separation logic. 3-14 - Tahina Ramananandro
, Paul Mountcastle, Benoît Meister, Richard Lethin:
A unified Coq framework for verifying C programs with floating-point computations. 15-26 - Peter Lammich:
Refinement based verification of imperative data structures. 27-36
Design and Implementation of Theorem Provers
- Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov:
The vampire and the FOOL. 37-48 - Lukasz Czajka:
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions. 49-57 - Cezary Kaliszyk, Karol Pak, Josef Urban:
Towards a mizar environment for isabelle: foundations and language. 58-65
Mathematics
- Wenda Li, Lawrence C. Paulson:
A modular, efficient formalisation of real algebraic numbers. 66-75 - Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub:
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. 76-87 - René Thiemann, Akihisa Yamada:
Formalizing jordan normal forms in Isabelle/HOL. 88-99 - Cyril Cohen, Boris Djalal:
Formalization of a newton series representation of polynomials. 100-109
Foundations
- Nathan Fulton, André Platzer:
A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics. 110-121 - Floris van Doorn:
Constructing the propositional truncation using non-recursive HITs. 122-129 - Vincent Rahli, Mark Bickford:
A nominal exploration of intuitionism. 130-141
Verification for Concurrent and Distributed Systems
- Johannes Åman Pohjola, Joachim Parrow:
Bisimulation up-to techniques for psi-calculi. 142-153 - Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas E. Anderson:
Planning for change in a formal verification of the raft consensus protocol. 154-165 - Michel St-Martin, Amy P. Felty:
A verified algorithm for detecting conflicts in XACML access control rules. 166-175
Compiler Verification
- Sandrine Blazy, Alix Trieu:
Formal verification of control-flow graph flattening. 176-187 - Steven Schäfer, Sigurd Schneider, Gert Smolka:
Axiomatic semantics for compiler verification. 188-196
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-12-13 20:20 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
