Logik-Sem., 17.07.06, P. Revesz
Uwe Waldmann
Einladung zum Vortrag
Zeit: Montag, 17.07.06, 11.15 Uhr
Ort: Hörsaal 023, MPI Saarbrücken (Geb. E1.4)
Peter Revesz (University of Nebraska-Lincoln):
Constraint-Database Tools for Software Verification
Zusammenfassung:
One approach to software verification is based on finding
(an approximation of) the reachability set of transition systems.
Such an approximation then can be used for either falsification or
verification of given complex error conditions about transitions
systems. To make this approach practical, we rely on several
deep and interesting connections between constraint databases and
transition systems. We show how the reachability sets of transition
systems can be computed using existing constraint database systems,
such as the MLPQ (www.cse.unl.edu/~revesz/MLPQ/mlpq.htm) or other
constraint database systems that can compute a precise,
overapproximation, or underapproximation of the least fixed point
model of recursive (Datalog-based) constraint database queries.
After giving some examples of how this works in practice, we explain
the essence of the constraint database theory which makes this
possible. We explain that often the constraint database query
optimization and evaluation techniques are more sophisticated
than any of their analogues in the software verification area.
For example, the constraint database techniques involve new
quantifier elimination methods that are more powerful than that
for Presburger arithmetic and "simplification rules" that can be
favorably compared with "meta-transitions" and "accelerations"
used in transition systems.
______________________________________________________________________
Das Logikseminar ist eine gemeinsame Veranstaltung des DFKI, des MPI
und der Fachrichtungen Informatik, Philosophie und Rechtswissenschaft.
Vortragswünsche bitte an Uwe Waldmann, MPI, Tel.: (0681) 9325-205,
uni-intern: 92205, E-Mail: u...@mpi-sb.mpg.de