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)|
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 behaviors that cause the properties in the debugging set to fail must be fixed first.
|Speaker Bio:||Matthias is a senior research engineer at Diffblue where he develops automated verfication 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.|