Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including k-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.


    Access

    Download


    Export, share and cite



    Title :

    Augmenting Interpolation-Based Model Checking with Auxiliary Invariants


    Additional title:

    Lect.Notes Computer


    Contributors:
    Neele, Thomas (editor) / Wijs, Anton (editor) / Beyer, Dirk (author) / Chien, Po-Chun (author) / Lee, Nian-Ze (author)

    Conference:

    International Symposium on Model Checking Software ; 2024 ; Luxembourg City, Luxembourg April 10, 2024 - April 11, 2024


    Published in:

    Model Checking Software ; Chapter : 13 ; 227-247


    Publication date :

    2024-10-13


    Size :

    21 pages





    Type of media :

    Article/Chapter (Book)


    Type of material :

    Electronic Resource


    Language :

    English




    Elevator checking video auxiliary system

    WANG XIAOQIAO / KOU YANFEI / SUN NAN | European Patent Office | 2020

    Free access

    Augmenting Corner Descriptors

    Rosin, P. L. | British Library Online Contents | 1996


    Thrust Augmenting Ejectors

    H. Viets | NTIS | 1975


    Auxiliary device for checking green channel of highway toll station

    CHANG XU / ZHANG LI / YANG HUI et al. | European Patent Office | 2024

    Free access

    Thrust Augmenting Ejectors

    M. Alperin / J. J. Wu | NTIS | 1981