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 (...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Moscato, M.M., López Pombo, C.G., Frias, M.F.
Formato: SER
Materias:
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
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_03029743_v6255LNCS_n_p275_Moscato
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_03029743_v6255LNCS_n_p275_Moscato
record_format dspace
spelling todo:paper_03029743_v6255LNCS_n_p275_Moscato2023-10-03T15:19:14Z Dynamite 2.0: New features based on UnSAT-core extraction to improve verification of software requirements Moscato, M.M. López Pombo, C.G. Frias, M.F. 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 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. Fil:López Pombo, C.G. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Frias, M.F. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v6255LNCS_n_p275_Moscato
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic 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
spellingShingle 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
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
topic_facet 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
description 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.
format SER
author Moscato, M.M.
López Pombo, C.G.
Frias, M.F.
author_facet Moscato, M.M.
López Pombo, C.G.
Frias, M.F.
author_sort Moscato, M.M.
title Dynamite 2.0: New features based on UnSAT-core extraction to improve verification of software requirements
title_short Dynamite 2.0: New features based on UnSAT-core extraction to improve verification of software requirements
title_full Dynamite 2.0: New features based on UnSAT-core extraction to improve verification of software requirements
title_fullStr Dynamite 2.0: New features based on UnSAT-core extraction to improve verification of software requirements
title_full_unstemmed Dynamite 2.0: New features based on UnSAT-core extraction to improve verification of software requirements
title_sort dynamite 2.0: new features based on unsat-core extraction to improve verification of software requirements
url http://hdl.handle.net/20.500.12110/paper_03029743_v6255LNCS_n_p275_Moscato
work_keys_str_mv AT moscatomm dynamite20newfeaturesbasedonunsatcoreextractiontoimproveverificationofsoftwarerequirements
AT lopezpombocg dynamite20newfeaturesbasedonunsatcoreextractiontoimproveverificationofsoftwarerequirements
AT friasmf dynamite20newfeaturesbasedonunsatcoreextractiontoimproveverificationofsoftwarerequirements
_version_ 1782029170533990400

Ejemplares similares