Back to the future, revisiting precise program verification using SMT solvers

DOI10.1145/1328438.1328461MaRDI QIDQ3189836zbMATH OpenOpenAlexFDO

Authors 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

reachabilitydecision proceduresSMT solverssoftware verificationlinked listsheap-manipulating programs

Mathematics Subject Classification ID

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

Recommendations

• Verifying Heap-Manipulating Programs in an SMT Framework
• Separation logic modulo theories
• Satisfiability modulo heap-based programs
• Solving quantified verification conditions using satisfiability modulo theories
• Modular reasoning about heap paths via effectively propositional formulas

Cited in

(29)

• Verifying Heap-Manipulating Programs in an SMT Framework
• scientific article; zbMATH DE number 7350781 (Why is no real title available?)
• An efficient decision procedure for imperative tree data structures
• Symbolic predictive analysis for concurrent programs
• Bounded quantifier instantiation for checking inductive invariants
• Verification of heap manipulating programs with ordered data by extended forest automata
• Decision Procedure for Entailment of Symbolic Heaps with Arrays
• Local reasoning for global graph properties
• Complete instantiation-based interpolation
• The decision problem for undirected graphs with reachability and acyclicity
• Decidable fragments of many-sorted logic
• SMT-based verification of program changes through summary repair
• Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
• DKAL and Z3: a logic embedding experiment
• A shape graph logic and a shape system
• Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
• Partitioned memory models for program analysis
• Program analysis via satisfiability modulo path programs
• Function summarization modulo theories
• Proof-Guided Underapproximation Widening for Bounded Model Checking
• A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness
• Parametrized invariance for infinite state processes
• Relevance heuristics for program analysis
• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• Distributed bounded model checking
• Dafny: an automatic program verifier for functional correctness
• Invariants synthesis over a combined domain for automated program verification
• SGGS decision procedures
• A Logic-Based Framework for Reasoning about Composite Data Structures

Describes a project that uses

Uses Software

• TVLA
• DART
• SIMPLIFY
• z3
• Spec#

This page was built for publication: Back to the future, revisiting precise program verification using SMT solvers

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