Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised, but established results and errors need not be~reachable. OX function specifications are thus incompatible with true bug-finding supported by symbolic execution tools such as Pulse and Pulse-X. In contrast, under-approximating (UX) program logics, such as incorrectness separation logic, are used to find true results and bugs: established results and errors are reachable, but there is no mechanism for understanding if all terminating behaviour has been characterised.
We introduce exact separation logic (ESL), which provides fully-verified function specifications compatible with both OX verification and UX true bug-funding: all terminating behaviour is characterised, and all established results and errors are reachable. We prove soundness for ESL with mutually recursive functions, demonstrating, for the first time, function compositionality for a UX logic. We show that UX program logics require subtle definitions of internal and external function specifications compared with the familiar definitions of OX logics. We investigate the expressivity of ESL and, for the first time, explore the role of abstraction in UX reasoning by verifying abstract ESL specifications of various data-structure algorithms. In doing so, we highlight the difference between abstraction (hiding information) and over-approximation (losing information). Our findings demonstrate that, expectedly, abstraction cannot be used as freely in UX logics as in OX logics, but also that it should be feasible to use ESL to provide tractable function specifications for self-contained, critical code, which would then be used for both verification and true bug-finding.
Fri 21 JulDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00
|On using VeriFast, VerCors, Plural, and KeY to check object usage|
João Mota NOVA School of Science and Technology, António Ravara NOVA LINCS & FCT, NOVA University of Lisbon, Marco Giunti NOVA-LINCS, FCT NOVA / Universidade Nova de LisboaDOI
|Exact Separation Logic|
Petar Maksimović Imperial College London, UK, Caroline Cronjäger Ruhr-Universität Bochum, Andreas Lööw Imperial College London, Julian Sutherland Imperial College London, Philippa Gardner Imperial College LondonDOI Pre-print
|Morpheus: Automated Safety Verification of Data-dependent Parser Combinator Programs|
|Constraint Based Compiler Optimization for Energy Harvesting Applications|
|Dynamic Determinacy Race Detection for Task-Parallel Programs with Promises|
Feiyang Jin Georgia Institute of Technology, Lechen Yu Georgia Institute of Technology, Tiago Cogumbreiro University of Massachusetts Boston, Vivek Sarkar Georgia Institute of Technology, Jun Shirako Georgia Institute of TechnologyDOI
|On Leveraging Tests to Infer Nullable Annotations|
Jens Dietrich Victoria University of Wellington, David J. Pearce ConsenSys, Mahin Chandramohan Oracle LabsDOI