Program analysis via satisfiability modulo path programs

DOI10.1145/1706299.1706309MaRDI QIDQ5255063zbMATH OpenOpenAlexFDO

Authors William R. Harris, Sriram Sankaranarayanan, Franjo Ivančić, Aarti Gupta

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 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.183.906

zbMATH Keywords

abstract interpretationpath sensitivityprogram analysissatisfiability solversSMT solverssymbolic execution

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Programming Languages and Systems
• Dynamic Path Reduction for Software Model Checking
• Counterexample guided path reduction for static program analysis
• Randomized resource-aware path-sensitive static analysis
• Back to the future, revisiting precise program verification using SMT solvers

Cited in

(13)

• A framework for memory efficient context-sensitive program analysis
• Backward symbolic execution with loop folding
• Abstract interpretation as automated deduction
• Model Checking MSVL Programs Based on Dynamic Symbolic Execution
• Abstract Interpretation as Automated Deduction
• Randomized resource-aware path-sensitive static analysis
• SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement
• Deciding floating-point logic with abstract conflict driven clause learning
• Paths vs. trees in set-based program analysis
• Program Analysis Using Weighted Pushdown Systems
• Programming Languages and Systems
• A slice-based decision procedure for type-based partial orders
• Analyzing mathematical programs using MProbe

This page was built for publication: Program analysis via satisfiability modulo path programs

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