research-article

Control Explicit--Data Symbolic Model Checking

Authors:
Petr Bauch

Masaryk University, Brno, Botanicka, Czech Republic

Masaryk University, Brno, Botanicka, Czech Republic
View Profile

,
Vojtěch Havel

Masaryk University, Brno, Botanicka, Czech Republic

Masaryk University, Brno, Botanicka, Czech Republic
View Profile

,
Jiří Barnat

Masaryk University, Brno, Botanicka, Czech Republic

Masaryk University, Brno, Botanicka, Czech Republic
View Profile

ACM Transactions on Software Engineering and Methodology Volume 25 Issue 2Article No.: 15pp 1–48https://doi.org/10.1145/2888393

Published:06 April 2016Publication History

ACM Transactions on Software Engineering and Methodology

Abstract

Automatic verification of programs and computer systems with data nondeterminism (e.g., reading from user input) represents a significant and well-motivated challenge. The case of parallel programs is especially difficult, because then also the control flow nontrivially complicates the verification process. We apply the techniques of explicit-state model checking to account for the control aspects of a program to be verified and use set-based reduction of the data flow, thus handling the two sources of nondeterminism separately. We build the theory of set-based reduction using first-order formulae in the bit-vector theory to encode the sets of variable evaluations representing program data. These representations are tested for emptiness and equality (state matching) during the verification, and we harness modern satisfiability modulo theory solvers to implement these tests.

We design two methods of implementing the state matching, one using quantifiers and one that is quantifier-free, and we provide both analytical and experimental comparisons. Further experiments evaluate the efficiency of the set-based reduction method, showing the classical, explicit approach to fail to scale with the size of data domains. Finally, we propose and evaluate two heuristics to decrease the number of expensive satisfiability queries, together yielding a 10-fold speedup.

References

