HSF

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.


References in zbMATH (referenced in 12 articles )

Showing results 1 to 12 of 12.
Sorted by year (citations)

  1. Garcia-Contreras, Isabel; Morales, José F.; Hermenegildo, Manuel V.: Incremental and modular context-sensitive analysis (2021)
  2. Lopez-Garcia, P.; Darmawan, L.; Klemen, M.; Liqat, U.; Bueno, F.; Hermenegildo, M. V.: Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption (2018)
  3. Kafle, Bishoksan; Gallagher, John P.: Horn clause verification with convex polyhedral abstraction and tree automata-based refinement (2017)
  4. Beyene, Tewodros A.; Popeea, Corneliu; Rybalchenko, Andrey: Efficient CTL verification via Horn constraints solving (2016)
  5. Kafle, Bishoksan; Gallagher, John P.; Ganty, Pierre: Solving non-linear Horn clauses using a linear Horn clause solver (2016)
  6. Beyene, Tewodros; Chaudhuri, Swarat; Popeea, Corneliu; Rybalchenko, Andrey: A constraint-based approach to solving games on infinite graphs (2014)
  7. De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio: Verifying array programs by transforming verification conditions (2014)
  8. Larraz, Daniel; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: Minimal-model-guided approaches to solving polynomial constraints and extensions (2014)
  9. De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio: Specialization with constrained generalization for software model checking (2013)
  10. Popeea, Corneliu; Rybalchenko, Andrey: Threader: a verifier for multi-threaded programs. (Competition contribution) (2013) ioport
  11. 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)
  12. Grebenshchikov, Sergey; Gupta, Ashutosh; Lopes, Nuno P.; Popeea, Corneliu; Rybalchenko, Andrey: HSF(C): a software verifier based on Horn clauses (competition contribution) (2012) ioport