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

Ejemplares similares

Ejemplares similares