CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016

Topics of interest:

We welcome submissions in research areas related to formal certification of programs and proofs. The following is a suggested list of topics of interest to CPP. This is a non-exhaustive list and should be read as a guideline rather than a requirement.

  • certified or certifying programming, compilation, linking, OS kernels, runtime systems, and security monitors
  • program logics, type systems, and semantics for certified code
  • certified decision procedures, mathematical libraries, and mathematical theorems
  • proof assistants and proof theory
  • new languages and tools for certified programming
  • program analysis, program verification, and proof-carrying code
  • certified secure protocols and transactions
  • certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest
  • certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification
  • certificates for program termination *logics for certifying concurrent and distributed programs
  • higher-order logics, logical systems, separation logics, and logics for security
  • teaching mathematics and computer science with proof assistants

Please see the external CPP web site for the full details.

Dates
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Mon 18 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00
Session 1: Invited talk by Harvey FriedmanCPP at Room St Petersburg II
09:00
60m
Talk
Perspectives on Formal Verfication
CPP
Harvey FriedmanOhio State University
14:00 - 15:30
Session 3: Design and Implementation of Theorem ProversCPP at Room St Petersburg II
14:00
30m
Talk
The Vampire and the FOOL
CPP
Evgenii KotelnikovChalmers University of Technology, Laura KovacsChalmers University of Technology, Giles RegerUniversity of Manchester, Andrei VoronkovUniversity of Manchester
14:30
30m
Talk
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
CPP
Lukasz CzajkaUniversity of Innsbruck
15:00
30m
Talk
Mizar Environment for Isabelle
CPP
Cezary KaliszykUniversity of Innsbruck, Karol PąkUniversity of Bialystok, Institute of Computer Science, Josef Urban

Tue 19 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00
Session 5: Invited talk by Leonardo de MouraCPP at Room St Petersburg II
09:00
60m
Talk
Dependent Type Practice
CPP
Leonardo de MouraMicrosoft Research, Redmond
14:00 - 15:30
Session 7: Verification for Concurrent and Distributed SystemsCPP at Room St Petersburg II
14:00
30m
Talk
Bisimulation Up-to Techniques for Psi-calculi
CPP
Johannes Å. PohjolaUppsala University, Joachim ParrowUppsala University
14:30
30m
Talk
Planning for Change in a Formal Verification of the Raft Consensus Protocol
CPP
Doug WoosUniversity of Washington, James R. WilcoxUniversity of Washington, Steve AntonUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Michael D. ErnstUniversity of Washington, Thomas AndersonUniversity of Washington
Pre-print
15:00
30m
Talk
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
CPP
Michel St-MartinUniversity of Ottawa, Amy FeltyUniversity of Ottawa
16:00 - 17:00
Session 8: Compiler VerificationCPP at Room St Petersburg II
16:00
30m
Talk
Formal Verification of Control-flow Graph Flattening
CPP
Sandrine BlazyIRISA / University of Rennes 1, Alix TrieuENS Rennes
16:30
30m
Talk
Axiomatic Semantics for Compiler Verification
CPP
Steven Schäfer, Sigurd SchneiderSaarland University, Gert SmolkaSaarland University
18:00 - 21:00
CPP Reception, sponsored by the DeepSpec projectCPP at Room St Petersburg I
18:00
3h
Social Event
CPP Reception, sponsored by the DeepSpec project
CPP

Call for Papers

Please see the external CPP web site for the full details, but here’s a summary of the most important points.

  • Abstracts due: October 7
  • Papers due: October 12
  • Author Notification: November 18
  • Final versions due: December 4
  • Conference: January 18-19

The paper format is compatible with the one from recent POPL and ICFP conferences.

Accepted Papers

Title
A Logic of Proofs for Differential Dynamic Logic
CPP
A Modular, Efficient Formalisation of Real Algebraic Numbers
CPP
A Nominal Exploration of Intuitionism
CPP
A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
CPP
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
CPP
Axiomatic Semantics for Compiler Verification
CPP
Bisimulation Up-to Techniques for Psi-calculi
CPP
Constructing the Propositional Truncation using Non-recursive HITs
CPP
Formal Verification of Control-flow Graph Flattening
CPP
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
CPP
Formalization of a Newton series representation of polynomials
CPP
Formalizing Jordan Normal Forms in Isabelle/HOL
CPP
Higher-order Representation Predicates in Separation Logic
CPP
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
CPP
Mizar Environment for Isabelle
CPP
Planning for Change in a Formal Verification of the Raft Consensus Protocol
CPP
Pre-print
Refinement Based Verification of Imperative Data Structures
CPP
The Vampire and the FOOL
CPP