Formal Methods- Spring 2017-18

FORMAL METHODS Spring 2017-18
Taught by: Prof. Pallab Dasgupta Teaching Assistant: Antonio Bruto da Costa CLASS TIMINGS Monday: 10:00 AM - 11:00 AM Wednesday: 8:00 AM - 10:00 AM Thursday: 10:00 AM - 11:00 AM

Course Material

Topic	Resources	Remarks
Slideset 1 (Model Checking - Baier and Katoen)	[ZIP]
Succinct Representations	[PPTX]
Slideset 2 (Verification Slides: BDD,BMC,CEGAR)	[ZIP]
Class Test 1	[QP] [Solution Outline]
Bounded Model Checking	[ZIP]
Timed Automata	[PPTX] [Other Material (ZIP)] [Other Slides (ZIP)]	Tutorial-1 Tutorial-2 Tutorial-3
The UPPAAL Model Checker	[Material (ZIP)] [Tool JAR]	[Tool Page]
Term Project and Report	[Assignment Problem Statement]	Submissions to be e-mailed to antonio@iitkgp.ac.in
Hybrid Systems and Hybrid Automata	[Slides] [Introduction to HA (not to be distributed)]	Tutorial on Hybrid Systems and Program Analysis
Program Verification	[Slides]	1. Build the Characteristic Function for the Predicate Abstraction described on slide 32 of this slideset. [NOTE] Slide 49 of the Predicate Abstraction material has a typo: Interpret as C=> and ~C=> instead of B=> and ~B=> 2. Slide 49: Consider assert(~(y>x)) and identify the wp(y--) in the if block.