Sciweavers

Share
CAV
2010
Springer

Abstract Analysis of Symbolic Executions

9 years 7 months ago
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.
Aws Albarghouthi, Arie Gurfinkel, Ou Wei, Marsha C
Added 02 Sep 2010
Updated 02 Sep 2010
Type Conference
Year 2010
Where CAV
Authors Aws Albarghouthi, Arie Gurfinkel, Ou Wei, Marsha Chechik
Comments (0)
books