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.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Augmenting Interpolation-Based Model Checking with Auxiliary Invariants


    Weitere Titelangaben:

    Lect.Notes Computer


    Beteiligte:
    Neele, Thomas (Herausgeber:in) / Wijs, Anton (Herausgeber:in) / Beyer, Dirk (Autor:in) / Chien, Po-Chun (Autor:in) / Lee, Nian-Ze (Autor:in)

    Kongress:

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


    Erschienen in:

    Model Checking Software ; Kapitel : 13 ; 227-247


    Erscheinungsdatum :

    13.10.2024


    Format / Umfang :

    21 pages





    Medientyp :

    Aufsatz/Kapitel (Buch)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    Elevator checking video auxiliary system

    WANG XIAOQIAO / KOU YANFEI / SUN NAN | Europäisches Patentamt | 2020

    Freier Zugriff

    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. | Europäisches Patentamt | 2024

    Freier Zugriff

    Thrust Augmenting Ejectors

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