| Course Name | Formal Verification |
| Course Code | 23CSE464 |
| Program | B. Tech. in Computer Science and Engineering (CSE) |
| Credits | 3 |
| Campus | Amritapuri ,Coimbatore,Bengaluru, Amaravati, Chennai |
Proving the correctness of sequential programs with respect to a given contract: verification rules and application examples, partial and total correctness. Verification of simple C programs using tools such as Alt-Ergo and Frama-C.
Specifying the input-output contract of a sequential program using logical formulae with bounded quantifiers. Applying the Weakest Preconditions calculus for deriving verification conditions for programs with well-structured control and linear data structures. Formulating loop invariants for iterative programs. Applying the technique for programs such as sorting and searching.
Developing finite-state models for concurrent programs and specifying their behavioural correctness using propositional temporal logic. Defining models using a language such as PROMELA and checking their correctness using SPIN. Applying the technique to check safety properties, such as mutual exclusion and absence of deadlock, and liveness properties such as responsiveness to requests.
Course Objectives
Course Outcomes
CO1: Understand the necessity of proving correctness of programs with respect to formal specification.
CO2: Apply program verification techniques to prove and analyze correctness of programs.
CO3: Understand the problems associated with concurrent programs and their effects on their behavioral
correctness.
CO4: Understand and use a few state-of-the-art tools to model and verify sequential and concurrent systems.
CO-PO Mapping
| PO/PSO | PO1 | PO2 | PO3 | PO4 | PO5 | PO6 | PO7 | PO8 | PO9 | PO10 | PO11 | PO12 | PSO1 | PSO2 |
| CO | ||||||||||||||
| CO1 | 2 | 1 | – | – | 1 | – | – | – | – | 3 | – | – | 3 | 2 |
| CO2 | 3 | 2 | 2 | 2 | 2 | – | – | – | – | 3 | 2 | – | 3 | 2 |
| CO 3 | 2 | 1 | – | – | 1 | – | – | – | – | 3 | 2 | – | 3 | 2 |
| CO4 | 3 | 2 | 2 | 2 | 2 | – | – | – | – | 3 | 2 | – | 3 | 2 |
Evaluation Pattern: 70:30
| Assessment | Internal | End Semester |
| MidTerm Exam | 20 | |
| Continuous Assessment – Theory (*CAT) | 10 | |
| Continuous Assessment – Lab (*CAL) | 40 | |
| **End Semester | 30 (50 Marks; 2 hours exam) |
*CAT – Can be Quizzes, Assignments, and Reports
*CAL – Can be Lab Assessments, Project, and Report
**End Semester can be theory examination/ lab-based examination/ project presentation
Textbook(s)
Allan Blanchard, “Introduction to C program proof with Frama-C and its WP plugin”, 2020.
Reference(s)
Huth M, Ryan M. “Logic in Computer Science”. Second Edition, Cambridge University Press; 2004.
Jose Bacelar Almeida et al., “Rigorous Software Development: An Introduction to Program Verification”, Springer-Verlag London, 2011, ISBN: 978-0-85729- 017-5.
Ben-Ari M, “Principles of the Spin model checker”, 2008 edition, Springer Science & Business Media; 2008.
DISCLAIMER: The appearance of external links on this web site does not constitute endorsement by the School of Biotechnology/Amrita Vishwa Vidyapeetham or the information, products or services contained therein. For other than authorized activities, the Amrita Vishwa Vidyapeetham does not exercise any editorial control over the information you may find at these locations. These links are provided consistent with the stated purpose of this web site.