ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy Models

Nicolás Rosner, Juan P. Galeotti, Carlos López Pombo, Marcelo F. Frias
Digital Printed Abstract View Cite
Type
Short Paper
Publication
2nd International Conference on ASM, Alloy, B, and Z (ABZ'10)

Abstract

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{RosnerGPF10,
  author       = {Nicol{\'{a}}s Rosner and
                  Juan P. Galeotti and
                  Carlos L{\'{o}}pez Pombo and
                  Marcelo F. Frias},
  editor       = {Marc Frappier and
                  Uwe Gl{\"{a}}sser and
                  Sarfraz Khurshid and
                  R{\'{e}}gine Laleau and
                  Steve Reeves},
  title        = {ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy
                  Models},
  booktitle    = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
                  {ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5977},
  pages        = {396--397},
  publisher    = {Springer},
  year         = {2010},
  url          = {https://doi.org/10.1007/978-3-642-11811-1\_33},
  doi          = {10.1007/978-3-642-11811-1\_33},
  timestamp    = {Mon, 03 Mar 2025 20:58:01 +0100},
  biburl       = {https://dblp.org/rec/conf/asm/RosnerGPF10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'10

Related