|
CS Home
Dept Info/Contacts
People
Research
Events
Courses
Undergrad Programs:
Computer Science
Informatics
Graduate Program
Prospective Students
Faculty Hiring
Employment
Resources
Help Lab Hours
Student Groups
Support the Department: Weeg Professorship
|
|
Advances in Automated Verification of Data Flow Programs
Prof. Cesare Tinelli
Department of Computer Science
University of Iowa
Friday, May 02, 2008
4:00-5:000pm, 140 SH
Abstract
Data flow languages are high level programming languages commonly used
in industry to model and implement reactive embedded systems
controlling all sort of devices (from vending machines to airplanes).
We present a general approach for proving automatically the
correctness of data flow programs with respect to safety properties,
properties that must hold in every state of a program's execution. The
approach extends and combines Model Checking with Satisfiability
Modulo Theories (SMT) techniques. In it, a given program and safety
property are first translated into logical formulas belonging to a
decidable fragment of first-order logic that includes the combined
theory of the programs data types--such as integers, reals, Booleans
and so on. Then the property is proved by induction over the length of
program executions using an SMT solver specialized on that theory. A
distinguishing feature of this approach is that it can check safety
properties of infinite-state data flow programs as well as
finite-state ones. This talk will provide a high level description of
the basic approach and its main enhancements as applied to the data
flow language Lustre. Then it will present experimental results
comparing our initial implementation of the approach with existing
verifiers for Lustre.
This is joint work with George Hagen.
|
