This year’s Oski Deep Bound Track Hardware Model Checking Competition (HWMCC) was a thrillingly close contest that came down to just one benchmark design of more than 100 benchmarks. The winner was announced at the Hardware Model Checking Competition Report session of the annual Formal Methods in Computer-Aided Design (FMCAD) Conference, held in Austin, Texas, on September 30, 2015. Winner Norbert Manthey of the Institute of Artificial Intelligence and a graduate of TU Dresden, Germany, took the prized first place from runners up Alberto Griggio, and Marco Roveri, researchers at Fondazione Bruno Kessler, and graduates of the University of Trento, Italy.
“The model checking solvers in the HWMCC competition continue to keep pace with industrial-strength model checkers. Oski Technology relies on advances in this technolology to deploy End-to-End formal verification methodology across the most complex designs in the industry” notes Oski Technology president and CEO, Vigyan Singhal, who congratulated this year’s winner and the runners up of the Oski Deep Bounds Award, and emphasized the outstanding calibre of the competition entries.
The Oski Deep Bounds Award was designed to recognize exceptional technological achievement for solutions that achieve deep bounds, and the model checking solvers in the competition continue to keep pace with industrial-strength model checkers.
Armin Biere is the organizer of HWMCC 2015, the competitive event for hardware model checkers, and also a professor of computer science at Jonannes Kepler University in Linz, Austria. HWMCC is a driving force to improve model checkers and encourages participants to present their work and share results with a broader audience. Entrants were invited to solve benchmarks in the AIGER format.
FMCAD is the leading conference and forum on formal methods theory and applications in hardware and system verification, where HWMCC is co-located.