M. Ben-Ari (2006):
Principles of Concurrent and Distributed Programming (2nd Edition) (Prentice-Hall International Series in Computer Science).
Addison-Wesley Longman Publishing Co., Inc.,
Boston, MA, USA.
M. Ben-Ari, Z. Manna & A. Pnueli (1981):
The temporal logic of branching time.
In: POPL '81: Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages.
ACM,
pp. 164–176,
doi:10.1145/567532.567551.
R. E. Bryant (1986):
Graph-Based Algorithms for Boolean Function Manipulation.
IEEE Transactions on Computers 35,
pp. 677–691,
doi:10.1109/TC.1986.1676819.
J. R. Burch, E. M. Clarke & D. E. Long (1991):
Symbolic Model Checking with Partitioned Transition Relations.
North-Holland,
pp. 49–58.
G. Ciardo & A. J. Yu (2005):
Saturation-based symbolic reachability analysis using conjunctive and disjunctive partitioning.
In: Proc. CHARME, LNCS 3725.
Springer-Verlag,
pp. 146–161.
A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani & A. Tacchella (2002):
NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking.
In: Proc. International Conference on Computer-Aided Verification (CAV 2002),
LNCS 2404.
Springer,
Copenhagen, Denmark.
E. M. Clarke & E. A. Emerson (1982):
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic.
In: Logic of Programs, Workshop.
Springer-Verlag,
London, UK,
pp. 52–71,
doi:10.1007/BFb0025774.
E. M. Clarke, O. Grumberg & D. A. Peled (2000):
Model checking.
MIT Press.
A. Goel, G. Hasteer & R. Bryant (2003):
Symbolic representation with ordered function templates.
In: Proceedings of the 40th annual Design Automation Conference,
DAC '03.
ACM,
New York, NY, USA,
pp. 431–435,
doi:10.1145/775832.775946.
Alexander Kaiser, Daniel Kroening & Thomas Wahl (2010):
Dynamic Cutoff Detection in Parameterized Concurrent Programs.
In: Computer-Aided Verification (CAV),
doi:10.1007/978-3-642-14295-6_55.
T. Kam, T. Villa, R. Brayton & A. Sangiovanni-Vincentelli (1998):
Multi-valued decision diagrams: theory and applications.
Multiple-Valued Logic 4(1-2),
pp. 9–62.
K. L. McMillan (1993):
Symbolic Model Checking.
Kluwer Academic Publishers,
Norwell, MA, USA.
A. S. Miner (2001):
Efficient solution of GSPNs using Canonical Matrix Diagrams.
In: Proceedings of the 9th International Workshop on Petri Nets and Performance Models.
IEEE Comp. Soc. Press,
pp. 101–110,
doi:10.1109/PNPM.2001.953360.
A. S. Miner (2004):
Saturation for a General Class of Models.
In: QEST '04: Proceedings of the The Quantitative Evaluation of Systems, First International Conference.
IEEE Computer Society,
Washington, DC, USA,
pp. 282–291,
doi:10.1109/QEST.2004.38.
G. L. Peterson (1981):
Myths About the Mutual Exclusion Problem..
Inf. Process. Lett. 12(3),
pp. 115–116,
doi:10.1016/0020-0190(81)90106-X.
A. Pnueli (1981):
A temporal logic of concurrent programs.
Theoretical Computer Science 13,
pp. 45–60.
A. Pnueli, S. Ruah & L. Zuck (2001):
Automatic Deductive Verification with Invisible Invariants.
Springer,
pp. 82–97.
J.-P. Queille & J. Sifakis (1982):
Specification and verification of concurrent systems in CESAR.
In: DesProceedings of the 5th Colloquium on International Symposium on Programming.
Springer-Verlag,
London, UK,
pp. 337–351,
doi:10.1007/3-540-11494-7_22.
R. K. Ranjan, A. Aziz, R. K. Brayton, B. Plessier & C. Pixley (1995):
Efficient BDD algorithms for FSM synthesis and verification.
In: In IEEE/ACM Proceedings International Workshop on Logic Synthesis, Lake Tahoe (NV.
F. Somenzi (2009):
CUDD: CU Decision Diagram Package, Release 2.4.2.
University of Colorado at Boulder,
http://vlsi.colorado.edu/ fabio/CUDD/.
T. Wahl, N. Blanc & A. Emerson (2008):
Sviss: Symbolic Verification of Symmetric Systems.
In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS).
B. Yang, R. E. Bryant, D. R. O'Hallaron, A. Biere, O. Coudert, G. Janssen, R. K. Ranjan & F. Somenzi (1998):
A Performance Study of BDD-Based Model Checking.
In: Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design,
FMCAD '98.
Springer-Verlag,
London, UK,
pp. 255–289.