Abstract
In this paper we present an overview of the verification tool μcke. It is an implementation of a BDD-based μ-calculus model checker and uses several optimization techniques that are lifted from special purpose model checkers to the μ-calculus. This gives the user more expressibility without loosing efficiency.
sup. by DFG GRK 209-96 “Graduiertenkolleg Beherrschbarkeit Komplexer Systeme”
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
K. Bartlett, R. Scantlebury, and P. Wilkinson. A note on reliable full-duplex transmissions over half-duplex lines. Communications of the ACM, 5(2):260–261, 1969.
I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli. Methodology and system for practical formal verification of reactive hardware. In Dill [9], pages 182–193.
A. Biere. Efficient μ-Calculus Model Checking with Binary Decision Diagrams. PhD thesis, Fakultät für Informatik, Universität Karlsruhe, Germany, Jan. 1997. In German. To appear.
J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401–424, Apr. 1994.
J. R. Burch, E. M. Clarke, and K. L. McMillan. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142–170, 1992.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, April 1986.
E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jah, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the futurebus+ cache coherence protocol. Formal Methods in System Design, 6:217–232, 1995.
O. Coudert and J. C. Madre. A unified framework for the formal verification of sequential circuits. In IEEE Intl. Conference on Computer-Aided Design, pages 126–129, 1990.
D. L. Dill, editor. Computer Aided Verification, 6th International Conference, CAV'94, volume 818 of LNCS. Springer-Verlag, June 1994.
Á. T. Eiríksson and K. L. McMillan. Using formal verification/analysis methods on the critical path in system design: A case study. In Wolper [20], pages 367–380.
R. Enders, T. Filkorn, and D. Taubner. Generating BDDs for symbolic model checking. Distributed Computing, 6:155–164, 1993.
G. Janssen. ROBDD software. Technical report, Department of Electrical Engineering, Eindhoven University of Technology, Oct. 1993.
A. Kick. Generation of Counterexamples and Witnesses for Model Checking. PhD thesis, Fakultät für Informatik, Universität Karlsruhe, Germany, July 1996.
K. L. McMillan. Symbolic Model Checking. Kluwer, 1993.
V. G. Naik and A. P. Sistla. Modeling and verification of a real life protocol using symbolic model checking. In Dill [9], pages 194–206.
J. Philipps and P. Scholz. Formal verification of statecharts with instantaneous chain reactions. In TACAS'97,1997.
S. Rajan, N. Shankar, and M. K. Srivas. An integration of model checking with automated proof checking. In Wolper [20], pages 84–97.
A. Rauzy. Toupie=μ-calculus+constraints. In Wolper [20], pages 114–126.
R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In IEEE Intl. Conference on Computer-Aided Design, pages 42–47, 1993.
P. Wolper, editor. Computer Aided Verification, 7th International Conference, CAV'95, volume 939 of LNCS. Springer-Verlag, July 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Biere, A. (1997). μcke — Efficient μ-calculus model checking. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_50
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_50
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive