By Dominik Strasser – VP Engineering, OneSpin Solutions
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 don’t converge after hours using one proof schedule can be resolved by a different proof method in 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 optimisation. 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 optimisation strategies to today’s junior and expert formal users.
Click the link to see the full video.