Compositional may-must program analysis: unleashing the power of alternation

DOI10.1145/1706299.1706307MaRDI QIDQ5255061zbMATH OpenOpenAlexFDO

Authors Patrice Godefroid, Aditya V. Nori, Sai Deep Tetali, 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 refinementdirected testingsoftware model checking

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

• scientific article; zbMATH DE number 2087567
• Compositional shape analysis by means of bi-abduction
• A framework for combining analysis and verification
• scientific article; zbMATH DE number 1693485
• Compositional shape analysis by means of bi-abduction

Cited in

(14)

• How testing helps to diagnose proof failures
• Demand-driven interprocedural analysis for map-based abstract domains
• Backward symbolic execution with loop folding
• Reusing predicate precision in value analysis
• A two-phase approach for conditional floating-point verification
• Unbounded procedure summaries from bounded environments
• An abstraction-refinement framework for trigger querying
• Refinement checking on parametric modal transition systems
• Whale: an interpolation-based algorithm for inter-procedural verification
• Combining model checking and testing
• Formal testing for separation assurance
• SMT-based model checking for recursive programs
• Doomed program points
• Parallel program analysis via range splitting

Describes a project that uses

Uses Software

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

This page was built for publication: Compositional may-must program analysis: unleashing the power of alternation

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