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. © 2010 Springer-Verlag.
Registro:
Documento: |
Artículo
|
Título: | Dynamite 2.0: New features based on UnSAT-core extraction to improve verification of software requirements |
Autor: | Moscato, M.M.; López Pombo, C.G.; Frias, M.F. |
Ciudad: | Natal |
Filiación: | Department of Computer Science, FCEyN, Universidad de Buenos Aires, Argentina Department of Computer Engineering, Technological Institute of Buenos Aires (ITBA), CONICET, Argentina
|
Palabras clave: | Alloy analyzers; Lightweight formal methods; Networking domain; Non-trivial; Proof steps; Software requirements; Theorem provers; Unsat cores; Alloys; Feature extraction; Formal methods; Program debugging; Verification; Theorem proving |
Año: | 2010
|
Volumen: | 6255 LNCS
|
Página de inicio: | 275
|
Página de fin: | 289
|
DOI: |
http://dx.doi.org/10.1007/978-3-642-14808-8_19 |
Título revista: | 7th International Colloquium on Theoretical Aspects of Computing, ICTAC 2010
|
Título revista abreviado: | Lect. Notes Comput. Sci.
|
ISSN: | 03029743
|
Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v6255LNCS_n_p275_Moscato |
Referencias:
- Arkoudas, K., (2001) Type-ω DPLs, , MIT AI Memo 2001-27
- Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M., Integrating Model Checking and Theorem Proving for Relational Reasoning (2003) Proceedings of RelMiCS 2003, , Springer, Heidelberg
- Böhme, S., Nipkow, T., Sledgehammer: Judgement Day (2010) IJCAR 2010, , to appear
- Blanchette, J.C., Nipkow, T., Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder (2009) TAP 2009
- Dunets, A., Schellhorn, G., Reif, W., Automated Flaw Detection in Algebraic Specifications (2010) Journal of Automated Reasoning
- Eén, N., Sörensson, N., MiniSat-p-v1.14 (2006) A Proof-logging Version of MiniSat, , September
- Frias, M.F., López Pombo, C.G., Moscato, M.M., Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications (2007) LNCS, 4424, pp. 587-601. , Grumberg, O., Huth, M. (eds.) TACAS 2007. Springer, Heidelberg
- Hoare, C.A.R., Leavens, G.T., Misra, J., Shankar, N., (2007) The Verified Software Initiative: A Manifesto
- Jackson, D., Alloy: A lightweight object modelling notation (2002) ACM Transactions on Software Engineering and Methodology, 11, pp. 256-290
- Jackson, D., Schechter, I., Shlyakhter, I., Alcoa: The Alloy Constraint Analyzer (2000) ICSE 2000, pp. 730-733
- Kang, E., Jackson, D., Formal Modeling and Analysis of a Flash Filesystem in Alloy (2008) LNCS, 5238, pp. 294-308. , Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008 Springer, Heidelberg
- Owre, S., Rushby, J.M., Shankar, N., PVS: A prototype verification system (1992) LNCS (LNAI), 607, pp. 148-752. , Kapur, D. (ed.) CADE 1992. Springer, Heidelberg
- Pudlák, P., Semantic Selection of Premisses for Automated Theorem Proving (2007) Proceedings of ESARLT 2007, pp. 27-44
- Ramananandro, T., Mondex, an electronic purse: Specification and refinement checks with the Alloy model-finding method (2008) Formal Aspects of Computing, 20 (1), pp. 21-39
- Sutcliffe, G., Puzis, Y., (2007) SRASS a Semantic Relevance Axiom Selection System, , http://www.cs.miami.edu/~tptp/ATPSystems/SRASS/
- Torlak, E., Chang, F., Jackson, D., Finding Minimal Unsatisfiable Cores of Declarative Specifications (2008) LNCS, 5014, pp. 326-341. , Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. Springer, Heidelberg
- Torlak, E., Jackson, D., Kodkod: A Relational Model Finder (2007) LNCS, 4424, pp. 632-647. , Grumberg, O., Huth, M. (eds.) TACAS 2007. Springer, Heidelberg
- Urban, J., MaLARea: A Metasystem for Automated Reasoning in Large Theories (2007) Proceedings of ESARLT 2007, pp. 45-58
- Weber, T., Integrating a SAT Solver with an LCF-style Theorem Prover ENTCS, 144 (2), pp. 67-78. , Proceedings of PDPAR 2005
- Weber, T., (2008) SAT-based Finite Model Generation for Higher-Order Logic, , Ph.D. Thesis, TUM
- Zave, P., Compositional binding in network domains (2006) LNCS, 4085, pp. 332-347. , Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006 Springer, Heidelberg
Citas:
---------- APA ----------
Moscato, M.M., López Pombo, C.G. & Frias, M.F.
(2010)
. Dynamite 2.0: New features based on UnSAT-core extraction to improve verification of software requirements. 7th International Colloquium on Theoretical Aspects of Computing, ICTAC 2010, 6255 LNCS, 275-289.
http://dx.doi.org/10.1007/978-3-642-14808-8_19---------- CHICAGO ----------
Moscato, M.M., López Pombo, C.G., Frias, M.F.
"Dynamite 2.0: New features based on UnSAT-core extraction to improve verification of software requirements"
. 7th International Colloquium on Theoretical Aspects of Computing, ICTAC 2010 6255 LNCS
(2010) : 275-289.
http://dx.doi.org/10.1007/978-3-642-14808-8_19---------- MLA ----------
Moscato, M.M., López Pombo, C.G., Frias, M.F.
"Dynamite 2.0: New features based on UnSAT-core extraction to improve verification of software requirements"
. 7th International Colloquium on Theoretical Aspects of Computing, ICTAC 2010, vol. 6255 LNCS, 2010, pp. 275-289.
http://dx.doi.org/10.1007/978-3-642-14808-8_19---------- VANCOUVER ----------
Moscato, M.M., López Pombo, C.G., Frias, M.F. Dynamite 2.0: New features based on UnSAT-core extraction to improve verification of software requirements. Lect. Notes Comput. Sci. 2010;6255 LNCS:275-289.
http://dx.doi.org/10.1007/978-3-642-14808-8_19