Verification-Preserving Inlining in Automatic Separation Logic Verifiers
Bounded verification has proved useful to detect bugs and to increase confidence in the correctness of a program. In contrast to unbounded verification, reasoning about calls via (bounded) inlining and about loops via (bounded) unrolling does not require method specifications and loop invariants and, therefore, reduces the annotation overhead to the bare minimum, namely specifications of the properties to be verified. For verifiers based on traditional program logics, verification is preserved by inlining (and unrolling): successful unbounded verification of a program w.r.t. some annotation implies successful verification of the inlined program. That is, any error detected in the inlined program reveals a true error in the original program. However, this essential property might not hold for automatic separation logic verifiers such as Caper, GRASShopper, RefinedC, Steel, VeriFast, and verifiers based on Viper. In this setting, inlining generally changes the resources owned by method executions, which may affect automatic proof search algorithms and introduce spurious errors.
In this paper, we present the first technique for verification-preserving inlining in automatic separation logic verifiers. We identify a semantic condition on programs and prove in Isabelle/HOL that it ensures verification-preserving inlining for state-of-the-art automatic separation logic verifiers. We also prove a dual result: successful verification of the inlined program ensures that there are method and loop annotations that enable the verification of the original program for bounded executions. To check our semantic condition automatically, we present two approximations that can be checked syntactically and with a program verifier, respectively. We implement these checks in Viper and demonstrate that they are effective for non-trivial examples from different verifiers.
Fri 27 OctDisplayed time zone: Lisbon change
16:00 - 17:30
|Verification-Preserving Inlining in Automatic Separation Logic Verifiers|
|Leaf: Modularity for Temporary Sharing in Separation Logic|
Travis Hance Carnegie Mellon University, Jon Howell VMware Research, Oded Padon VMware Research, Bryan Parno Carnegie Mellon UniversityDOI
|Proof Automation for Linearizability in Separation Logic|
|Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic|
Jaehwang Jung KAIST, Janggun Lee KAIST, Jaemin Choi KAIST, Jaewoo Kim KAIST, Sunho Park KAIST, Jeehoon Kang KAISTDOI
|Functional collection programming with semi-ring dictionaries|
Amir Shaikhha University of Edinburgh, Mathieu Huot University of Oxford, Jaclyn Smith Oxford University, Dan Olteanu University of ZurichLink to publication DOI