Abstract Analysis of Symbolic Executions

Analysis of Symbolic Executions Aws Albarghouthi1 , Arie Gurfinkel2 , Ou Wei1,3 , and Marsha Chechik1 1 Department of Computer Science, University of Toronto, Canada 2 Software Engineering Institute, Carnegie Mellon University, USA 3 Nanjing University of Aeronautics and Astronautics, China Multicore technology has moved concurrent programming to the forefront of computer science. In this paper, we look at the problem of reasoning about concurrent systems with infinite data domains and non-deterministic input, and develop a method for verification and falsification of safety properties of such systems. Novel characteristics of this method are (a) constructing under-approximating models via symbolic execution with abstract matching and (b) proving safety using underapproximating models.

• Type: Conference
• Year: 2010
• Where: CAV
• Authors: Aws Albarghouthi, Arie Gurfinkel, Ou Wei, Marsha Chechik
• Keywords: CAV 2010, Computer Science, Hardware, Symbolic Execution, Symbolic Executions Aws