HSF(C): A Software Verifier based on Horn Clauses. SF is a framework that automates verification of programs. HSF(C) is the instantiation of HSF for verification of C programs. HSF(C) is based on predicate abstraction and refinement following the CEGAR paradigm. There are a number of successful tools including SLAM, Blast, ARMC and CPAChecker that are also based on abstraction refinement. By using abstraction refinement, HSF(C) finds auxiliary assertions required for proving software properties automatically.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Beyene, Tewodros; Chaudhuri, Swarat; Popeea, Corneliu; Rybalchenko, Andrey: A constraint-based approach to solving games on infinite graphs (2014)
- De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio: Verifying array programs by transforming verification conditions (2014)
- Larraz, Daniel; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: Minimal-model-guided approaches to solving polynomial constraints and extensions (2014)
- De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio: Specialization with constrained generalization for software model checking (2013)
- Popeea, Corneliu; Rybalchenko, Andrey: Threader: a verifier for multi-threaded programs. (Competition contribution) (2013)
- Flanagan, Cormac (ed.); König, Barbara (ed.): Tools and algorithms for the construction and analysis of systems. 18th international conference, TACAS 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 -- April 1, 2012. Proceedings (2012)
- Grebenshchikov, Sergey; Gupta, Ashutosh; Lopes, Nuno P.; Popeea, Corneliu; Rybalchenko, Andrey: HSF(C): a software verifier based on Horn clauses (competition contribution) (2012)