Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4
What and Who
Directed Explicit-State Model Checking
Stefan Leue
Uni Freiburg
Logik-Seminar
AG 1, AG 2, AG 3, AG 4
Expert Audience
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 13 February 2003
16:15
-- Not specified --
46.1 - MPII
HS 024
Saarbrücken
Abstract
Model Checking has proven to be an effective software verification
technique. Explicit-state model checking, as for instance implemented
in the popular tool SPIN, has proven particularly successful in
the analysis of concurrent software systems. The popularity of
explicit-state model checkers is due to, amongst others, the fact that
when a property violation is found, the model checker returns a trail
leading from the initial system state into the property violating
state. This greatly helps fault explanation. Most explicit-state model
checkers perform depth-first searches on the state space. While this
is memory efficient, the resulting error trails can be very long.
We discuss alternatives to the state space explorations that address
this problem. These include breadth-first searches, iterated deepening
searches, and, most importantly, heuristic guide searches such as A*
and iterative deepening A*. We will show how heuristic functions can
be determined and illustrate applications of directed explicit-state
model checking to the validation of safety and liveness properties. We
finally prove that directed explicit-state model checking can be used
effectively even in the presence of partial-order reduction.
______________________________________________________________________
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-227,
uni-intern: 92227, E-Mail: #email not disclosed#
Contact
--email hidden
passcode not visible
logged in users only
Uwe Brahm, 04/12/2007 12:20 -- Created document.