ask others

CPP 2016: Saint Petersburg, FL, USA

> Home > Conferences and Workshops > CPP

- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/2016
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/2016
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

- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/Friedman16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Friedman16
Harvey M. Friedman:
Perspectives on formal verification (invited talk). 1
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/Moura16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Moura16
Leonardo Mendonça de Moura:
Dependent type practice (invited talk). 2

Verifying Imperative Programs

- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/Chargueraud16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Chargueraud16
Arthur Charguéraud:
Higher-order representation predicates in separation logic. 3-14
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/RamananandroMML16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/RamananandroMML16
Tahina Ramananandro, Paul Mountcastle, Benoît Meister, Richard Lethin:
A unified Coq framework for verifying C programs with floating-point computations. 15-26
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/Lammich16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Lammich16
Peter Lammich:
Refinement based verification of imperative data structures. 27-36

Design and Implementation of Theorem Provers

- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/KotelnikovKRV16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/KotelnikovKRV16
Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov:
The vampire and the FOOL. 37-48
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/Czajka16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Czajka16
Lukasz Czajka:
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions. 49-57
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/KaliszykPU16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/KaliszykPU16
Cezary Kaliszyk, Karol Pak, Josef Urban:
Towards a mizar environment for isabelle: foundations and language. 58-65

Mathematics

- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/LiP16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/LiP16
Wenda Li, Lawrence C. Paulson:
A modular, efficient formalisation of real algebraic numbers. 66-75
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/BernardBRS16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/BernardBRS16
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
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/Thiemann016
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Thiemann016
René Thiemann, Akihisa Yamada:
Formalizing jordan normal forms in Isabelle/HOL. 88-99
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/CohenD16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/CohenD16
Cyril Cohen, Boris Djalal:
Formalization of a newton series representation of polynomials. 100-109

Foundations

- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/FultonP16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/FultonP16
Nathan Fulton, André Platzer:
A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics. 110-121
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/Doorn16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/Doorn16
Floris van Doorn:
Constructing the propositional truncation using non-recursive HITs. 122-129
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/RahliB16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/RahliB16
Vincent Rahli, Mark Bickford:
A nominal exploration of intuitionism. 130-141

Verification for Concurrent and Distributed Systems

- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/PohjolaP16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/PohjolaP16
Johannes Åman Pohjola, Joachim Parrow:
Bisimulation up-to techniques for psi-calculi. 142-153
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/WoosWATEA16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/WoosWATEA16
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
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/St-MartinF16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/St-MartinF16
Michel St-Martin, Amy P. Felty:
A verified algorithm for detecting conflicts in XACML access control rules. 166-175

Compiler Verification

- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/BlazyT16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/BlazyT16
Sandrine Blazy, Alix Trieu:
Formal verification of control-flow graph flattening. 176-187
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/SchaferSS16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/SchaferSS16
Steven Schäfer, Sigurd Schneider, Gert Smolka:
Axiomatic semantics for compiler verification. 188-196

maintained by

at