VeriMAP

VeriMAP: Transformation-aided Horn Clause Verification. VeriMAP is a tool for supporting CHC software verifiers. VeriMAP is capable of: (i) generating the CHC encoding of a verification problem, and (ii) improving the effectiveness and the efficiency of CHC solvers by applying transformations of CHCs. The tool is, to a large extent, parametric with respect to the languages in which the program and the property to be verified are written, and allows the user to take advantage of the very effective techniques and tools that have been developed in the fields of constraint logic programming and SMT solving


References in zbMATH (referenced in 11 articles , 1 standard article )

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

  1. Garcia-Contreras, Isabel; Morales, José F.; Hermenegildo, Manuel V.: Incremental and modular context-sensitive analysis (2021)
  2. Bohlender, Dimitri; Kowalewski, Stefan: Leveraging Horn clause solving for compositional verification of PLC software (2020)
  3. De Angelis, Emanuele; Fioravanti, Fabio; Proietti, Maurizio: Transformational verification of Quicksort (2020)
  4. Mastria, Elena; Zangari, Jessica; Perri, Simona; Calimeri, Francesco: A machine learning guided rewriting approach for ASP logic programs (2020)
  5. Kafle, Bishoksan; Gallagher, John P.: Horn clause verification with convex polyhedral abstraction and tree automata-based refinement (2017)
  6. De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio: Removing unnecessary variables from Horn clause verification conditions (2016)
  7. Kafle, Bishoksan; Gallagher, John P.; Ganty, Pierre: Solving non-linear Horn clauses using a linear Horn clause solver (2016)
  8. Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey: Horn clause solvers for program verification (2015)
  9. De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio: Proving correctness of imperative programs by linearizing constrained Horn clauses (2015)
  10. Gange, Graeme; Navas, Jorge A.; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.: Horn clauses as an intermediate representation for program analysis and transformation (2015)
  11. De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio: Verimap: A tool for verifying programs through transformations (2014) ioport