Relational verification via invariant-guided synchronization

MaRDI QIDQ5016382zbMATH OpenFDO

Authors

Publication date 13 December 2021

Full work available at URL https://arxiv.org/abs/1907.03997, http://eptcs.web.cse.unsw.edu.au/paper.cgi?HCVSPERR2019.6

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Exploiting synchrony and symmetry in relational verification
• Property directed equivalence via abstract simulation
• Relational verification through Horn clause transformation
• Relational logic with framing and hypotheses
• Certified verification of relational properties

Cites work

• Automating induction for solving Horn clauses
• Beyond 2-safety: asymmetric product programs for relational program verification
• Exploiting synchrony and symmetry in relational verification
• Product programs and relational program logics
• Relational decomposition
• Relational logic with framing and hypotheses
• Relational program reasoning using compiler IR
• Secure information flow by self-composition
• Static Analysis
• Towards modularly comparing programs using automated theorem provers

Cited in

(6)

• Relational program reasoning using compiler IR
• Certified verification of relational properties
• Bridging arrays and ADTs in recursive proofs
• Property directed equivalence via abstract simulation
• Exploiting synchrony and symmetry in relational verification
• Analysis and Transformation of Constrained Horn Clauses for Program Verification

This page was built for publication: Relational verification via invariant-guided synchronization

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