SENG 4120

Software system is critical to many aspects of our lives. Students explore the mathematical foundations of software modeling including propositional logic, proof theory and semantics of predicate logic, and extended finite state machines. Students learn model verification using linear-time temporal logic, branching-time logic, and explore various model-checking algorithms. Students are introduced to the techniques of program verification, partial and total correctness, proof calculus, modal logics, and binary decision trees. Students gain hands-on experience using a tool for model checking.