Dynamite: A tool for the verification of alloy models based on PVS

Automatic analysis of Alloy models is supported by the Alloy Analyzer, a tool that translates an Alloy model to a propositional formula that is then analyzed using off-the-shelf SAT solvers. The translation requires user-provided bounds on the sizes of data domains. The analysis is limited by the bo...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Moscato, M.M., Lopez Pombo, C.G., Frias, M.F.
Formato: JOUR
Materias:
Alloy
Alloy calculus
PVS
Unsat-cores
Alloying
Calculations
Formal logic
Theorem proving
Tools
Alloy analyzers
Automatic analysis
Critical applications
Data domains
Propositional formulas
Semi-automatics
Alloys
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_1049331X_v23_n2_p_Moscato
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_1049331X_v23_n2_p_Moscato
record_format dspace
spelling todo:paper_1049331X_v23_n2_p_Moscato2023-10-03T15:58:38Z Dynamite: A tool for the verification of alloy models based on PVS Moscato, M.M. Lopez Pombo, C.G. Frias, M.F. Alloy Alloy calculus PVS Unsat-cores Alloying Calculations Formal logic Theorem proving Tools Alloy analyzers Automatic analysis Critical applications Data domains Propositional formulas PVS Semi-automatics Unsat-cores Alloys Automatic analysis of Alloy models is supported by the Alloy Analyzer, a tool that translates an Alloy model to a propositional formula that is then analyzed using off-the-shelf SAT solvers. The translation requires user-provided bounds on the sizes of data domains. The analysis is limited by the bounds and is therefore partial. Thus, the Alloy Analyzer may not be appropriate for the analysis of critical applications where more conclusive results are necessary. Dynamite is an extension of PVS that embeds a complete calculus for Alloy. It also includes extensions to PVS that allow one to improve the proof effort by, for instance, automatically analyzing new hypotheses with the aid of the Alloy Analyzer. Since PVS sequents may get cluttered with unnecessary formulas, we use the Alloy unsat-core extraction feature in order to refine proof sequents. An internalization of Alloy's syntax as an Alloy specification allows us to use the Alloy Analyzer for producing witnesses for proving existentially quantified formulas. Dynamite complements the partial automatic analysis offered by the Alloy Analyzer with semi-automatic verification through theorem proving. It also improves the theorem proving experience by using the Alloy Analyzer for early error detection, sequent refinement, and witness generation. © 2014 ACM. Fil:Lopez 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. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_1049331X_v23_n2_p_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
Alloy calculus
PVS
Unsat-cores
Alloying
Calculations
Formal logic
Theorem proving
Tools
Alloy analyzers
Automatic analysis
Critical applications
Data domains
Propositional formulas
PVS
Semi-automatics
Unsat-cores
Alloys
spellingShingle Alloy
Alloy calculus
PVS
Unsat-cores
Alloying
Calculations
Formal logic
Theorem proving
Tools
Alloy analyzers
Automatic analysis
Critical applications
Data domains
Propositional formulas
PVS
Semi-automatics
Unsat-cores
Alloys
Moscato, M.M.
Lopez Pombo, C.G.
Frias, M.F.
Dynamite: A tool for the verification of alloy models based on PVS
topic_facet Alloy
Alloy calculus
PVS
Unsat-cores
Alloying
Calculations
Formal logic
Theorem proving
Tools
Alloy analyzers
Automatic analysis
Critical applications
Data domains
Propositional formulas
PVS
Semi-automatics
Unsat-cores
Alloys
description Automatic analysis of Alloy models is supported by the Alloy Analyzer, a tool that translates an Alloy model to a propositional formula that is then analyzed using off-the-shelf SAT solvers. The translation requires user-provided bounds on the sizes of data domains. The analysis is limited by the bounds and is therefore partial. Thus, the Alloy Analyzer may not be appropriate for the analysis of critical applications where more conclusive results are necessary. Dynamite is an extension of PVS that embeds a complete calculus for Alloy. It also includes extensions to PVS that allow one to improve the proof effort by, for instance, automatically analyzing new hypotheses with the aid of the Alloy Analyzer. Since PVS sequents may get cluttered with unnecessary formulas, we use the Alloy unsat-core extraction feature in order to refine proof sequents. An internalization of Alloy's syntax as an Alloy specification allows us to use the Alloy Analyzer for producing witnesses for proving existentially quantified formulas. Dynamite complements the partial automatic analysis offered by the Alloy Analyzer with semi-automatic verification through theorem proving. It also improves the theorem proving experience by using the Alloy Analyzer for early error detection, sequent refinement, and witness generation. © 2014 ACM.
format JOUR
author Moscato, M.M.
Lopez Pombo, C.G.
Frias, M.F.
author_facet Moscato, M.M.
Lopez Pombo, C.G.
Frias, M.F.
author_sort Moscato, M.M.
title Dynamite: A tool for the verification of alloy models based on PVS
title_short Dynamite: A tool for the verification of alloy models based on PVS
title_full Dynamite: A tool for the verification of alloy models based on PVS
title_fullStr Dynamite: A tool for the verification of alloy models based on PVS
title_full_unstemmed Dynamite: A tool for the verification of alloy models based on PVS
title_sort dynamite: a tool for the verification of alloy models based on pvs
url http://hdl.handle.net/20.500.12110/paper_1049331X_v23_n2_p_Moscato
work_keys_str_mv AT moscatomm dynamiteatoolfortheverificationofalloymodelsbasedonpvs
AT lopezpombocg dynamiteatoolfortheverificationofalloymodelsbasedonpvs
AT friasmf dynamiteatoolfortheverificationofalloymodelsbasedonpvs
_version_ 1782025131689771008

Ejemplares similares