Model checking with bounded context switches
作者： Niels Jakob Rehof , Shaz Qadeer
DOI:
关键词:
摘要: Validity of one or more assertions for any concurrent execution a plurality software instructions with at most k−1 context switches can be determined. checking account the in an unbounded stack depth scenario. A finite data domain representation used. The represented by pushdown system. thread creation during instructions.
lens.org 参考文章(40)
M. Robby, Bogor : An Extensible and Highly Modular Model Checking Framework Proc. 9th ESEC/11th FSE, 2003. ,(2003)
Shaz Qadeer, Dinghao Wu, Data race detection using sequential program analysis ,(2004)
Sriram K. Rajamani, Thomas J. Ball, Rupak Majumdar, Todd D. Millstein, System and method for generating a predicate abstraction of a program ,(2002)
Mark Christiaens, Topological, on-the-fly classification of objects into a global set and local sets ,(2000)
Martin Rinard, Analysis of Multithreaded Programs static analysis symposium. pp. 1- 19 ,(2001) , 10.1007/3-540-47764-0_1
Sriram K. Rajamani, Thomas J. Ball, Methods for enhancing program analysis ,(2001)
Claudio Imoberdorf, Jean S. Hartmann, System and method for functional testing of distributed, component-based software ,(2000)
Edmund M. Clarke, E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic Logic of Programs, Workshop. pp. 52- 71 ,(1981) , 10.1007/BFB0025774
J. P. Queille, J. Sifakis, Specification and verification of concurrent systems in CESAR Proceedings of the 5th Colloquium on International Symposium on Programming. pp. 337- 351 ,(1982) , 10.1007/3-540-11494-7_22
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer, Thread-modular abstraction refinement computer aided verification. pp. 262- 274 ,(2003) , 10.1007/978-3-540-45069-6_27