Campus Event Calendar
Event Entry
What and Who
Modularity in Automated Reasoning and the Verification of Complex Systems
Viorica Sofronie-Stokkermans
Max-Planck-Institut für Informatik - RG 1
Senior Reseacher Series
AG 1, AG 3, AG 4, AG 5, SWS, RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 3 June 2009
16:00
60 Minutes
E1 4
024
Saarbrücken
Abstract
Due to the enormous speed in the development of information technology,
complex systems with embedded software are nowadays used in households,
cars, trains, planes or power plants. In all these areas, but especially
in safety critical domains, errors may have catastrophic effects.
It is therefore very important to automatically detect errors, and to
provide correctness guarantees for such systems.
For formally expressing the properties and evolution of systems one needs
to use numerical information, information about functions with certain
properties, and often also about data structures. Verification tasks can
often be reduced to validity or satisfiability tests in theories of
mathematics or logic expressive enough to capture all aspects mentioned
above.(These are usually extensions of standard theories with additional
functions, or combinations thereof.) It is therefore important to develop
efficient methods for reasoning in complex theories.
We describe a method which allows us to reduce proof tasks in combinations
of theories, modularly, to proof tasks in the component theories. The method
is flexible and efficient, and is sound and complete for a large class of
theories. We will discuss its applications in various domains (mathematics,
verification of real time or hybrid systems, and distributed terminological
databases). We will then address the problem of verifying systems consisting
of several interacting components, mentioning a theoretical framework
for the modular verification of such complex systems.
complex systems with embedded software are nowadays used in households,
cars, trains, planes or power plants. In all these areas, but especially
in safety critical domains, errors may have catastrophic effects.
It is therefore very important to automatically detect errors, and to
provide correctness guarantees for such systems.
For formally expressing the properties and evolution of systems one needs
to use numerical information, information about functions with certain
properties, and often also about data structures. Verification tasks can
often be reduced to validity or satisfiability tests in theories of
mathematics or logic expressive enough to capture all aspects mentioned
above.(These are usually extensions of standard theories with additional
functions, or combinations thereof.) It is therefore important to develop
efficient methods for reasoning in complex theories.
We describe a method which allows us to reduce proof tasks in combinations
of theories, modularly, to proof tasks in the component theories. The method
is flexible and efficient, and is sound and complete for a large class of
theories. We will discuss its applications in various domains (mathematics,
verification of real time or hybrid systems, and distributed terminological
databases). We will then address the problem of verifying systems consisting
of several interacting components, mentioning a theoretical framework
for the modular verification of such complex systems.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 05/27/2009 11:06
Jennifer Müller, 03/04/2009 08:35 -- Created document.
Jennifer Müller, 03/04/2009 08:35 -- Created document.