Campus Event Calendar: Andrey Rybalchenko (04/26/2007 in E1 4/019)

Campus Event Calendar

Campus Event Calendar:
- All Upcoming:
  - only for D1
  - only for D2
  - only for INET
  - only for D4
  - only for D5
  - only for D6
  - only for RG1
  - Mailing Lists
  - by Speaker
  - by Type
  - by Category
  - by Title
  - Calendar
  - RSS Feed
- History of Events:

Event Entry

What and Who

Abstraction for Liveness and Safety

Andrey Rybalchenko

Ecole Polytechnique Fédérale de Lausanne and Max Planck Institute for Computer Science

SWS Colloquium

Andrey Rybalchenko is researcher at Max Planck Institute for Computer Science in Saarbruecken and at Ecole Polytechnique Federale de Lausanne. He holds Dipl.-Inf. (2002) and Dr.-Ing. (summa cum laude, 2005) degrees from the University of Saarland, Germany. Andrey's research interests focus on automated methods and tools for formal software verification, ranging from the design of program analysis methods to the development of algorithms for symbolic computation and automated deduction. Andrey's doctoral research revolutionized verification of liveness properties for software systems by introducing ``transition invariants''. Jointly with Microsoft Research, Andrey developed the Terminator tool, which is the first tool to perform automatic verification of liveness properties for software. He is also developing the ARMC tool for automatically proving safety properties of complex infinite state systems, which has been successfully applied for the verification of safety critical parts of the European Train Control System. Andrey is a recipient of Guenther Hotz medal (2002) from the University of Saarland and Otto Hahn medal (2005) from the Max Planck Society.

AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2

Expert Audience

English

Note: We use this to send email in the morning.

Date, Time and Location

Thursday, 26 April 2007

15:00

-- Not specified --

E1 4

019

Saarbrücken

Abstract

We present new approaches to verification of liveness and safety properties of software. Proving liveness properties of programs is central to the process of ensuring that software systems can always react. Verification of liveness properties had been an open problem since 1970s, due to the lack of modular termination arguments and adequate abstraction techniques. We highlight our experience in developing the theoretical foundations for the first software verification tool for termination that provides capacity for large program fragments (of more than 20,000 lines of code) together with support for programming language features such as arbitrarily nested loops, pointers, function-pointers, side-effects, etc. We also describe our experience in applying the tool on device driver dispatch routines from the Windows operating system. In the second part of the talk, we will focus on abstraction techniques that are at heart of state-of-the-art verification tools for safety. We address their limitations, which severely restrict the practical applicability. We propose a new approach for finding abstraction of a program that overcomes the inherent limitations of current abstraction refinement schemes.

Contact

Brigitta Hansen

0681 - 9325203

--email hidden

System used:

Meeting URL:

Meeting ID:

Passcode:

passcode not visible

Code Visible for:

logged in users only

Uwe Brahm, 04/19/2007 10:07
Brigitta Hansen, 04/18/2007 12:58
Brigitta Hansen, 04/18/2007 12:23 -- Created document.

Imprint / Impressum | Data Protection / Datenschutzhinweis