ParAlloy: Towards a framework for efficient parallel analysis of alloy models

Alloy [Jac02a] is a widely adopted relational modeling language. Its appealing syntax and the support provided by the Alloy Analyzer [Jac02b] tool make model analysis accessible to a public of non-specialists. A model and property are translated to a propositional formula, which is fed to a SAT-solv...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Rosner, Nicolás, Galeotti, Juan Pablo, López Pombo, Carlos Gustavo, Frias, Marcelo
Publicado:	2010
Materias:	Alloy analyzers Data domains Model analysis Parallel analysis Propositional formulas Relational modeling SAT solvers SAT-solving Abstracting Alloys Contour followers Cerium alloys
Acceso en línea:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5977LNCS_n_p396_Rosner http://hdl.handle.net/20.500.12110/paper_03029743_v5977LNCS_n_p396_Rosner
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paper:paper_03029743_v5977LNCS_n_p396_Rosner
record_format	dspace
spelling	paper:paper_03029743_v5977LNCS_n_p396_Rosner2023-06-08T15:28:35Z ParAlloy: Towards a framework for efficient parallel analysis of alloy models Rosner, Nicolás Galeotti, Juan Pablo López Pombo, Carlos Gustavo Frias, Marcelo Alloy analyzers Data domains Model analysis Parallel analysis Propositional formulas Relational modeling SAT solvers SAT-solving Abstracting Alloys Contour followers Cerium alloys Alloy [Jac02a] is a widely adopted relational modeling language. Its appealing syntax and the support provided by the Alloy Analyzer [Jac02b] tool make model analysis accessible to a public of non-specialists. A model and property are translated to a propositional formula, which is fed to a SAT-solver to search for counterexamples. The translation strongly depends on user-provided bounds for data domains called scopes - the larger the scopes, the more confident the user is about the correctness of the model. Due to the intrinsic complexity of the SAT-solving step, it is often the case that analyses do not scale well enough to remain feasible as scopes grow. © 2010 Springer. Fil:Rosner, N. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Galeotti, J.P. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 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. 2010 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5977LNCS_n_p396_Rosner http://hdl.handle.net/20.500.12110/paper_03029743_v5977LNCS_n_p396_Rosner
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 Data domains Model analysis Parallel analysis Propositional formulas Relational modeling SAT solvers SAT-solving Abstracting Alloys Contour followers Cerium alloys
spellingShingle	Alloy analyzers Data domains Model analysis Parallel analysis Propositional formulas Relational modeling SAT solvers SAT-solving Abstracting Alloys Contour followers Cerium alloys Rosner, Nicolás Galeotti, Juan Pablo López Pombo, Carlos Gustavo Frias, Marcelo ParAlloy: Towards a framework for efficient parallel analysis of alloy models
topic_facet	Alloy analyzers Data domains Model analysis Parallel analysis Propositional formulas Relational modeling SAT solvers SAT-solving Abstracting Alloys Contour followers Cerium alloys
description	Alloy [Jac02a] is a widely adopted relational modeling language. Its appealing syntax and the support provided by the Alloy Analyzer [Jac02b] tool make model analysis accessible to a public of non-specialists. A model and property are translated to a propositional formula, which is fed to a SAT-solver to search for counterexamples. The translation strongly depends on user-provided bounds for data domains called scopes - the larger the scopes, the more confident the user is about the correctness of the model. Due to the intrinsic complexity of the SAT-solving step, it is often the case that analyses do not scale well enough to remain feasible as scopes grow. © 2010 Springer.
author	Rosner, Nicolás Galeotti, Juan Pablo López Pombo, Carlos Gustavo Frias, Marcelo
author_facet	Rosner, Nicolás Galeotti, Juan Pablo López Pombo, Carlos Gustavo Frias, Marcelo
author_sort	Rosner, Nicolás
title	ParAlloy: Towards a framework for efficient parallel analysis of alloy models
title_short	ParAlloy: Towards a framework for efficient parallel analysis of alloy models
title_full	ParAlloy: Towards a framework for efficient parallel analysis of alloy models
title_fullStr	ParAlloy: Towards a framework for efficient parallel analysis of alloy models
title_full_unstemmed	ParAlloy: Towards a framework for efficient parallel analysis of alloy models
title_sort	paralloy: towards a framework for efficient parallel analysis of alloy models
publishDate	2010
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5977LNCS_n_p396_Rosner http://hdl.handle.net/20.500.12110/paper_03029743_v5977LNCS_n_p396_Rosner
work_keys_str_mv	AT rosnernicolas paralloytowardsaframeworkforefficientparallelanalysisofalloymodels AT galeottijuanpablo paralloytowardsaframeworkforefficientparallelanalysisofalloymodels AT lopezpombocarlosgustavo paralloytowardsaframeworkforefficientparallelanalysisofalloymodels AT friasmarcelo paralloytowardsaframeworkforefficientparallelanalysisofalloymodels
_version_	1768541938303107072

ParAlloy: Towards a framework for efficient parallel analysis of alloy models

Ejemplares similares