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, N., Galeotti, J.P., Lopez Pombo, C.G., Frias, M.F.
Formato: SER
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: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 todo:paper_03029743_v5977LNCS_n_p396_Rosner
record_format dspace
spelling todo:paper_03029743_v5977LNCS_n_p396_Rosner2023-10-03T15:19:13Z ParAlloy: Towards a framework for efficient parallel analysis of alloy models Rosner, N. Galeotti, J.P. Lopez Pombo, C.G. Frias, M.F. 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. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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, N.
Galeotti, J.P.
Lopez Pombo, C.G.
Frias, M.F.
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.
format SER
author Rosner, N.
Galeotti, J.P.
Lopez Pombo, C.G.
Frias, M.F.
author_facet Rosner, N.
Galeotti, J.P.
Lopez Pombo, C.G.
Frias, M.F.
author_sort Rosner, N.
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
url http://hdl.handle.net/20.500.12110/paper_03029743_v5977LNCS_n_p396_Rosner
work_keys_str_mv AT rosnern paralloytowardsaframeworkforefficientparallelanalysisofalloymodels
AT galeottijp paralloytowardsaframeworkforefficientparallelanalysisofalloymodels
AT lopezpombocg paralloytowardsaframeworkforefficientparallelanalysisofalloymodels
AT friasmf paralloytowardsaframeworkforefficientparallelanalysisofalloymodels
_version_ 1807319863521181696

Ejemplares similares