S. Anand, C. Păsăreanu, and W. Visser. 2006. Symbolic execution with abstract subsumption checking. In SPIN. LNCS, Vol. 3925. Springer, 163--181. DOI:http://dx.doi.org/10.1007/11691617_10 Google ScholarDigital Library
H. Andersen and H. Hulgaard. 1997. Boolean expression diagrams. In Proc. of LICS. 88--98. DOI:http://dx.doi. org/10.1109/LICS.1997.614938 Google ScholarDigital Library
S. Baarir and A. Duret-Lutz. 2007. Emptiness check of powerset buchi automata using inclusion tests. In Proc. of ACDS. 41--50. DOI:http://dx.doi.org/10.1109/ACSD.2007.49 Google ScholarDigital Library
D. Babic and M. Musuvathi. 2005. Modular Arithmetic Decision Procedure. Technical Report. Microsoft Research Redmont.Google Scholar
J. Barnat, P. Bauch, and V. Havel. 2014a. Model checking parallel programs with inputs. In Proc. of PDP. 756--759. DOI:http://dx.doi.org/10.1109/PDP.2014.44 Google ScholarDigital Library
J. Barnat, P. Bauch, and V. Havel. 2014b. Temporal verification of simulink diagrams. In Proc. of HASE. 81--88. DOI:http://dx.doi.org/10.1109/HASE.2014.20 Google ScholarDigital Library
J. Barnat, J. Beran, L. Brim, T. Kratochvíla, and P. Ročkai. 2012. Tool chain to support automated formal verification of avionics simulink designs. In FMICS. LNCS, Vol. 7437. Springer, 78--92. DOI:http://dx.doi.org/10.1007/978-3-642-32469-7_6Google Scholar
J. Barnat, L. Brim, V. Havel, J. Havlíček, J. Kriho, M. Lenčo, P. Ročkai, V. Štill, and J. Weiser. 2013. DiVinE 3.0 -- explicit-state model-checker for multithreaded C/C++ programs. In CAV. 863--868. DOI:http://dx.doi.org/10.1007/978-3-642-39799-8_60Google Scholar
J. Barnat, L. Brim, and J. Stříbrná. 2001. Distributed LTL model-checking in SPIN. In SPIN. LNCS, Vol. 2057. Springer, 200--216. DOI:http://dx.doi.org/10.1007/3-540-45139-0_13 Google ScholarDigital Library
C. Barrett, D. Dill, and J. Levitt. 1998. A decision procedure for bit-vector arithmetic. In Proc. of DAC. 522--527. DOI:http://dx.doi.org/10.1145/277044.277186 Google ScholarDigital Library
P. Bauch, V. Havel, and J. Barnat. 2014a. Accelerating temporal verification of simulink diagrams using satisfiability modulo theories. SQJ 22 (2014), 1--27. DOI:http://dx.doi.org/10.1007/s11219-014-9259-x Google ScholarDigital Library
P. Bauch, V. Havel, and J. Barnat. 2014b. LTL model checking of LLVM bitcode with symbolic data. In MEMICS. LNCS, Vol. 8934. Springer, 47--59. DOI:http://dx.doi.org/10.1007/978-3-319-14896-0_5Google Scholar
B. Becker, R. Drechsler, and R. Enders. 1997. On the representational power of bit-level and word-level decision diagrams. In Proc. of ASP-DAC. 461--467. DOI:http://dx.doi.org/10.1109/ASPDAC.1997.600304Google Scholar
D. Beyer and M. Keremoglu. 2011. CPAchecker: A tool for configurable software verification. In CAV. 184--190. DOI:http://dx.doi.org/10.1007/978-3-642-22110-1_16 Google ScholarDigital Library
D. Beyer and S. Löwe. 2013. Explicit-state software model checking based on CEGAR and interpolation. In FASE. LNCS, Vol. 7793. Springer, 146--162. DOI:http://dx.doi.org/10.1007/978-3-642-37057-1_11 Google ScholarDigital Library
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. 1999a. Symbolic model checking without BDDs. In TACAS. LNCS, Vol. 1579. Springer, 193--207. DOI:http://dx.doi.org/10.1007/3-540-49059-0_14 Google ScholarDigital Library
A. Biere, E. Clarke, and Y. Zhu. 1999b. Multiple state and single state tableaux for combining local and global model checking. In Correct System Design. LNCS, Vol. 1710. Springer, 163--179. DOI:http://dx.doi.org/10.1007/3-540-48092-7_8 Google ScholarDigital Library
P. Bjesse. 1999. Symbolic Model Checking with Sets of States Represented as Formulas. Technical Report. Chalmers Technical University.Google Scholar
J. Bohn, W. Damm, O. Grumberg, H. Hungar, and K. Laster. 1998. First-order-CTL model checking. In FSTTCS. LNCS, Vol. 1530. Springer, 283--294. DOI:http://dx.doi.org/10.1007/978-3-540-49382-2_27 Google ScholarDigital Library
B. Boigelot. 1999. Symbolic Methods for Exploring Infinite State Space. Ph.D. Dissertation. University of Liege.Google Scholar
B. Boigelot and P. Wolper. 1994. Symbolic verification with periodic sets. In CAV. LNCS, Vol. 818. Springer, 55--67. DOI:http://dx.doi.org/10.1007/3-540-58179-0_43 Google ScholarDigital Library
A. Bradley. 2011. SAT-based model checking without unrolling. In VMCAI. 70--87. DOI:http://dx.doi.org/10.1007/978-3-642-18275-4_7 Google ScholarDigital Library
P. Braione, G. Denaro, B. Křena, and M. Pezzè. 2008. Verifying LTL properties of bytecode with symbolic execution. In Proc. of Bytecode. Elsevier Science, 1--14.Google Scholar
L. Brim, I. Černá, P. Moravec, and J. Šimša. 2004. Accepting predecessors are better than back edges in distributed LTL model-checking. In FMCAD. LNCS, Vol. 3312. Springer, 352--366. DOI:http://dx.doi.org/ 10.1007/978-3-540-30494-4_25Google Scholar
R. Bruttomesso, A. Cimatti, A. Franzén, A. Griggio, Z. Hanna, A. Nadel, A. Palti, and R. Sebastiani. 2007. A lazy and layered SMT(BV) solver for hard industrial verification problems. In CAV. LNCS, Vol. 4590. Springer, 547--560. DOI:http://dx.doi.org/10.1007/978-3-540-73368-3_54 Google ScholarDigital Library
R. Bryant. 1986. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35, 8 (1986), 677--691. Google ScholarDigital Library
R. Bryant. 1991. On the complexity of VLSI implementations and graph representations of boolean functions with application to integer multiplication. IEEE Trans. Comput. 40, 2 (1991), 205--213. DOI:http://dx.doi.org/10.1109/12.73590 Google ScholarDigital Library
R. Bryant and Y.-A. Chen. 1995. Verification of arithmetic circuits with binary moment diagrams. In Proc. of DAC. 535--541. DOI:http://dx.doi.org/10.1145/217474.217583 Google ScholarDigital Library
R. Bryant, D. Kroening, J. Ouaknine, S. Seshia, O. Strichman, and B. Brady. 2007. Deciding bit-vector arithmetic with abstraction. In TACAS. LNCS, Vol. 4424. Springer, 358--372. DOI:http://dx.doi.org/ 10.1007/978-3-540-71209-1_28 Google ScholarDigital Library
M. Büchi and E. Sekerinski. 1998. Formal methods for component software: The refinement calculus perspective. In ECOOP. LNCS, Vol. 1357. Springer, 332--337. DOI:http://dx.doi.org/10.1007/3-540-69687-3_68Google Scholar
T. Bultan, R. Gerber, and C. League. 1998. Verifying systems with integer constraints and boolean predicates: A composite approach. In Proc. of ISSTA. 113--123. DOI:http://dx.doi.org/10.1145/271771.271799 Google ScholarDigital Library
I. Černá and R. Pelánek. 2003. Distributed explicit fair cycle detection (set based approach). In SPIN. LNCS, Vol. 2648. Springer, 623--623. DOI:http://dx.doi.org/10.1007/3-540-44829-2_4Google Scholar
M. Ciesielski, D. Pradhan, and A. Jabir. 2009. Canonical Graph-Based Representations for Verification of Arithmetic and Data Flow Designs. Cambridge University Press, Chapter 7, 173--245.Google Scholar
A. Cimatti, I. Narasamdya, and M. Roveri. 2012. Software model checking with explicit scheduler and symbolic threads. LMCS 8, 2 (2012), 1--42. DOI:http://dx.doi.org/10.2168/LMCS-8(2:18)2012Google Scholar
A. Cimatti, M. Roveri, and P. Bertoli. 2001. Searching powerset automata by combining explicit-state and symbolic model checking. In TACAS. LNCS, Vol. 2031. Springer, 313--327. DOI:http://dx.doi.org/ 10.1007/3-540-45319-9_22 Google ScholarDigital Library
E. Clarke, E. Emerson, and A. Sistla. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM T. Progr. Lang. Sys. 8, 2 (1986), 244--263. DOI:http://dx.doi.org/ 10.1145/5397.5399 Google ScholarDigital Library
E. Clarke, O. Grumberg, and D. Peled. 1999. Model Checking. MIT Press. Google ScholarDigital Library
A. Coen-Porisini, G. Denaro, C. Ghezzi, and M. Pezzé. 2001. Using symbolic execution for verifying safety-critical systems. In Proc. of ESEC/FSE. 142--151. DOI:http://dx.doi.org/10.1145/503209.503230 Google ScholarDigital Library
B. Cook, D. Kroening, and N. Sharygina. 2005. Symbolic model checking for asynchronous boolean programs. In SPIN. LNCS, Vol. 3639. Springer, 75--90. DOI:http://dx.doi.org/10.1007/11537328_9 Google ScholarDigital Library
C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. 1992. Memory-efficient algorithms for the verification of temporal properties. Form. Method Syst. Des. 1, 2 (1992), 275--288. DOI:http://dx.doi.org/ 10.1007/BF00121128 Google ScholarDigital Library
P. Cousot and R. Cousot. 1977. Abstract interpretation: A unified Lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of POPL. ACM, 238--252. DOI:http://dx.doi.org/ 10.1145/512950.512973 Google ScholarDigital Library
D. Cyrluk, O. Möller, and H. Rueß. 1997. An efficient decision procedure for the theory of fixed-sized bit-vectors. In CAV. LNCS, Vol. 1254. Springer, 60--71. DOI:http://dx.doi.org/10.1007/3-540-63166-6_9 Google ScholarDigital Library
L. de Moura and N. Bjørner. 2008. Z3: An efficient SMT solver. In TACAS. LNCS, Vol. 4963. Springer, 337--340. DOI:http://dx.doi.org/10.1007/978-3-540-78800-3_24 Google ScholarDigital Library
L. de Moura, H. Rueß, and M. Sorea. 2003. Bounded model checking and induction: From refutation to verification. In CAV. LNCS, Vol. 2725. Springer, 14--26. DOI:http://dx.doi.org/10.1007/978-3-540-45069-6_2Google Scholar
A. Duret-Lutz, K. Klai, D. Poitrenaud, and Y. Thierry-Mieg. 2011. Self-loop aggregation product—A new hybrid approach to on-the-fly LTL model checking. In ATVA. LNCS, Vol. 6996. Springer, 336--350. DOI:http://dx.doi.org/10.1007/978-3-642-24372-1_24 Google ScholarDigital Library
C. Eisner and D. Peled. 2002. Comparing symbolic and explicit model checking of a software system. In SPIN. LNCS, Vol. 2318. Springer, 230--239. DOI:http://dx.doi.org/10.1007/3-540-46017-9_18 Google ScholarDigital Library
A. Farzan, Z. Kincaid, and A. Podelski. 2013. Inductive data flow graphs. In Proc. of POPL. 129--142. DOI:http://dx.doi.org/10.1145/2429069.2429086 Google ScholarDigital Library
E. Gunter and D. Peled. 2005. Model checking, testing and verification working together. Form. Asp. Comput. 17, 2 (2005), 201--221. DOI:http://dx.doi.org/10.1007/s00165-005-0059-8 Google ScholarCross Ref
A. Gupta, C. Popeea, and A. Rybalchenko. 2011. Predicate abstraction and refinement for verifying multi-threaded programs. In Proc. of POPL. ACM, 331--344. DOI:http://dx.doi.org/10.1145/1926385.1926424 Google ScholarDigital Library
S. Haddad, J.-M. Ilié, and K. Klai. 2004. Design and evaluation of a symbolic and abstraction-based model checker. In ATVA. LNCS, Vol. 3299. Springer, 196--210. DOI:http://dx.doi.org/10.1007/978-3-540-30476-0_19Google Scholar
J. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, R. Paige, T. Rauhe, and A. Sandholm. 1995. Mona: Monadic second-order logic in practice. In TACAS. LNCS, Vol. 1019. Springer, 89--110. DOI:http://dx.doi.org/ 10.1007/3-540-60630-0_5 Google ScholarDigital Library
H. Hungar, O. Grumberg, and W. Damm. 1995. What if model checking must be truly symbolic. In CHARME. LNCS, Vol. 987. Springer, 1--20. DOI:http://dx.doi.org/10.1007/3-540-60385-9_1 Google ScholarDigital Library
S. Khurshid, C. Păsăreanu, and W. Visser. 2003. Generalized symbolic execution for model checking and testing. In TACAS. LNCS, Vol. 2619. Springer, 553--568. DOI:http://dx.doi.org/10.1007/3-540-36577-X_40 Google ScholarDigital Library
J. King. 1976. Symbolic execution and program testing. Commun. ACM 19, 7 (1976), 385--394. DOI:http://dx.doi. org/10.1145/360248.360252 Google ScholarDigital Library
D. Kroening and O. Strichman. 2010. Decision Procedures: An Algorithmic Point of View. Springer. Google ScholarDigital Library
O. Kupferman and M. Vardi. 1996. Module checking. In CAV. LNCS, Vol. 1102. Springer, 75--86. DOI:http://dx.doi.org/10.1007/3-540-61474-5_59 Google ScholarDigital Library
H. Lin. 1996. Symbolic transition graph with assignment. In CONCUR. LNCS, Vol. 1119. Springer, 50--65. DOI:http://dx.doi.org/10.1007/3-540-61604-7_47 Google ScholarDigital Library
Z. Manna and A. Pnueli. 1995. Temporal Verification of Reactive Systems: Safety. Springer. Google ScholarDigital Library
K. McMillan. 1992. Symbolic Model Checking. Ph.D. Dissertation. Carnegie Mellon University.Google ScholarDigital Library
K. McMillan. 2002. Applying SAT methods in unbounded symbolic model checking. In CAV. LNCS, Vol. 2404. Springer, 250--264. DOI:http://dx.doi.org/10.1007/3-540-45657-0_19 Google ScholarDigital Library
K. McMillan. 2003. Interpolation and SAT-based model checking. In CAV. 1--13. DOI:http://dx.doi.org/10.1007/978-3-540-45069-6_1Google Scholar
R. Pelánek. 2007. BEEM: Benchmarks for explicit model checkers. In SPIN. LNCS, Vol. 4595. Springer, 263--267. DOI:http://dx.doi.org/10.1007/978-3-540-73370-6_17Google Scholar
M. Pichora. 2003. Automated Reasoning About Hardware Data Types Using Bit-Vectors of Symbolic Lengths. Ph.D. Dissertation. University of Toronto. Google ScholarDigital Library
A. Podelski and A. Rybalchenko. 2005. Transition predicate abstraction and fair termination. In Proc. of POPL. 132--144. DOI:http://dx.doi.org/10.1145/1040305.1040317 Google ScholarDigital Library
K. Ravi, A. Pardo, G. Hachtel, and F. Somenzi. 1996. Modular verification of multipliers. In FMCAD. LNCS, Vol. 1166. Springer, 49--63. DOI:http://dx.doi.org/10.1007/BFb0031799 Google ScholarDigital Library
R. Sebastiani, S. Tonetta, and M. Vardi. 2005. Symbolic systems, explicit properties: On hybrid approaches for LTL symbolic model checking. In CAV. LNCS, Vol. 3576. Springer, 100--246. DOI:http://dx.doi.org/ 10.1007/11513988_35 Google ScholarDigital Library
K. Sen, D. Marinov, and G. Agha. 2005. CUTE: A concolic unit testing engine for C. ACM SIGSOFT 30, 5 (2005), 263--272. DOI:http://dx.doi.org/10.1145/1095430.1081750 Google ScholarDigital Library
R. Shostak. 1982. Deciding combinations of theories. In CADE. LNCS, Vol. 138. Springer, 209--222. DOI:http://dx.doi.org/10.1007/BFb0000061 Google ScholarDigital Library
P. Šimeček. 2006. DiVinE -- Distributed Verification Environment. Master’s thesis. Masaryk University.Google Scholar
A. Simon and A. King. 2007. Taming the wrapping of integer arithmetic. In SAS. LNCS, Vol. 4634. Springer, 121--136. DOI:http://dx.doi.org/10.1007/978-3-540-74061-2_8 Google ScholarDigital Library
M. Vardi. 2001. Branching vs. linear time: Final showdown. In TACAS. LNCS, Vol. 2031. Springer, 1--22. DOI:http://dx.doi.org/10.1007/3-540-45319-9_1 Google ScholarDigital Library
M. Vardi and P. Wolper. 1986. An automata-theoretic approach to automatic program verification. In Proc. of LICS. IEEE Computer Society Press, 332--344.Google Scholar
B.-Y. Wang. 2006. On the satisfiability of modular arithmetic formulae. In ATVA. LNCS, Vol. 4218. Springer, 186--199. DOI:http://dx.doi.org/10.1007/11901914_16 Google ScholarDigital Library
P. Williams, A. Biere, E. Clarke, and A. Gupta. 2000. Combining decision diagrams and SAT procedures for efficient symbolic model checking. In CAV. LNCS, Vol. 1855. Springer, 124--138. DOI:http://dx.doi.org/ 10.1007/10722167_13 Google ScholarDigital Library
C. Wintersteiger, Y. Hamadi, and L. de Moura. 2013. Efficiently solving quantified bit-vector formulas. Form. Method. Syst. Des. 42, 1 (2013), 3--23. DOI:http://dx.doi.org/10.1007/s10703-012-0156-2 Google ScholarDigital Library
P. Wolper and B. Boigelot. 2000. On the construction of automata from linear arithmetic constraints. In TACAS. LNCS, Vol. 1785. 1--19. DOI:http://dx.doi.org/10.1007/3-540-46419-0_1 Google ScholarDigital Library
T. Xie, D. Marinov, W. Schulte, and D. Notkin. 2005. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In TACAS. LNCS, Vol. 3440. Springer, 365--381. DOI:http://dx.doi.org/10.1007/978-3-540-31980-1_24 Google ScholarDigital Library

