Formal users know that selecting the right proof engine and its related parameters can make a huge difference in runtime. In some cases, assertion checks that run for many hours, only to return an inconclusive proof result, may be manually optimized to achieve unbounded proofs within minutes.
While dealing with proof engines may be interesting for formal experts, ideally users should be able to predict runtime and obtain unbounded proofs, even without any knowledge of the proof engines within tools. Data analysis and machine learning algorithms provide new approaches to automated proof optimization. In this presentation, we show how OneSpin has leveraged formal verification data accumulated over the course of almost 20 years to deliver the next generation of automatic proof optimization strategies to today’s junior and expert formal users.
Dominik Strasser, co-founder of OneSpin Solutions, was named VP Engineering in June 2012. He has a track record of 20+ years in engineering management and engineering.Since 2005 he headed the development of OneSpin’s flagship product 360DV. Prior to OneSpin, Strasser led the formal verification development group at Infineon Technologies in Munich. Previously, at Siemens, he led industrial research projects on formal verification and industrial computing at the company’s Corporate Research Lab in Germany.
He began his career in the compiler department of Siemens Nixdorf doing C and C++ compilers for Unix and mainframe operating systems.DominikStrasser holds a Diplom-Informatiker (equivalent to a master’s degree in computer science) from the Munich Technical University, Germany.
DVCLUB Europe is made possible through the generosity of our sponsors.