Navegar

Colección

Datos Estadísticas

Artículo

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" (2010) 7th International Colloquium on Theoretical Aspects of Computing, ICTAC 2010. 6255 LNCS:275-289
La versión final de este artículo es de uso interno. El editor solo permite incluir en el repositorio el artículo en su versión post-print. Por favor, si usted la posee enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

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