Index Terms

Control Explicit--Data Symbolic Model Checking

Recommendations

Regular model checking for LTL(MSO)

Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of ...
Read More
Explicit state model checking with generalized Büchi and Rabin automata
SPIN 2017: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software

In the automata theoretic approach to explicit state LTL model checking, the synchronized product of the model and an automaton that represents the negated formula is checked for emptiness. In practice, a (transition-based generalized) Büchi automaton (...
Read More
Model checking with generalized Rabin and Fin-less automata

In the automata theoretic approach to explicit state LTL model checking, the synchronized product of the model and an automaton that represents the negated formula is checked for emptiness. In practice, a (transition-based generalized) B chi automaton (...
Read More

Reviews

Reviewer: Lalit P Saxena

There is a recent trend toward the automation of the model checking and computer program verification process. The program or the model being verified and its verifiable property need to be restricted in the finite state spaces. The authors address the set-based reduction method for automatic computer program verification. The authors develop two methods of implementing state matching: one using quantifiers and another that is quantifier-free. The authors use two case studies to investigate the relationship between image-based and equivalence-based state matching, namely DVE (native language of DIVINE) models and random models. Further, the authors employ the DVE language for open systems, set-based reduction with explicit sets, set-based reduction with symbolic sets, equivalence-based versus image-based state matching and image versus equivalence using linear search, and experiments with witness-based matching resolution in both DVE and random models. The authors claim the novelty of their method lies in "the combination of explicit-state model checking with sets of variable evaluations represented as images of bit-vector functions." They further observe that explicit model checking made it possible to verify programs with nontrivial data flow. For future enhancements, the authors suggest "precisely distinguish[ing] between the sets of variable evaluations" and improving program verification using counterexample guided refinement, loop acceleration, and a compositional approach to control flow. This paper is an interesting read for those who are working in the area of explicit-state model checking and computer program verification. The authors affirm that "the ability to produce counterexamples is a crucial property of linear temporal logic model checking," which makes this paper worth reading. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Published in
ACM Transactions on Software Engineering and Methodology Volume 25, Issue 2
May 2016
328 pages
ISSN:1049-331X
EISSN:1557-7392
DOI:10.1145/2913009
Editor:
David S. Rosenblum
National University of Singapore, Singapore
Issue’s Table of Contents
Copyright © 2016 ACM
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
- Published: 6 April 2016
- Accepted: 1 January 2016
- Revised: 1 December 2015
- Received: 1 January 2015
Published in tosem Volume 25, Issue 2

Permissions
Request permissions about this article.
Request Permissions

Check for updates
Author Tags
Model checking
modular arithmetic
static analysis
Qualifiers
- research-article
- Research
- Refereed
Conference
Funding Sources
Other Metrics
View Article Metrics

Article Metrics
- 1
  Total Citations
  View Citations
- 281
  Total Downloads
- Downloads (Last 12 months)5
- Downloads (Last 6 weeks)2
Other Metrics
View Author Metrics
Cited By
View all

PDF Format

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Control Explicit--Data Symbolic Model Checking

ACM Transactions on Software Engineering and Methodology

Abstract

References

Cited By

Index Terms

Recommendations

Regular model checking for LTL(MSO)

Explicit state model checking with generalized Büchi and Rabin automata

Model checking with generalized Rabin and Fin-less automata

Reviews

Access critical reviews of Computing literature here