Thread-Modular Abstraction Refinement

13 years 10 months ago
Thread-Modular Abstraction Refinement
odular Abstraction Refinement Thomas A. Henzinger1 , Ranjit Jhala1 , Rupak Majumdar1 , and Shaz Qadeer2 1 University of California, Berkeley 2 Microsoft Research, Redmond Abstract. We present an algorithm called Tar ("Thread-modular Abstraction Refinement") for model checking safety properties of concurrent software. The Tar algorithm uses thread-modular assume-guarantee reasoning to overcome the exponential complexity in the control state of multithreaded programs. Thread modularity means that Tar explores the state space of one thread at a time, making assumptions about how the environment can interfere. The Tar algorithm uses counterexampleredicate-abstraction refinement to overcome the usually infinite complexity in the data state of C programs. A successive approximation scheme automatically infers the necessary precision on data variables as well as suitable environment assumptions. The scheme is novel in that transition relations are approximated from above, while at t...
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar,
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2003
Where CAV
Authors Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer
Comments (0)