GIAN Course on

Verification of Cyber Physical Systems

8-12 January 2018
Indian Institute of Science, Bangalore.



About the course

Cyber-physical systems (CPS) are a new genre of software controlled physical systems that arise in applications involving automotive, aerospace, robotics, process control and medical devices. They integrate computation, control and communication in novel ways to provide sophisticated functionalities such as autonomous driving in self-driving cars and automated load balancing in smart grids. On one hand, CPS enable systems that guarantee enhanced safety, security and efficiency. On the other hand, they are extremely safety critical, since, software or system errors can be disastrous. The grand challenge towards the development and deployment of CPS is to develop methodology that can provide high-confidence in their correct functioning.

Formal methods is a branch of computer science that deals with rigorous methods for analysis of systems that provide provable guarantees about the correctness. A verification algorithm takes as input a mathematical model of the system and a formal unambiguous description of the correctness specification and outputs a proof of the correctness of the system in the case that the system is correct.

In this course, we will discuss state-of-the-art formal verification techniques for CPS design and analysis. In particular, we will focus on an important aspect of CPS, namely, the interaction between discrete and continuous elements that arise as a result of the interaction of software (discrete) with physical systems (continuous). We capture these behaviors in the framework of hybrid automata, and provide detailed coverage of the core algorithms and software tools that have been developed for the verification of these hybrid automata.


The venue of the workshop is Room L9, Center for Continuing Education (CCE), (Opposite Security Office, ATM Gate) IISc, Bangalore 560012.

Fees and Registration

Category Fees
Non-Indian USD 500
Indian Industry INR 15,000
Indian Academic / Government Research Lab INR 10,000
Indian Student INR 2,000

Those who would like to attend the course are requested to register themselves on the GIAN portal, and then on the course registration page.

Limited on-campus accommodation is available, and can be provided on request and payment of applicable charges.

Schedule of talks

Day Time Title Lecturer
Mon, 8 Jan 2018 9:30am Introduction to Hybrid Automata: Syntax, Semantics, Examples Pavithra Prabhakar
11:00am Coffee Break
11:30am Specifications: Linear Temporal Logics, Metric Temporal Logics; Satisfiability Pavithra Prabhakar
1:00pm Lunch
2:00pm Tutorial: Modeling and Simulation of Hybrid Automata, Specification writing.
Tue, 9 Jan 2018 9:30am Finite state automata, invariant/safety verification Deepak D'Souza
11:00am Coffee Break
11:30am Model-checking LTL/CTL Deepak D'Souza
1:00pm Lunch
2:00pm Tutorial: Model-Checking with SPIN
Wed, 10 Jan 2018 9:30am Continuous dynamical systems, solutions Pavithra Prabhakar
11:00am Coffee Break
11:30am Stability analysis, eigen value and Lyapunov function based analysis Pavithra Prabhakar
1:00pm Lunch
2:00pm Tutorial: Template based Lyapunov function search in SOSTOOLS
Thu, 11 Jan 2018 9:30am Symbolic state-space exploration, Flowpipe construction, Data structures such as Zonotopes Pavithra Prabhakar
11:00am Coffee Break
11:30am Bounded Safety Verification using SMT solvers, Bounded Error Approximations Pavithra Prabhakar
1:00pm Lunch
2:00pm Tutorial: Using the BEAVER tool, bounded safety verification of robot navigation
Fri, 12 Jan 2018 9:30am Safety Verification: Predicate abstraction, Abstractions of dynamics using Hybridization, and CEGAR Pavithra Prabhakar
11:00am Coffee Break
11:30am Stability Verification: Predicate Abstraction, Hybridization and CEGAR for stability Pavithra Prabhakar
1:00pm Lunch
2:00pm Tutorial: AVERIST tool illustrating predicate abstraction, hybridization and CEGAR


Deepak D'Souza, IISc Bangalore
Phone: 91-80-22932368