Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:An SMT-Based Approach to Coverability Analysis
Speaker:Filip Niksic
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:SWS Student Defense Talks - Qualifying Exam
We use this to send out email in the morning.
Level:Expert Audience
Date, Time and Location
Date:Friday, 12 December 2014
Duration:60 Minutes
Model checkers based on Petri net coverability have been used
successfully in recent years to verify safety properties of concurrent
shared-memory or asynchronous message-passing software. We revisit a
constraint approach to coverability based on classical Petri net
analysis techniques. We show how to utilize an SMT solver to implement
the constraint approach, and additionally, to generate an inductive
invariant from a safety proof. We empirically evaluate our procedure on
a large set of existing Petri net benchmarks. Even though our technique
is incomplete, it can quickly discharge most of the safe instances.
Additionally, the inductive invariants computed are usually orders of
magnitude smaller than those produced by existing solvers.
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):
Created:Maria-Louise Albrecht/MPI-KLSB, 03/10/2016 01:42 PM Last modified:Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Maria-Louise Albrecht, 03/10/2016 01:45 PM -- Created document.