Predicate pairing with abstraction for relational verification

DOI10.1007/978-3-319-94460-9_17MaRDI QIDQ1671163zbMATH OpenOpenAlexFDO

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

Publication date 6 September 2018

Full work available at URL https://arxiv.org/abs/1709.04809

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Predicate pairing for program verification
• Relational verification through Horn clause transformation
• Constraint-based relational verification
• Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
• Relational logic with framing and hypotheses

Cited in

(7)

• Constraint-based relational verification
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• Predicate pairing for program verification
• Predicate signatures from pair encodings via dual system proof technique
• scientific article; zbMATH DE number 2000443 (Why is no real title available?)
• Relational verification through Horn clause transformation
• Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification

This page was built for publication: Predicate pairing with abstraction for relational verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1671163)