Efficient Model Checking Using Tabled Resolution
作者： YS Ramakrishna , CR Ramakrishnan , IV Ramakrishnan , Scott A Smolka , Terrance Swift
关键词:
摘要: We demonstrate the feasibility of using XSB tabled logic programming system as a programmable fixed-point engine for implementing efficient local model checkers. In particular, we present XMC, an XSB-based checker CCS-like value-passing language and alternation-free fragment modal mu-calculus. XMC is written in under 200 lines code, which constitute declarative specification CCS mu-calculus at level semantic equations.
springer.com
core.ac.uk
elsevier.com
acm.org 
sci-hub.st 参考文章(30)
Steven Dawson, CR Ramakrishnan, IV Ramakrishnan, Terrance Swift, None, Optimizing Clause Resolution: Beyond Unification Factoring. ILPS. pp. 194- 208 ,(1995)
E. Allen Emerson, Chin Laung Lei, EFFICIENT MODEL CHECKING IN FRAGMENTS OF THE PROPOSITIONAL MU-CALCULUS. logic in computer science. pp. 267- 278 ,(1986)
Zohar Manna, Amir Pnueli, Temporal Verification of Reactive Systems Springer New York. ,(1995) , 10.1007/978-1-4612-4222-2
Antoine Rauzy, Toupie = µ-Calculus + Constraints computer aided verification. pp. 114- 126 ,(1995) , 10.1007/3-540-60045-0_44
Edmund M. Clarke, E. Allen Emerson, DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC 25 Years of Model Checking. ,vol. 131, pp. 196- 215 ,(2008) , 10.1007/978-3-540-69850-0_12
Sérgio Vale Aguiar Campos, Kenneth L. McMillan, Edmund M. Clarke, Vassili Hartonas-Garmhausen, Symbolic Model Checking ,(1993)
Robin Milner, Communication and Concurrency ,(1989)
Rance Cleaveland, Steve Sims, The NCSU Concurrency Workbench computer aided verification. pp. 394- 397 ,(1996) , 10.1007/3-540-61474-5_87
Lalita Jategaonkar Jagadeesan, Carlos Puchol, James E. Olnhausen, Safety Property Verification of ESTEREL Programs and Applications to Telecommunications Software computer aided verification. pp. 127- 140 ,(1995) , 10.1007/3-540-60045-0_45
Hisao Tamaki, Taisuke Sato, OLD resolution with tabulation international conference on logic programming. pp. 84- 98 ,(1986) , 10.1007/3-540-16492-8_66