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