MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

An SMT-Based Approach to Coverability Analysis

Filip Niksic
MMCI
SWS Student Defense Talks - Qualifying Exam
SWS  
Expert Audience
English

Date, Time and Location

Friday, 12 December 2014
14:00
60 Minutes
G26
111
Kaiserslautern

Abstract

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.

Contact

--email hidden
passcode not visible
logged in users only

Maria-Louise Albrecht, 03/10/2016 13:45 -- Created document.