Slides:

• Lecture Overview (1-up, 6-up)

Document:

• Lecture Overview (1-up, 2-up)

Slides:

• Bogor Overview (1-up, 6up)
• Core Algorithm (1-up, 6-up)

Supplemental Reading:

• Bogor: An Extensible and Highly-Modular Model Checking Framework by Robby, Matthew B. Dwyer, John Hatcliff in the Proceedings of the Fourth Joint Meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003).
• Foundations of Model-checking course notes chapter (1-up, 6-up)
• Book companion

Slides:

• Bogor Architecture (1-up, 6-up)
• Bogor Extensions (1-up, 6-up)

Supplemental Reading:

• Bogor Extensions Tutorial (1-up, 2-up)

Slides:

• Representing Java (1-up, 6-up)
• Statespace Reductions (1-up, 6-up)
• JML Checking (1-up, 6-up)

Supplemental Reading:

• Checking Strong Specifications Using An Extensible Software Model Checking Framework by Robby, Edwin Rodriguez, Matthew B. Dwyer, John Hatcliff in the Proceedings of the Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004)
• Checking Strong Specifications Using An Extensible Software Model Checking Framework (extended version) by Robby, Edwin Rodriguez, Matthew B. Dwyer, John Hatcliff submitted for journal publication.
• Verifying Atomicity Specifications for Concurrent Object-Oriented Software using Model Checking by John Hatcliff, Robby, Matthew B. Dwyer in the Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2004).
• Patterns in Property Specification for Finite-state Verification by Matthew B. Dwyer, George S. Avrunin, and J. C. Corbett in Proceedings of the 21st International Conference on Software Engineering

Slides:

• Cadena Overview (1-up, 6-up)

Supplemental Reading:

• Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems by John Hatcliff, William Deng, Matthew Dwyer, Georg Jung, Venkatesh Prasad Ranganath in Proceedings of the 2003 International Conference on Software Engineering (ICSE 2003).
• Model-checking Middleware-based Event-driven Real-time Embedded Software by William Deng, Matthew B. Dwyer, John Hatcliff, Georg Jung, Robby, Gurdip Singh in the Proceedings of the First International Symposium on Formal Methods for Components and Objects (FMCO 2002).
• A Case Study in Domain-customized Model Checking for Real-time Component Software by Matthew Hoosier, John Hatcliff, Robby, Matthew B. Dwyer (submitted for publication).

Examples:

• Bogor/BIR models generated by Cadena (basicsp.bir, modalsp.bir).