Bounded Model Checking for Concurrent Systems: Synchronous Vs. Asynchronous
作者： Malay K. Ganai
DOI: 10.1007/978-1-4419-9359-5_6
关键词:
摘要: Concurrent systems are hard to verify due complex and unintended asynchronous interactions. Exploring the state space of such a system is daunting task. Model checking techniques that use symbolic search partial-order reduction gaining popularity. In this chapter, we focus primarily on bounded model (BMC) approaches decision procedures for length counter-examples safety properties as data races assertion violations in multi-threaded concurrent systems. particular, contrast several state-of-the-art based synchronous modeling styles used formulating problems, sizes corresponding formulas.
springer.com
sci-hub.st 参考文章(48)
Aarti Gupta, Malay Ganai, SAT-Based Scalable Formal Verification Solutions (Series on Integrated Circuits and Systems) Springer-Verlag New York, Inc.. ,(2007)
Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof, Yichen Xie, Zing: Exploiting Program Structure for Model Checking Concurrent Software CONCUR 2004 - Concurrency Theory. pp. 1- 15 ,(2004) , 10.1007/978-3-540-28644-8_1
Shaz Qadeer, Jakob Rehof, Context-Bounded Model Checking of Concurrent Software Tools and Algorithms for the Construction and Analysis of Systems. pp. 93- 107 ,(2005) , 10.1007/978-3-540-31980-1_7
Robert Nieuwenhuis, Albert Oliveras, DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic Computer Aided Verification. pp. 321- 334 ,(2005) , 10.1007/11513988_33
Sérgio Vale Aguiar Campos, Kenneth L. McMillan, Edmund M. Clarke, Vassili Hartonas-Garmhausen, Symbolic Model Checking ,(1993)
Byron Cook, Daniel Kroening, Natasha Sharygina, Symbolic Model Checking for Asynchronous Boolean Programs Model Checking Software. pp. 75- 90 ,(2005) , 10.1007/11537328_9
Malay K. Ganai, Chao Wang, Interval Analysis for Concurrent Trace Programs Using Transaction Sequence Graphs Runtime Verification. pp. 253- 269 ,(2010) , 10.1007/978-3-642-16612-9_20
Chao Wang, Sudipta Kundu, Malay Ganai, Aarti Gupta, Symbolic Predictive Analysis for Concurrent Programs formal methods. ,vol. 5850, pp. 256- 272 ,(2009) , 10.1007/978-3-642-05089-3_17
Doron Peled, All from One, One for All: on Model Checking Using Representatives computer aided verification. pp. 409- 423 ,(1993) , 10.1007/3-540-56922-7_34
Patrice Godefroid, Didier Pirottin, Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract) computer aided verification. pp. 438- 449 ,(1993) , 10.1007/3-540-56922-7_36