Solving Constrained Horn Clauses (CHC) is necessitated by numerous fields in formal methods, from verifying software and smart contracts to modeling systems, yet the competitive scene for academic tools remains fairly sparse, especially compared to more popular fields such as software verification. Comparative evaluation as a competition, such as SV-COMP or CHC-COMP, sparks a more cohesive community around fields in formal methods. Lately, a trend has been emerging with tools such as Btor2C that bridge multiple fields together, thus widening this cohesion. Following that example, we propose and perform an experiment, where we use CHC-to-C transformation to apply software verification tools to linear CHC problems. In the process, we help both fields by diversifying the scene of CHC solvers and providing new and valuable benchmarks to aid the development of software verification tools. Using these benchmarks, we uncovered a previously hidden bug in multiple verification tools that can lead to false positive results. By analysing the results of the experiment, we can confidently make a recommendation for developers of software verifiers to consider supporting CHCs via our pre-verification transformation.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Solving Constrained Horn Clauses as C Programs with CHC2C


    Weitere Titelangaben:

    Lect.Notes Computer


    Beteiligte:
    Neele, Thomas (Herausgeber:in) / Wijs, Anton (Herausgeber:in) / Bajczi, Levente (Autor:in) / Molnár, Vince (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 : 8 ; 146-163


    Erscheinungsdatum :

    13.10.2024


    Format / Umfang :

    18 pages





    Medientyp :

    Aufsatz/Kapitel (Buch)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    Uncertainty-valued horn clauses

    Hall, Victoria | TIBKAT | 1994

    Freier Zugriff

    Uncertainty-valued horn clauses

    Hall, Victoria | TIBKAT | 1994


    A sharp threshold for the phase transition of a restricted Satisfiability problem for Horn clauses

    Dunne, P. E. / Bench-Capon, T. J. M. | British Library Online Contents | 2001


    Aerospace Contract Clauses

    SAE Technical Papers | 2006


    Aerospace Contract Clauses

    SAE Technical Papers | 2017