Semi-automated Reasoning About Non-determinism in C Expressions

Title

Semi-automated Reasoning About Non-determinism in C Expressions

 Author

Frumin, Dan (Radboud Universiteit Nijmegen)
Gondelman, Léon (Radboud Universiteit Nijmegen)
Krebbers, R.J. (TU Delft Programming Languages)

Contributor

Caires, Luís (editor)

Date

2019

 Abstract

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 of 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 the new monadic definitional semantics of a subset of C.

 To reference this document use:

http://resolver.tudelft.nl/uuid:56864c67-0400-44a3-857b-8f4f2c9754db

 DOI

https://doi.org/10.1007/978-3-030-17184-1_3

 Publisher

Springer, Cham

 ISBN

978-3-030-17183-4

 Source

Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings

 Event

28th European Symposium on Programming, ESOP 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, 2019-04-06 → 2019-04-11, Prague, Czech Republic

 Series

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 0302-9743, 11423 LNCS

 Part of collection

Institutional Repository

 Document type

conference paper

 Rights

© 2019 Dan Frumin, Léon Gondelman, R.J. Krebbers
Files
PDF Frumin2019_Chapter_Semi_a ... boutNo.pdf 901.45 KB
Close viewer