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

esop-2019-papers
10:30 - 12:30: ESOP 2019 - Program Verification at SUN II
Chair(s): Luís CairesNOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
esop-2019-papers10:30 - 11:00
Talk
Glen Mével, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, François PottierInria, France
Link to publication
esop-2019-papers11:00 - 11:30
Talk
Guido MartínezCIFASIS-CONICET, Argentina, Danel AhmanUniversity of Ljubljana, Victor DumitrescuNomadic Labs Paris, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Cătălin HriţcuInria Paris, Monal NarasimhamurthyUniversity of Colorado, Boulder, Zoe ParaskevopoulouPrinceton University, Clément Pit-ClaudelMIT CSAIL, Jonathan ProtzenkoMicrosoft Research, Redmond, Tahina RamananandroMicrosoft Research, n.n., Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research
Link to publication
esop-2019-papers11:30 - 12:00
Talk
Dan FruminRadboud University, Léon GondelmanLRI, Université Paris-Sud, Robbert KrebbersDelft University of Technology
Link to publication
esop-2019-papers12:00 - 12:30
Talk
Michael Peyton JonesIOHK, Mario Alvarez-PicalloUniversity of Oxford, Alexander Eyers-TaylorSemmle, C.-H. Luke OngUniversity of Oxford
Link to publication