The SeaHorn verification framework. In this paper, we present SeaHorn, a software verification framework. The key distinguishing feature of SeaHorn is its modular design that separates the concerns of the syntax of the programming language, its operational semantics, and the verification semantics. SeaHorn encompasses several novelties: it (a) encodes verification conditions using an efficient yet precise inter-procedural technique, (b) provides flexibility in the verification semantics to allow different levels of precision, (c) leverages the state-of-the-art in software model checking and abstract interpretation for verification, and (d) uses Horn-clauses as an intermediate language to represent verification conditions which simplifies interfacing with multiple verification tools based on Horn-clauses. SeaHorn provides users with a powerful verification tool and researchers with an extensible and customizable framework for experimenting with new software verification techniques. The effectiveness and scalability of SeaHorn are demonstrated by an extensive experimental evaluation using benchmarks from SV-COMP 2015 and real avionics code.
Keywords for this software
References in zbMATH (referenced in 11 articles )
Showing results 1 to 11 of 11.
- Meseguer, José: Generalized rewrite theories, coherence completion, and symbolic methods (2020)
- Beyer, Dirk; Dangl, Matthias; Wendler, Philipp: A unifying view on SMT-based software verification (2018)
- Kafle, Bishoksan; Gallagher, John P.; Gange, Graeme; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.: An iterative approach to precondition inference using constrained Horn clauses (2018)
- Kiefer, Moritz; Klebanov, Vladimir; Ulbrich, Mattias: Relational program reasoning using compiler IR (2018)
- Lucas, Salvador; Gutiérrez, Raúl: Automatic synthesis of logical models for order-sorted first-order theories (2018)
- Kafle, Bishoksan; Gallagher, John P.: Horn clause verification with convex polyhedral abstraction and tree automata-based refinement (2017)
- Wang, Wei; Barrett, Clark; Wies, Thomas: Partitioned memory models for program analysis (2017)
- Gange, Graeme; Navas, Jorge A.; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.: An abstract domain of uninterpreted functions (2016)
- Strichman, Ofer; Veitsman, Maor: Regression verification for unbalanced recursive functions (2016)
- Tan, Jiaqi; Tay, Hui Jun; Gandhi, Rajeev; Narasimhan, Priya: AUSPICE-R: automatic safety-property proofs for realistic features in machine code (2016)
- Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey: Horn clause solvers for program verification (2015)