Ultimate Automizer and the CommuHash Normal Form
Matthias Heizmann, Max Barth, Daniel Dietsch, Leonard Fichtner, Jochen Hoenicke, Dominik Klumpp, Mehdi Naouar, Tanja Schindler, Frank Schüssele, Andreas Podelski
Abstract
Abstract The verification approach of Ultimate Automizer utilizes SMT formulas. This paper presents techniques to keep the size of the formulas small. We focus especially on a normal form, called CommuHash normal form that was easy to implement and had a significant impact on the runtime of our tool.
Topics & Concepts
Computer scienceFocus (optics)Programming languageAlgorithmTheoretical computer scienceOpticsPhysicsFormal Methods in VerificationSoftware Testing and Debugging TechniquesLogic, programming, and type systems