Efficient Verification of Multi-Property Designs2018-05-31T14:24:30+00:00

Verification Futures 2018

Conference:Verification Futures 2018 (click here to see full programme)
Speaker:Matthias Güdemann, Senior Research Engineer. Diffblue
Presentation Title:Efficient Verification of Multi-Property Designs (The Benefit of Wrong Assumptions)
Abstract:We consider the problem of efficiently checking a set of safety properties P1,…., Pk of one design. We introduce a new approach called JA-verification where JA stands for” Just-Assume”(as opposed to” assume-guarantee”). In this approach, when proving property Pi, one assumes that every property Pj for j!= i holds. The process of proving properties either results in showing that P1,…., Pk hold without any assumptions or finding a” debugging set” of properties. The latter identifies a subset of failed properties that cause failure of other properties. The design behaviours that cause the properties in the debugging set to fail must be fixed first.

Topics Covered:

  • Formal Verification
  • Model checking
  • Multi-properties
Speaker Bio:Matthias is a senior research engineer at Diffblue where he develops automated verification tools for C and Java as well as tool for hardware verification. Before joining Diffblue he worked in the French railway industry on formal verification of autonomous light rail systems.