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

Ejemplares similares

Ejemplares similares