2024 Faculty Courses School of Computing Department of Mathematical and Computing Science Graduate major in Mathematical and Computing Science
Software Verification
- Academic unit or major
- Graduate major in Mathematical and Computing Science
- Instructor(s)
- Yasuhiko Minamide
- Class Format
- Lecture (Face-to-face)
- Media-enhanced courses
- -
- Day of week/Period
(Classrooms) - 5-6 Tue / 5-6 Fri
- Class
- -
- Course Code
- MCS.T509
- Number of credits
- 200
- Course offered
- 2024
- Offered quarter
- 1Q
- Syllabus updated
- Mar 14, 2025
- Language
- Japanese
Syllabus
Course overview and goals
This course covers the theories for software verification. We first introduce the operational semantics of programming languages and Hoare logic, and discuss the soundness and completeness of Hoare Logic. Then, we discuss other theories related to software verification: model checking, automata over infinite words, LTL, and CTL.
Course description and aims
Students understand the theories related to software verification and get better understanding of various computation models.
Keywords
operational semantics, Hoare logic, model checking, automaton over infinite words, temporal logic
Competencies
- Specialist skills
- Intercultural skills
- Communication skills
- Critical thinking skills
- Practical and/or problem-solving skills
Class flow
Lectures will be given according to the following schedule. Students solve some exercises during lecture to check their understanding. There will be about seven assignments where students also solve some exercises.
Course schedule/Objectives
| Course schedule | Objectives | |
|---|---|---|
| Class 1 | Operational semantics of programming languages |
Operational semantics: big-step and small-step |
| Class 2 | Hoare Logic (1) |
Inference rules of Hoare logic |
| Class 3 | Hoare Logic (2): soundness and relative completeness |
Relative completeness, expressiveness of assertion language |
| Class 4 | Propositional logic and satisfiability |
Propositional logic, SAT |
| Class 5 | Review of predicate logic |
Semantics of predication logic, normal forms |
| Class 6 | Automated theorem proving: resolution principle |
Unification, resolution principle |
| Class 7 | Decision procedure for arithmetics |
Decision procedure for Presburger arithmetic |
| Class 8 | Automata over infinite words (1) |
ω-regular languages, Büchiオートマトン |
| Class 9 | Automata over infinite words (2) |
Closure properties, Muller automaton |
| Class 10 | Linear-time temporal logic (LTL) |
Semantics and model checking of LTL |
| Class 11 | Examination to check students' understanding |
Mid-term examination |
| Class 12 | Computational tree logic (CTL) |
Semantics and model checking of CTL |
| Class 13 | Binary decision diagram |
Operations on BDD |
| Class 14 | Software model checking |
Abstraction, counterexample guided abstraction refinement (CEGAR) |
Study advice (preparation and review)
To enhance effective learning, students are encouraged to spend approximately 100 minutes preparing for class and another 100 minutes reviewing class content afterwards (including assignments) for each class.
They should do so by referring to textbooks and other course material.
Textbook(s)
None required.
Reference books, course materials, etc.
Course materials are provided during class.
The following is reference books related to this course.
*Formal Semantics of Programming Languages, Glynn Winskel, MIT Press, 1993.
*Automata Theory: An Algorithmic Approach, Javier Esparza and Michael Blondin, MIT Press, 2023.
Evaluation methods and criteria
Students are assessed based on scores of reports and exercise problems.
Related courses
- MCS.T214 ： Theory of Automata and Languages
- MCS.T334 ： Compiler Construction
- MCS.T313 ： Mathematical Logic
- MCS.T404 ： Logical Foundations of Computing
Prerequisites
Students require the knowledge of mathematical logic, automata, and context-free grammars.
Exercises of Software verification must be done on a PC of each student. Exercises can be done on Docker of Mac OS, Linux, and Windows.