Back to the future

DOI10.1145/1328438.1328461zbMath1295.68087OpenAlexW1979619055MaRDI QIDQ3189836

Shuvendu K. Lahiri, Shaz Qadeer

Publication date: 12 September 2014

Published in: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

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

zbMATH Keywords

reachabilitylinked listssoftware verificationSMT solversdecision proceduresheap-manipulating programs

Mathematics Subject Classification ID

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

Related Items (18)

Local Reasoning for Global Graph Properties ⋮ Verification of heap manipulating programs with ordered data by extended forest automata ⋮ Decision Procedure for Entailment of Symbolic Heaps with Arrays ⋮ A Logic-Based Framework for Reasoning about Composite Data Structures ⋮ Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ Unnamed Item ⋮ Partitioned Memory Models for Program Analysis ⋮ Symbolic predictive analysis for concurrent programs ⋮ Complete instantiation-based interpolation ⋮ Parametrized invariance for infinite state processes ⋮ Bounded Quantifier Instantiation for Checking Inductive Invariants ⋮ DKAL and Z3: A Logic Embedding Experiment ⋮ Complexity and Algorithms for Monomial and Clausal Predicate Abstraction ⋮ An Efficient Decision Procedure for Imperative Tree Data Structures ⋮ A shape graph logic and a shape system ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification ⋮ Decidable fragments of many-sorted logic ⋮ SGGS decision procedures

Uses Software

• Spec#
• z3
• SIMPLIFY
• DART
• TVLA

This page was built for publication: Back to the future