Relational verification through Horn clause transformation

DOI10.1007/978-3-662-53413-7_8zbMath1394.68227OpenAlexW2512875025MaRDI QIDQ1664383

Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti

Publication date: 27 August 2018

Full work available at URL: https://doi.org/10.1007/978-3-662-53413-7_8

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (6)

Operationally-based program equivalence proofs using LCTRSs ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Unnamed Item ⋮ Relational program reasoning using compiler IR ⋮ Predicate Pairing for program verification ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates

This page was built for publication: Relational verification through Horn clause transformation