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: López Pombo, Carlos Gustavo, Frias, Marcelo
Publicado: 2014
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:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_1049331X_v23_n2_p_Moscato
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 paper:paper_1049331X_v23_n2_p_Moscato
record_format dspace
spelling paper:paper_1049331X_v23_n2_p_Moscato2023-06-08T16:01:22Z Dynamite: A tool for the verification of alloy models based on PVS López Pombo, Carlos Gustavo Frias, Marcelo 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. 2014 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_1049331X_v23_n2_p_Moscato 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
López Pombo, Carlos Gustavo
Frias, Marcelo
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.
author López Pombo, Carlos Gustavo
Frias, Marcelo
author_facet López Pombo, Carlos Gustavo
Frias, Marcelo
author_sort López Pombo, Carlos Gustavo
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
publishDate 2014
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_1049331X_v23_n2_p_Moscato
http://hdl.handle.net/20.500.12110/paper_1049331X_v23_n2_p_Moscato
work_keys_str_mv AT lopezpombocarlosgustavo dynamiteatoolfortheverificationofalloymodelsbasedonpvs
AT friasmarcelo dynamiteatoolfortheverificationofalloymodelsbasedonpvs
_version_ 1768541664485310464

Ejemplares similares