Computational Logic and Software Verification
Table of Contents
General Infromation
Courese Number: 332402
Instructor: Jyun-Ao Lin
Location: 二教 204(e)
Time: 09:10 – 12:00, Wednesday
Overviews
Computational logic has been used in a wide range of application in computer science, ranging from the deductive approach to Artificial Intelligence advocated by AI’s founder John McCarthy, to proving the absence of bugs in large industrial software such as the 14th metro line in Paris, or checking difficult theorems the as the one of Feit-Thompson in the classification of finite simple groups.
The goal of this course is to explain how logic can be used in order for modeling problems of computational or mathematical nature, and how computers can be used to achieve this.
Recommended Prerequisites
Some basic discrete mathematics, computer programming, algorithms, theory of computation.
Communication
When you need help from the course staff, please use office hours or hang around after lecture. For issues requiring privacy, please feel free to email the course instructor.
Office Hours
13:00–17:30 Monday
Topics and Class Schedule
Topics
Propositional Logic
Predicate Logic
Model Checking
Program Verification
Class Schedule
The current schedule is tentative and subject to change.
| Date | # | Lecture | Support |
|---|---|---|---|
| 02/21 | 1 | Introduction | intro slide,PL-1 |
| 02/28 | 2 | Holiday | |
| 03/06 | 3 | Propositional Logic | PL slide |
| 03/13 | 4 | SAT-Solver | SAT Slide |
| 03/20 | 5 | DPLL and CDCL | DPLL/CDCL slide |
| 03/27 | 6 | First-Order Logic | FOL slide |
| 04/03 | 7 | Earthquake | FOT slide |
| 04/10 | 8 | First-Order Theory | see above |
| 04/17 | 9 | Review | |
| 04/24 | 10 | Mid-term | |
| 05/01 | 11 | Quantifier-Elimination | QE slide |
| 05/08 | 12 | LTL Model-Checking | LTL-MC slide |
| 05/15 | 13 | CTL Model-Checking | CTL-MC slide |
| 05/22 | 14 | SAT-based Model-Checking Algorithm | SAT-MC slide |
| 05/29 | 15 | Program Verification | Prog-Verf slide |
| 06/05 | 16 | Total Correctness | Total-Corr slide |
| 06/12 | 17 | Final Project Presentation | |
| 06/19 | 18 | Final Project Presentation |
Useful References
- A. R. Bradley, Z. Manna, Calculus of Computation
- D. Kroening, O. Strichman, Decision Procedures
- J. Harrison, Handbook of Practical Logic and Automated Reasoning
- C. Baier, J.-P. Katoen, Principal of Model Checking
- K. R. Apt, F. S. Boer, E.-R. Olderog, Verification of Sequential and Concurrent Program
- F. Nielson, H. R. Nielson, C. Hankin, Principal of Program Analysis
Evalution
Asseignments (50 %)
Written Homework:
The goal of the written homework is to help you refine the fundamental skills, and better understand the theoretical underpinnings, that you will need in order to do well on the labs and exams. Grading for these assignments is based on the correctness of your answer, and the presentation of your reasoning. You should strive for clarity and conciseness, while making sure to show each step of your reasoning. Categorical answers with no explanation will not even receive partial credit, but lucid explanations of your attempt to find the answer will.
Written homework will be handed in in PDF format via teams, and should preferably be typeset in LaTeX.
Programming Homework:
The programming homework is designed to give you hands-on experience writing bug-free code with the help of formal verification tools. In general, we will ask you to implement some interesting functionality, such as a SAT solver or fault-tolerant communication protocol. The most important criterion with respect to grading programs is correctness.
Programming Homework will be send in a Unix compressed archive
name.tgz. Your archive must include a README file describing how
to compile and run your program. It must also include a short report
(2 pages max.) describing the salient parts of your code.
Academic Integrity
Students are expected to complete each assignment on their own, and should be able to explain all of the work that they hand in. Copying code or proof material from other students, from online sources, or from prior instances of this course is not allowed. However, you are encouraged to discuss assignments with each other at a sufficiently high level to avoid the risk of duplicating implementation or proof. Examples of this would be discussing algorithms and properties referred to in the assignment, helping other students with questions about a programming language or tool required to complete the assignment, discussing a general proof technique, or referring to an online source with useful information. Similarly, you may consult online sources, tutorials, and public libraries. If you find specifically helpful material it is critical that you (a) do not copy the code or proof, but study it as a guide and then do your own work, and (b) cite the source with your classmates' names, suitable URLs and chat prompts (if you use any generative AIs) in your solution. If you have questions about whether something might be permissible, contact the course staff before you proceed.
Mid-terms (20 %)
TBA
Final Project (20 %)
TBA
Attendance (10 %)
All students are expected to attend the lectures. However I appreciate that different people learn differently. Thus the attendance won't be recorded.
Some tools you may be interested in
Proof Assistant
LaTeX
- LaTeX for Logicians
- mathpar There are many options for typesetting inference rules and
derivation rules in LaTeX. We recommend
mathparwhich is included with most TeX distributions.
Acknowledgement and Credits
The course is designed based on the Introduction to Computational Logic by Bow-Yaw Wang. I thank him for providing his teaching materials including source code of slides.