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.

• Type: Conference
• Year: 2006
• Where: FMCAD
• Authors: Byron Cook, Daniel Kroening, Natasha Sharygina
• Keywords: Algorithm Models Recursion, FMCAD 2006, Formal Methods, Symbolic Algorithm, Unbounded Thread Creation