Semi-Automated Reasoning About Non-Determinism in C Expressions
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
10:30 - 12:30: ESOP 2019 - Program Verification at SUN II Chair(s): Luís CairesNOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa | ||||||||||||||||||||||||||||||||||||||||||
10:30 - 11:00 Talk | Link to publication | |||||||||||||||||||||||||||||||||||||||||
11: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 | |||||||||||||||||||||||||||||||||||||||||
11:30 - 12:00 Talk | Dan FruminRadboud University, Léon GondelmanLRI, Université Paris-Sud, Robbert KrebbersDelft University of Technology Link to publication | |||||||||||||||||||||||||||||||||||||||||
12:00 - 12:30 Talk | Michael Peyton JonesIOHK, Mario Alvarez-PicalloUniversity of Oxford, Alexander Eyers-TaylorSemmle, C.-H. Luke OngUniversity of Oxford Link to publication |