FORMAL SYSTEMS
Spring 2018-19
Taught by: Prof. Pallab Dasgupta

Teaching Assistant: Antonio Bruto da Costa, Sudipa Mandal

CLASS TIMINGS
Monday: 12:00 PM - 1:00 PM
Wednesday: 10:00 AM - 12:00 PM
Thursday: 8:00 AM - 9:00 AM


Lectures and Course Material

Sr. No.
Topic
Resources
Remarks
-
Reference Book
-
Principles of Model Checking - by Christel Baier and Joost-Pieter Katoen
1
Transition Systems
[PPTX]
Open and Closed Systems (FSMs), Transition Systems
2
Linear Time Properties
[PPTX]
 
3
Safety and Liveness Properties
[PPTX]
 
4
NuSMV (An Introduction to Model Checking)
[Slide-Set]
Go HERE to download the NuSMV binaries for your operating system.
5
Buchi Automata
[PPTX]
 
[Tutorial]
Tutorial-2 : LT Properties and Omega-Regular Expressions
[PDF]
Outline of Solutions.
If you notice any corrections required, please e-mail the TAs.
6
Temporal Logics (LTL and CTL)
[PPTX]
 
[Tutorial]
Tutorial-3 : NBAs and LTL Properties
[PDF]
Select Solutions for LTL and Omega-REs
If you notice any corrections required, please e-mail the TAs.
7
Model Checking LTL (LTL to GNBAs)
[PPTX] [PDF]
 
8
Scalability of Model Checking
[PPTX]
 
9
BDDs
[PPTX]
 
10
Program Verification and Abstractions
[PPTX]
 
11
Program Verification - The CEGAR Loop
[PPTX]
 
12
Timed Automata and TCTL
[PPTX]
Fundamential Article on Timed Automata:
Rajeev Alur and David L. Dill, "A Theory of Timed Automata", Theoretical Computer Science '94, Vol 126, Pg 183-235
-
SAT and Reachability
[Course Work - Assignment]
Zchaff - SAT Solver
EVALUATION to be held on the basis of this assignment on Monday, 8th of April 2019.
[Tutorial]
Tutorial-4 : Timed Automata
[PDF]
 
[Tutorial]
Tutorial-5 : Program Analysis and Hybrid Automata
[PDF]
 
13
Hybrid Automata
[PPTX]
 
-
Past End Semester Question Papers
[Question-Papers]