Dynamite 2.0: New Features Based on UnSAT-Core Extraction to Improve Verification of Software Requirements

According to the Verified Software Initiative manifesto, “Lightweight techniques and tools have been remarkably successful in finding bugs and problems in software. However, their success must not stop the pursuit of this projects long-term scientific ideals”.The Dynamite Proving System (DPS) blends the good qualities of the lightweight formal method Alloy with the certainty provided by the theorem prover PVS. Using the Alloy Analyzer during …