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.

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

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

1 2 next

  1. Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
  2. Cristiá, Maximiliano; Rossi, Gianfranco: A set solver for finite set relation algebra (2018)
  3. Joosten, Sebastiaan J. C.: Finding models through graph saturation (2018)
  4. Porncharoenwase, Sorawee; Nelson, Tim; Krishnamurthi, Shriram: CompoSAT: specification-guided coverage for model finding (2018)
  5. Wickerson, John; Batty, Mark; Sorensen, Tyler; Constantinides, George A.: Automatically comparing memory consistency models (2017)
  6. Cristiá, Maximiliano; Rossi, Gianfranco; Frydman, Claudia: Adding partial functions to constraint logic programming with sets (2015)
  7. Schneider, Steve; Treharne, Helen; Wehrheim, Heike: The behavioural semantics of Event-B refinement (2014)
  8. Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
  9. Giese, Holger; Lambers, Leen: Towards automatic verification of behavior preservation for model transformation via invariant checking (2012)
  10. Hallé, Sylvain; Villemaire, Roger; Cherkaoui, Omar; Deca, Rudy: A logical approach to data-aware automated sequence generation (2012)
  11. Ulbrich, Mattias; Geilmann, Ulrich; El Ghazi, Aboubakr Achraf; Taghdiri, Mana: A proof assistant for Alloy specifications (2012)
  12. 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)
  13. Sasturkar, Amit; Yang, Ping; Stoller, Scott D.; Ramakrishnan, C. R.: Policy analysis for administrative role-based access control (2011)
  14. Boronat, Artur; Meseguer, José: An algebraic semantics for MOF (2010)
  15. Hughes, Graham; Bultan, Tevfik: Automated verification of access control policies using a SAT solver (2008) ioport
  16. 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)
  17. Zeng, Liangzhao; Ngu, Anne H. H.; Benatallah, Boualem; Podorozhny, Rodion; Lei, Hui: Dynamic composition and optimization of web services (2008) ioport
  18. Frias, Marcelo F.; López Pombo, Carlos G.; Moscato, Mariano M.: Alloy Analyzer+PVS in the analysis and verification of Alloy specifications (2007)
  19. Gheyi, Rohit; Massoni, Tiago; Borba, Paulo: A static semantics for Alloy and its impact in refactorings (2007)
  20. Shlyakhter, Ilya: Generating effective symmetry-breaking predicates for search problems (2007)

1 2 next