K. L. McMillan
ABSTRACT
Relevance heuristics allow us to tailor a program analysis to a particular property to be verified. This in turn makes it possible to improve the precision of the analysis where needed, while maintaining scalability. In this talk I will discuss the principles by which SAT solvers and other decision procedures decide what information is relevant to a given proof. Then we will see how these ideas can be exploited in program verification using the method of Craig interpolation. The result is an analysis that is finely tuned to prove a given property of a program. At the end of the talk, I will cover some recent research in this area, including the use of interpolants for verifying heap-manipulating programs.
Index Terms
- Relevance heuristics for program analysis
Recommendations
Relevance heuristics for program analysis
POPL '08Relevance heuristics allow us to tailor a program analysis to a particular property to be verified. This in turn makes it possible to improve the precision of the analysis where needed, while maintaining scalability. In this talk I will discuss the ...
SAT-based Abstraction Refinement for Real-time Systems
In this paper, we present an abstraction refinement approach for model checking safety properties of real-time systems using SAT-solving. We present a faithful embedding of bounded model checking for systems of timed automata into propositional logic ...
Finding feasible abstract counter-examples
A strength of model checking is its ability to automate the detection of subtle system errors and produce traces that exhibit those errors. Given the high-computational cost of model checking most researchers advocate the use of aggressive property-...
Comments