Automated Verification IISC

I want to get the details of Automated Verification course of Indian Institute of Science IISc , Bangalore so can you provide me?

[pawan]

I am providing you the details of Automated Verification course of Indian Institute of Science IISc , Bangalore

Automated Verification course

E0 223: Automated Verification

Introduction

Computer systems in todays world are large, complex, costly, and often safety-critical. Their correctness is as critical as their performance. While testing is an indispensable technique for exploring behaviors of systems, it can rarely cover all behaviors of the system. Many bugs still make it past testing. Automated verification is an alternative to testing wherein a mathematical model of a system is built and analyzed, algorithmically, with respect to logical specifications. Some examples of successful applications of verification to real world systems are IEEE Futurebus+ cache coherence protocol, primary flight control software of Airbus A340, and Windows device drivers.

In this course, we will discuss formal modeling of systems and logical specifications of their properties. Our focus will be on understanding the core algorithmic techniques for formal analysis.

Course contents

Formal models of systems: simple programs, state transition diagrams, Kripke structures

Specification logics: propositional and first-order logic; temporal logics (CTL, LTL, CTL*); fixpoint logic: mu-calculus

Algorithmic analysis: satisfiability checking; decision procedures for satisfiability modulo theories; model checking: explicit, automata-theoretic, and symbolic

Course evaluation

Homeworks: Two homework assignments of problem solving nature will be given.
Mid-term exams: Two topic-wise mid-term exams will be conducted.

Seminar: Every student will be assigned a paper for presentation and will be required to submit a written example solved using the techniques of the paper.

End-term exam: An end-term exam covering the entire course contents will be taken.

Reference texts

Daniel Kroening, Ofer Strichman: Decision Procedures: An Algorithmic Point of View, Springer, 2008. Also available online.

Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, MIT Press, 2008.

Supplementary texts

Edmund M. Clarke, Orna Grumberg, Doron Peled: Model Checking, MIT Press, 2001.

Michael Huth, Mark Ryan: Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004.

Contact-

Indian Institute of Science
CV Raman Rd, Bengaluru, Karnataka 560012