Compositional may-must program analysis

DOI10.1145/1706299.1706307zbMath1312.68057OpenAlexW2134875273MaRDI QIDQ5255061

Patrice Godefroid, Sai Deep Tetali, Aditya V. Nori, Sriram K. Rajamani

Publication date: 11 June 2015

Published in: Proceedings of the 37th 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/1706299.1706307

zbMATH Keywords

abstraction refinementsoftware model checkingdirected testing

Mathematics Subject Classification ID

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

Related Items (13)

Whale: An Interpolation-Based Algorithm for Inter-procedural Verification ⋮ How testing helps to diagnose proof failures ⋮ Combining Model Checking and Testing ⋮ Backward symbolic execution with loop folding ⋮ Reusing predicate precision in value analysis ⋮ Doomed program points ⋮ Formal testing for separation assurance ⋮ A two-phase approach for conditional floating-point verification ⋮ Unbounded procedure summaries from bounded environments ⋮ SMT-based model checking for recursive programs ⋮ An abstraction-refinement framework for trigger querying ⋮ Demand-driven interprocedural analysis for map-based abstract domains ⋮ Refinement checking on parametric modal transition systems

Uses Software

• z3
• DART
• Bebop
• YASM
• CCured
• YOGI

This page was built for publication: Compositional may-must program analysis