Property Directed Abstract Interpretation

Directed Abstract Interpretation Noam Rinetzky1 and Sharon Shoham2 1 Tel Aviv University, Israel 2 The Academic College of Tel Aviv Yaffo, Israel Recently, Bradley proposed the PDR/IC3 model checking algorithm for verifying safety properties, where forward and backward reachability analyses are intertwined, and guide each other. Many variants of Bradley’s original algorithm have been developed and successfully applied to both hardware and software verification. However, these algorithms have been presented in an operational manner, in disconnect with the rich literature concerning the theoretical on of static analysis formulated by abstract interpretation. Inspired by PDR, we develop a nonstandard semantics which computes for every 0 ≤ N an over-approximation of the set of traces of length N leading to a safety violation. The over approximation is precise, in the sense that it only includes traces that do not start at an initial state, unless the program is unsafe, and in this cas...

• Type: Journal
• Year: 2016
• Where: VMCAI
• Authors: Noam Rinetzky, Sharon Shoham
• Keywords: Software Engineering, VMCAI 2016