ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Mon 8 Apr 2019 11:30 - 12:00 at SUN II - Program Verification Chair(s): Luís Caires

Research into C verification often ignores that the C standard leaves the evaluation order of expressions unspecified, and assigns undefined behavior to write-write or read-write conflicts in subexpressions—so called ``sequence point violations''. These aspects should be accounted for in verification because C compilers exploit them. We present a verification condition generator (vcgen) that enables one to semi-automatically prove the absence of undefined behavior in a given C program for any evaluation order. The key novelty in our approach is a symbolic execution algorithm that computes a frame at the same time as a postcondition. The frame is used to automatically determine how resources should be distributed among subexpressions. We prove correctness of our vcgen with respect to a new monadic definitional semantics of a subset of C. This semantics is modular and gives a concise account of non-determinism in C. We have implemented our vcgen as a tactic in the Coq interactive theorem prover, and have proved correctness of it using a separation logic for a new monadic definitional semantics of a subset of C.

Mon 8 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30
Program VerificationESOP at SUN II
Chair(s): Luís Caires NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
10:30
30m
Talk
Time Credits and Time Receipts in Iris
ESOP
Glen Mével , Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, François Pottier Inria, France
Link to publication
11:00
30m
Talk
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
ESOP
Guido Martínez CIFASIS-CONICET, Argentina, Danel Ahman University of Ljubljana, Victor Dumitrescu Nomadic Labs Paris, Nick Giannarakis Princeton University, Chris Hawblitzel Microsoft Research, Cătălin Hriţcu Inria Paris, Monal Narasimhamurthy University of Colorado, Boulder, Zoe Paraskevopoulou Princeton University, Clément Pit-Claudel MIT CSAIL, Jonathan Protzenko Microsoft Research, Redmond, Tahina Ramananandro Microsoft Research, n.n., Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research
Link to publication
11:30
30m
Talk
Semi-Automated Reasoning About Non-Determinism in C Expressions
ESOP
Dan Frumin Radboud University, Léon Gondelman LRI, Université Paris-Sud, Robbert Krebbers Delft University of Technology
Link to publication
12:00
30m
Talk
Fixing Incremental Computation: Derivatives of fixpoints, and the recursive semantics of Datalog
ESOP
Michael Peyton Jones IOHK, Mario Alvarez-Picallo University of Oxford, Alexander Eyers-Taylor Semmle, C.-H. Luke Ong University of Oxford
Link to publication