Cormac Flanagan
Patrice Godefroid
Skip Abstract Section
Abstract
We present a new approach to partial-order reduction for model checking software. This approach is based on initially exploring an arbitrary interleaving of the various concurrent processes/threads, and dynamically tracking interactions between these to identify backtracking points where alternative paths in the state space need to be explored. We present examples of multi-threaded programs where our new dynamic partial-order reduction technique significantly reduces the search space, even though traditional partial-order algorithms are helpless.
- T. Ball and S. Rajamani. The SLAM Toolkit. In Proceedings of CAV'2001 (13th Conference on Computer Aided Verification), volume 2102 of Lecture Notes in Computer Science, pages 260--264, Paris, July 2001. Springer-Verlag.]] Google Scholar
Digital Library
- E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.]] Google ScholarDigital Library
- P. R. Cohen and E. A. Feigenbaum. Handbook of Artificial Intelligence. Pitman, London, 1982.]]Google Scholar
- J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu, Robby, and H. Zheng. Bandera: Extracting Finite-State Models from Java Source Code. In Proceedings of the 22nd International Conference on Software Engineering, 2000.]] Google ScholarDigital Library
- M. B. Dwyer, J. Hatcliff, V. R. Prasad, and Robby. Exploiting Object Escape and Locking Information in Partial Order Reduction for Concurrent Object-Oriented Programs. To appear in Formal Methods in System Design, 2004.]] Google ScholarDigital Library
- J. Esparza. Model Checking Using Net Unfoldings. Science of Computer Programming, 23:151--195, 1994.]] Google ScholarDigital Library
- J. Esparza and K. Heljanko. Implementing LTL model checking with net unfoldings. In Proceedings of the 8th SPIN Workshop (SPIN'2001), volume 2057 of Lecture Notes in Computer Science, pages 37--56, Toronto, May 2001. Springer-Verlag.]] Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Transactions for Software Model Checking. In Proceedings of the Workshop on Software Model Checking, pages 338--349, June 2003.]]Google ScholarCross Ref
- P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems -- An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer-Verlag, January 1996.]] Google ScholarDigital Library
- P. Godefroid. Model Checking for Programming Languages using VeriSoft. In Proceedings of POPL'97 (24th ACM Symposium on Principles of Programming Languages), pages 174--186, Paris, January 1997.]] Google ScholarDigital Library
- P. Godefroid. Software Model Checking: The VeriSoft Approach. To appear in Formal Methods in System Design, 2005. Also available as Bell Labs Technical Memorandum ITD-03-44189G.]] Google ScholarDigital Library
- P. Godefroid and D. Pirottin. Refining dependencies improves partial-order verification methods. In Proceedings of CAV'93 (5th Conference on Computer Aided Verification), volume 697 of Lecture Notes in Computer Science, pages 438--449, Elounda, June 1993. Springer-Verlag.]] Google ScholarDigital Library
- P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 2(2):149--164, April 1993.]] Google ScholarDigital Library
- T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy Abstraction. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages, pages 58--70, Portland, January 2002.]] Google ScholarDigital Library
- S. Katz and D. Peled. Defining conditional independence using collapses. Theoretical Computer Science, 101:337--359, 1992.]] Google ScholarDigital Library
- L. Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558--564, 1978.]] Google ScholarDigital Library
- F. Mattern. Virtual Time and Global States of Distributed Systems. In Proc. Workshop on Parallel and Distributed Algorithms, pages 215--226. North-Holland / Elsevier, 1989.]]Google Scholar
- A. Mazurkiewicz. Trace theory. In Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, volume 255 of Lecture Notes in Computer Science, pages 279--324. Springer-Verlag, 1986.]] Google ScholarDigital Library
- K. McMillan. Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits. In Proc. 4th Workshop on Computer Aided Verification, volume 663 of Lecture Notes in Computer Science, pages 164--177, Montreal, June 1992. Springer-Verlag.]] Google ScholarDigital Library
- D. Peled. All from one, one for all: on model checking using representatives. In Proc. 5th Conference on Computer Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 409--423, Elounda, June 1993. Springer-Verlag.]] Google ScholarDigital Library
- S. D. Stoller. Model-Checking Multi-Threaded Distributed Java Programs. International Journal on Software Tools for Technology Transfer, 4(1):71--91, October 2002.]]Google ScholarCross Ref
- S. D. Stoller and E. Cohen. Optimistic Synchronization-Based State-Space Reduction. In H. Garavel and J. Hatcliff, editors, Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2619 of Lecture Notes in Computer Science, pages 489--504. Springer-Verlag, April 2003.]] Google ScholarDigital Library
- S. D. Stoller, L. Unnikrishnan, and Y. A. Liu. Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods. In Proceedings of the 12th Conference on Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 264--279, Chicago, July 2000. Springer-Verlag.]] Google ScholarDigital Library
- C.A. Thekkath, T. Mann, and E.K. Lee. Frangipani: A scalable distributed file system. In Proceedings of the 16th ACM Symposium on Operating Systems Principles, pages 224--237, October 1997.]] Google ScholarDigital Library
- A. Valmari. Stubborn sets for reduced state space generation. In Advances in Petri Nets 1990, volume 483 of Lecture Notes in Computer Science, pages 491--515. Springer-Verlag, 1991.]] Google ScholarDigital Library
- A. Valmari. On-the-fly verification with stubborn sets. In Proc. 5th Conference on Computer Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 397--408, Elounda, June 1993. Springer-Verlag.]] Google ScholarDigital Library
- W. Visser, K. Havelund, G. Brat, and S. Park. Model Checking Programs. In Proceedings of ASE'2000 (15th International Conference on Automated Software Engineering), Grenoble, September 2000.]] Google ScholarDigital Library
Index Terms
- Dynamic partial-order reduction for model checking software
Recommendations
Dynamic partial-order reduction for model checking software
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe present a new approach to partial-order reduction for model checking software. This approach is based on initially exploring an arbitrary interleaving of the various concurrent processes/threads, and dynamically tracking interactions between these to ...
Partial-order reduction and trail improvement in directed model checking
In this paper we present work on trail improvement and partial-order reduction in the context of directed explicit-state model checking. Directed explicit-state model checking employs directed heuristic search algorithms such as A* or best-first search ...
Partial-Order Reduction in Symbolic State-Space Exploration
Special issue on CAV '97State-space explosion is a fundamental obstacle in the formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reduction and symbolic ...
Comments