Sciweavers

FMCAD
2006
Springer

Over-Approximating Boolean Programs with Unbounded Thread Creation

13 years 7 months ago
Over-Approximating Boolean Programs with Unbounded Thread Creation
Abstract-- This paper describes a symbolic algorithm for overapproximating reachability in Boolean programs with unbounded thread creation. The fix-point is detected by projecting the state of the threads to the globally visible parts, which are finite. Our algorithm models recursion by over-approximating the call stack that contains the return locations of recursive function calls, as reachability is undecidable in this case. The algorithm may obtain spurious counterexamples, which are removed iteratively of an abstraction refinement loop. Experiments show that the symbolic algorithm for unbounded thread creation scales abstract models.
Byron Cook, Daniel Kroening, Natasha Sharygina
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where FMCAD
Authors Byron Cook, Daniel Kroening, Natasha Sharygina
Comments (0)