Skip to main content

Efficient Verification of Multi-Property Designs

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.
Close Menu