close By using this website, you agree to the use of cookies. Detailed information on the use of cookies on this website can be obtained on OneSpin's Privacy Policy. At this point you may also object to the use of cookies and adjust the browser settings accordingly.

Formal Engines Learn from Experience

By Chris Edwards, Tech Design Forum | Feat. Dominik Strasser, VP Engineering, OneSpin


OneSpin’s work found that solver orchestration based on machine learning is effective. The company is armed with more than two decades worth of collected designs that extend as far back as the team’s original work at Siemens in the early 1990s.

Dominik Strasser, vice president of engineering at OneSpin, says with the machine-learning functions: “Users do not normally have to pick proof algorithms and we now have a system that has faster proofs for time-to-hold,” adding that time-to-fail has rarely been an issue.


As part of its ongoing work into applying AI to formal, a new project at OneSpin is aimed at helping with the debug process. “The tool finds out which part is the culprit. This is a very difficult problem to solve and a task for the future but we have some intermediate results. But don’t hold your breath,” Strasser says.

Another path OneSpin aims to pursue is using deep learning to analyse verification data. “Maybe then the runtime prediction will get better results,” Strasser hopes.


Related Links