salle A. Turing CE4
14 octobre 2014 - 14h00
Static Analysis Modulo Theory
par Andreas Podelski de University of Freiburg
Abstract: We present a new approach to program verification. We call it Static Analysis Modulo Theory in analogy with SMT solving. Satisfiability here corresponds to the existence of an error path in the program, or: unsatisfiability corresponds to the emptiness of an automaton. Each time the tool finds an error path, i.e., a word accepted by the automaton, it analyzes the word in the theory of the data domain. If the word is infeasible, it learns a new automaton which rejects the word (and many others). It then adds the new automaton to the intersection of the already existing automata. The emptiness check for the resulting intersection of automata corresponds to a static analysis over a theory-free abstract domain. The approach has been implemented in the tool Ultimate Automizer. It has been extended to procedural (possibly recursive) programs and concurrent (multi-threaded) programs (with a bounded or with an unbounded number of threads), and to termination (for procedural (possibly recursive) programs).
Joint work with Matthias Heizmann and Jochen Hoenicke and joint work with Azadeh Farzan and Zachary Kincaid.
