Program - CPP

Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States

co-located with POPL 2016

Filter

Mon 18 Jan

09:00 - 10:00: CPP - Session 1: Invited talk by Harvey Friedman at Room St Petersburg II

09:00 - 10:00
Talk

Perspectives on Formal Verfication

Harvey Friedman

10:30 - 12:00: CPP - Session 2: Verifying Imperative Programs at Room St Petersburg II

10:30 - 11:00
Talk

Higher-order Representation Predicates in Separation Logic

Arthur Charguéraud

11:00 - 11:30
Talk

A Unified Coq Framework for Verifying C Programs with Floating-Point Computations

Tahina Ramananandro, Paul Mountcastle, Benoit Meister, Richard Lethin

11:30 - 12:00
Talk

Refinement Based Verification of Imperative Data Structures

14:00 - 15:30: CPP - Session 3: Design and Implementation of Theorem Provers at Room St Petersburg II

14:00 - 14:30
Talk

The Vampire and the FOOL

Evgenii Kotelnikov, Laura Kovacs, Giles Reger, Andrei Voronkov

14:30 - 15:00
Talk

Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions

15:00 - 15:30
Talk

Mizar Environment for Isabelle

Cezary Kaliszyk, Karol Pąk, Josef Urban

16:00 - 18:00: CPP - Session 4: Mathematics at Room St Petersburg II

16:00 - 16:30
Talk

A Modular, Efficient Formalisation of Real Algebraic Numbers

Wenda Li, Lawrence Paulson

16:30 - 17:00
Talk

Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials

Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub

17:00 - 17:30
Talk

Formalizing Jordan Normal Forms in Isabelle/HOL

René Thiemann, Akihisa Yamada

17:30 - 18:00
Talk

Formalization of a Newton series representation of polynomials

Cyril Cohen, Boris Djalal

Tue 19 Jan

09:00 - 10:00: CPP - Session 5: Invited talk by Leonardo de Moura at Room St Petersburg II

09:00 - 10:00
Talk

Dependent Type Practice

Leonardo De Moura

10:30 - 12:00: CPP - Session 6: Foundations at Room St Petersburg II

10:30 - 11:00
Talk

A Logic of Proofs for Differential Dynamic Logic

Nathan Fulton, André Platzer

11:00 - 11:30
Talk

Constructing the Propositional Truncation using Non-recursive HITs

Floris van Doorn

11:30 - 12:00
Talk

A Nominal Exploration of Intuitionism

Vincent Rahli, Mark Bickford

14:00 - 15:30: CPP - Session 7: Verification for Concurrent and Distributed Systems at Room St Petersburg II

14:00 - 14:30
Talk

Bisimulation Up-to Techniques for Psi-calculi

Johannes Å. Pohjola, Joachim Parrow

14:30 - 15:00
Talk

Planning for Change in a Formal Verification of the Raft Consensus Protocol

Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas Anderson

15:00 - 15:30
Talk

A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules

Michel St-Martin, Amy Felty

16:00 - 17:00: CPP - Session 8: Compiler Verification at Room St Petersburg II

16:00 - 16:30
Talk

Formal Verification of Control-flow Graph Flattening

Sandrine Blazy, Alix Trieu

16:30 - 17:00
Talk

Axiomatic Semantics for Compiler Verification

Steven Schäfer, Sigurd Schneider, Gert Smolka

18:00 - 21:00: CPP - CPP Reception, sponsored by the DeepSpec project at Room St Petersburg I

18:00 - 21:00
Social Event

CPP Reception, sponsored by the DeepSpec project

Mon 18 Jan 2016


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30
Room St Petersburg II	CPP Session 1: Invited talk by Harvey Friedman 09:00 - 10:00																		CPP Session 2: Verifying Imperative Programs 10:30 - 12:00																																										CPP Session 3: Design and Implementation of Theorem Provers 14:00 - 15:30																								CPP Session 4: Mathematics 16:00 - 18:00

Tue 19 Jan 2016


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30						19:00						30						20:00						30						21:00						30
Room St Petersburg I																																																																	CPP CPP Reception, sponsored by the DeepSpec project 18:00 - 21:00
Room St Petersburg II	CPP Session 5: Invited talk by Leonardo de Moura 09:00 - 10:00																		CPP Session 6: Foundations 10:30 - 12:00																																										CPP Session 7: Verification for Concurrent and Distributed Systems 14:00 - 15:30																								CPP Session 8: Compiler Verification 16:00 - 17:00

Mon 18 Jan 2016


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45			18:00			15			30			45
Room St Petersburg II	CPP Perspectives on Formal Verfication 09:00 - 10:00																		CPP Higher-order Representation Predicates in Separation Logic 10:30 - 11:00						CPP A Unified Coq Framework for Verifying C Programs with Floating-Point Co ... 11:00 - 11:30						CPP Refinement Based Verification of Imperative Data Structures 11:30 - 12:00																														CPP The Vampire and the FOOL 14:00 - 14:30						CPP Improving automation in interactive theorem provers by efficient encodi ... 14:30 - 15:00						CPP Mizar Environment for Isabelle 15:00 - 15:30												CPP A Modular, Efficient Formalisation of Real Algebraic Numbers 16:00 - 16:30						CPP Formal proofs of transcendence for e and pi as an application of multiv ... 16:30 - 17:00						CPP Formalizing Jordan Normal Forms in Isabelle/HOL 17:00 - 17:30						CPP Formalization of a Newton series representation of polynomials 17:30 - 18:00

Tue 19 Jan 2016


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45			18:00			15			30			45			19:00			15			30			45			20:00			15			30			45			21:00			15			30			45
Room St Petersburg I																																																																	CPP CPP Reception, sponsored by the DeepSpec project 18:00 - 21:00
Room St Petersburg II	CPP Dependent Type Practice 09:00 - 10:00																		CPP A Logic of Proofs for Differential Dynamic Logic 10:30 - 11:00						CPP Constructing the Propositional Truncation using Non-recursive HITs 11:00 - 11:30						CPP A Nominal Exploration of Intuitionism 11:30 - 12:00																														CPP Bisimulation Up-to Techniques for Psi-calculi 14:00 - 14:30						CPP Planning for Change in a Formal Verification of the Raft Consensus Protocol 14:30 - 15:00						CPP A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules 15:00 - 15:30												CPP Formal Verification of Control-flow Graph Flattening 16:00 - 16:30						CPP Axiomatic Semantics for Compiler Verification 16:30 - 17:00

iCalendar subscription service for your personal schedule

You first need to have starred events () in order to use the iCalendar subscription service.

Currently Viewed Program

Downloads the currently viewed program (with filters applied) in iCal format