Program - CPP 2016

Time Zone

The program is currently displayed in (GMT-05:00) Guadalajara, Mexico City, Monterrey.

Use conference time zone: (GMT-05:00) Guadalajara, Mexico City, MonterreySelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

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 - 10:00 Talk		Perspectives on Formal Verfication CPP Harvey FriedmanOhio State University

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

	10:30 - 11:00 Talk		Higher-order Representation Predicates in Separation Logic CPP Arthur Charguéraud
	11:00 - 11:30 Talk		A Unified Coq Framework for Verifying C Programs with Floating-Point Computations CPP Tahina Ramananandro, Paul Mountcastle, Benoit Meister, Richard Lethin
	11:30 - 12:00 Talk		Refinement Based Verification of Imperative Data Structures CPP Peter LammichTechnische Universität München

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

	14:00 - 14:30 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 - 15:00 Talk		Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions CPP Lukasz CzajkaUniversity of Innsbruck
	15:00 - 15:30 Talk		Mizar Environment for Isabelle CPP Cezary KaliszykUniversity of Innsbruck, Karol PąkUniversity of Bialystok, Institute of Computer Science, Josef Urban

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

	16:00 - 16:30 Talk		A Modular, Efficient Formalisation of Real Algebraic Numbers CPP Wenda LiUniversity of Cambridge, Lawrence PaulsonCambridge University
	16:30 - 17:00 Talk		Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials CPP Sophie BernardINRIA, Yves BertotINRIA, Laurence RideauINRIA, Pierre-Yves StrubIMDEA Software Institute
	17:00 - 17:30 Talk		Formalizing Jordan Normal Forms in Isabelle/HOL CPP René ThiemannUniversity of Innsbruck, Akihisa Yamada
	17:30 - 18:00 Talk		Formalization of a Newton series representation of polynomials CPP Cyril Cohen, Boris DjalalINRIA

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 - 10:00 Talk		Dependent Type Practice CPP Leonardo De MouraMicrosoft Research, Redmond

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

	10:30 - 11:00 Talk		A Logic of Proofs for Differential Dynamic Logic CPP Nathan FultonCarnegie Mellon University, André Platzer
	11:00 - 11:30 Talk		Constructing the Propositional Truncation using Non-recursive HITs CPP Floris van DoornCarnegie Mellon University
	11:30 - 12:00 Talk		A Nominal Exploration of Intuitionism CPP Vincent RahliSnT, Mark BickfordCornell University

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

	14:00 - 14:30 Talk		Bisimulation Up-to Techniques for Psi-calculi CPP Johannes Å. PohjolaUppsala University, Joachim ParrowUppsala University
	14:30 - 15:00 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 - 15:30 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 - 16:30 Talk		Formal Verification of Control-flow Graph Flattening CPP Sandrine BlazyIRISA / University of Rennes 1, Alix TrieuENS Rennes
	16:30 - 17:00 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 - 21:00 Social Event		CPP Reception, sponsored by the DeepSpec project CPP

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


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
Room St Petersburg II	CPP Session 1: Invited talk by Harvey Friedman																		CPP Session 2: Verifying Imperative Programs																																										CPP Session 3: Design and Implementation of Theorem Provers																								CPP Session 4: Mathematics

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


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
Room St Petersburg I												CPP CPP Reception, sponsored by the DeepSpec project
Room St Petersburg II	CPP Session 5: Invited talk by Leonardo de Moura			CPP Session 6: Foundations							CPP Session 7: Verification for Concurrent and Distributed Systems					CPP Session 8: Compiler Verification

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


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
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
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


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
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

CPP 2016 Program

Filter Program

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

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

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

CPP

CPP

CPP

CPP

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

CPP

CPP

CPP

CPP

CPP

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

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

Tracks

CPP 2016 Program

Filter Program

Program Display Configuration

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

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

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

CPP

CPP

CPP

CPP

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

CPP

CPP

CPP

CPP

CPP

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

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

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

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

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

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

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

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