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.
