Alloy

Alloy: A new technology for software modelling. Alloy is a lightweight language for software modelling. It’s designed to be flexible and expressive, and yet amenable to fully automatic simulation and checking. At its core, Alloy is a simple first order logic extended with relational operators. A simple structuring mechanism allows Alloy to be used in a variety of idioms, and supports incremental construction of models. Alloy is analyzed by translation to SAT. The current version of the tool uses the Chaff and Berkmin solvers; these are powerful enough to handle a search space of 2 100 or more. Alloy has been applied to problems from very different domains, from checking the conventions of Microsoft COM to debugging the design of a name server. Most recently, we have used it to check distributed algorithms that are designed for arbitrary topologies. We are also investigating the use of Alloy to analyze object-oriented code.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 28 articles , 1 standard article )

Showing results 1 to 20 of 28.
Sorted by year (citations)

1 2 next

  1. Cristiá, Maximiliano; Rossi, Gianfranco: A set solver for finite set relation algebra (2018)
  2. Joosten, Sebastiaan J. C.: Finding models through graph saturation (2018)
  3. Wickerson, John; Batty, Mark; Sorensen, Tyler; Constantinides, George A.: Automatically comparing memory consistency models (2017)
  4. Cristiá, Maximiliano; Rossi, Gianfranco; Frydman, Claudia: Adding partial functions to constraint logic programming with sets (2015)
  5. Schneider, Steve; Treharne, Helen; Wehrheim, Heike: The behavioural semantics of Event-B refinement (2014)
  6. Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
  7. Giese, Holger; Lambers, Leen: Towards automatic verification of behavior preservation for model transformation via invariant checking (2012)
  8. Hallé, Sylvain; Villemaire, Roger; Cherkaoui, Omar; Deca, Rudy: A logical approach to data-aware automated sequence generation (2012)
  9. Ulbrich, Mattias; Geilmann, Ulrich; El Ghazi, Aboubakr Achraf; Taghdiri, Mana: A proof assistant for Alloy specifications (2012)
  10. Li, Guodong; Palmer, Robert; DeLisi, Michael; Gopalakrishnan, Ganesh; Kirby, Robert M.: Formal specification of MPI 2.0: case study in specifying a practical concurrent programming API (2011)
  11. Sasturkar, Amit; Yang, Ping; Stoller, Scott D.; Ramakrishnan, C. R.: Policy analysis for administrative role-based access control (2011)
  12. Boronat, Artur; Meseguer, José: An algebraic semantics for MOF (2010)
  13. Hughes, Graham; Bultan, Tevfik: Automated verification of access control policies using a SAT solver (2008) ioport
  14. Winkelmann, Jessica; Taentzer, Gabriele; Ehrig, Karsten; Küster, Jochen M.: Translation of restricted OCL constraints into graph constraints for generating meta model instances by graph grammars (2008)
  15. Zeng, Liangzhao; Ngu, Anne H. H.; Benatallah, Boualem; Podorozhny, Rodion; Lei, Hui: Dynamic composition and optimization of web services (2008) ioport
  16. Frias, Marcelo F.; López Pombo, Carlos G.; Moscato, Mariano M.: Alloy Analyzer+PVS in the analysis and verification of Alloy specifications (2007)
  17. Gheyi, Rohit; Massoni, Tiago; Borba, Paulo: A static semantics for Alloy and its impact in refactorings (2007)
  18. Shlyakhter, Ilya: Generating effective symmetry-breaking predicates for search problems (2007)
  19. Taghdiri, Mana; Jackson, Daniel: Inferring specifications to detect errors in code (2007) ioport
  20. Walsh, James D’arcy; Bordeleau, Francis; Selic, Bran: Domain analysis of dynamic system reconfiguration (2007) ioport

1 2 next