Paper Info
Title
Dynamite 2.0: new features based on UnSAT-core extraction to improve verification of software requirements
Abstract
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 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 pruning unnecessary information. We illustrate these new features using a non-trivial case-study coming from the networking domain.
Year
DOI
Venue
2010
10.1007/978-3-642-14808-8_19
ICTAC
Keywords
Field
DocType
unsat-core extraction,pvs theorem,dynamite proving system,software requirement,creative proof step,lightweight formal method alloy,lightweight technique,verified software initiative manifesto,new feature,dps alloy,alloy analyzer,theorem prover,theorem proving,software requirements
Obstacle,Programming language,Computer science,Alloy Analyzer,Automated theorem proving,Theoretical computer science,Dynamite,Software,Formal methods,Rule of inference,Software requirements
Conference
Volume
ISSN
ISBN
6255
0302-9743
3-642-14807-7
Citations 
PageRank 
References 
3
0.43
20
Authors
3
Name
Order
Citations
PageRank
Mariano M. Moscato1205.04
Carlos G. Lopez Pombo21448.51
Marcelo F. Frias329535.57