Course
Course Catalog URL:
Identifier:
COM S 5120
- Credits and contact hours: 3 credits, 3 contact hours
- Instructor’s or course coordinator’s name: Samik Basu
- Text book, title, author, and year: None required
- Other supplemental materials: Logic in Computer Science, Huth and Ryan.; Model Checking, Clarke, Grumberg and Peled.; Principles of Model Checking, Baier and Katoen.; Spin Model Checker, Holzmann.
Specific course information
- Brief description of the content of the course: A study of formal techniques for model-based specification and verification of software systems. Topics include logics, formalisms, graph theory, numerical computations, algorithms, and tools for automatic analysis of systems. Graduate credit requires in-depth study of concepts.
- Prerequisites or co-requisites: COM S 311, STAT 330; for graduate credit: graduate standing or permission of instructor
- Required, elective, or selected elective? Selected Elective
Specific goals for the course
- Specific outcomes of instruction:
- An ability to analyze a complex computing problem and to apply principles of computing to identify solutions (1)
- An ability to apply computer science theory and software development fundamentals to produce computing-based solutions (6)
Brief list of topics to be covered
- Temporal logic (CTL, LTL)
- Kripke structure
- Model checking
- Fixed points
- Labeled transition system
- Process algebra CCS
- Modal mu-calculus
- Program verification
- Counter-example analysis
- Theorem prover basics