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

MOSCATO, MARIANO MIGUEL; LOPEZ POMBO, CARLOS GUSTAVO; FRIAS, MARCELO FABIAN

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Lugar: Berlín; Año: 2010 vol. 6255 p. 275 - 289

0302-9743

According to the Verified Software Initiative manifesto, “Lightweight techniques and tools have been remarkably success- ful in finding bugs and problems in software. However, their suc- cess 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 the- orem prover PVS. Using the Alloy Analyzer during the proving process improves the PVS theorem proving experience by reducing the number of errors introduced along creative proof steps. Therefore, rather than becoming an obstacle to the goals of the Initiative, inside DPS Alloy becomes an aid. In this article we introduce new features of DPS based on the novel use of unsat cores to guide the proving process by prun- ing unnecessary information. We illustrate these new features using a non-trivial case-study coming from the networking domain.