Formal Methods in Software Engineering

Identifier
COMS 5120
Professor(s)

Last Updated: Spring 2025

  1. Credits and contact hours: 3 credits, 3 contact hours
  2. Text book, title, author, and year: None required
  3. Other supplemental materials: None

Specific course information

  1. Brief description of the content of the course: This course uses concepts from logic, algorithms and data structures, formal languages, graph theory, and linear algebra to explore technologies that can be be used to analyze the correctness of man-made discrete systems, including what is arguably the most complex class of artifacts: software, and in particular concurrent software. It also uses concepts from probability and stochastic processes to study aspects that go beyond mere logical correctness, and address instead performance (how fast or efficient is a system) and reliability (how long can a system work before breaking down, or what fraction of time a system is doing useful work as opposed to being repaired). Unlike testing and simulation, which can only give partial or approximate answers, the techniques we consider in this course can provide complete and exact answers (at least for some types of questions). However, they require substantially higher computational cost in terms of both time and memory, thus much research is devoted to improving their efficiency
  2. Prerequisites or co-requisites: graduate standing or permission of instructor
  3. Required, elective, or selected elective? Selected Elective

Specific goals for the course

  • An ability to analyze a complex computing problem and to apply principles of computing to identify solutions
  • An ability to apply computer science theory and software development fundamentals to produce computing-based solutions

Brief list of topics to be covered

  • Types of models 
  • Review of propositional logic
  • Model checking
  • Kripke structures
  • Computational tree logic (CTL)
  • Petri nets
  • Reachability and coverability analysis
  • Binary decision diagrams and symbolic CTL model checking
  •  Linear temporal logic (LTL)
  • Stochastic processes and discrete-time Markov chains (DTMCs)
  • Probabilistic model checking: DTMCs + CTL = PCTL