Formal Methods in Software Engineering

Course
Course Catalog URL: 
https://catalog.iastate.edu/azcourses/com_s/
Identifier: 
COM S 512
  1. Credits and contact hours: 3 credits, 3 contact hours
  2. Instructor’s or course coordinator’s name: Samik Basu
  3. Text book, title, author, and year: None required
  4. 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

  1. 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.
  2. Prerequisites or co-requisites: COM S 311, STAT 330; for graduate credit: graduate standing or permission of instructor
  3. Required, elective, or selected elective? Selected Elective

Specific goals for the course

  1. 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