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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Solving Constrained Horn Clauses as C Programs with CHC2C


    Additional title:

    Lect.Notes Computer


    Contributors:

    Conference:

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


    Published in:

    Model Checking Software ; Chapter : 8 ; 146-163


    Publication date :

    2024-10-13


    Size :

    18 pages





    Type of media :

    Article/Chapter (Book)


    Type of material :

    Electronic Resource


    Language :

    English




    Uncertainty-valued horn clauses

    Hall, Victoria | TIBKAT | 1994

    Free access

    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