Modular reasoning about heap paths via effectively propositional formulas

DOI10.1145/2535838.2535854zbMath1284.68403OpenAlexW1976401986MaRDI QIDQ5408433

Mooly Sagiv, Ori Lahav, Shachar Itzhaky, Aleksandar Nanevski, Anindya Banerjee

Publication date: 10 April 2014

Published in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2535838.2535854

zbMATH Keywords

verificationlinked listsmt

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (5)

A First-Order Logic with Frames ⋮ Property Directed Reachability for Proving Absence of Concurrent Modification Errors ⋮ From invariant checking to invariant inference using randomized search ⋮ What’s Decidable About Program Verification Modulo Axioms? ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates

Uses Software

• SMT-LIB
• Spec#
• z3

This page was built for publication: Modular reasoning about heap paths via effectively propositional formulas