E0 272 Formal Methods in Software Engineering
January-April 2024, 2:00-3:30pm, Tue, Thu.
Room 252, CSA.
First meeting: 2:00pm Tue 06 Jan 2026.
Credits 3:1
Instructors:
Deepak D'Souza and
K. V. Raghavan. Some
modules will be taught
by Raveendra
Kumar M. of TCS Research, and Snigdha Athaiya of Siemens Technology.
TA: Mrigank Pawagi.
Lecture slides
- 06 Jan : Overview
- 08, 13, 15, 20 Jan: Alloy
- Jan 27, 29, 30, Feb 3, 10: Spin
- Feb 12, 17, 19-a, 19-e: Refinement and Rodin
- Feb 24, 26, Mar 3, 5: VCC
- Mar 12, 17, 24, 26: JPF (Taught by Snigdha Athaiya of Siemens).
- Apr 7, 9, 14, 16: AFL
(Taught by Raveendra M. of Tata Consultancy Services).
Motivation
Software is used for an increasing range of business and personal
activities, and to control vital processes and tasks. This makes it
important that software be developed efficiently, and the software be
correct and reliable. However, software development and maintenance has
largely remained mostly a human activity, with sub-optimal usage of tools
and formal processes.
This course will equip students with knowledge of the latest advances in
the role of tools and formal methods in software engineering. The course
will focus on all stages of software engineering, from requirements,
design, coding, verification, and testing.
The methodology will be to study a series
of advanced tools that address challenges faced in these steps. This will
include both an introduction to the theoretical underpinnings of these
tools, as well as hands-on exploration in class as well as
in assignments.
Syllabus
- Conceptual modeling of requirements using logic (Tool: Alloy).
- Algorithmic verification (model-checking) of design/models (Tool: Spin).
- Verifying functional correctness (Event-B models): Abstract Data
Types and refinement (Tool: Rodin).
- Verifying pre-post conditions and functional correctness of
programs: Hoare logic assertions,
refinement of a program with respect to abstract ADT specification.
(Tool: VCC).
-
White-box testing of applications (Tool: JPF).
-
Grey-box testing of applications (Tool: AFL).
Prerequisites:
Exposure to programming, and the basics of mathematical logic and
discrete structures.
Grading Weightage
| Assignments: | 50% |
| Midsem exam: | 25% |
| Final exam: | 25% |
Schedule of Exams
Mid-semester exam: 1:30pm 10 March 2026
Final exam: 2:00pm Mon 27th April 2026