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.


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

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

1 2 next

  1. Schneider, Steve; Treharne, Helen; Wehrheim, Heike: The behavioural semantics of Event-B refinement (2014)
  2. Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
  3. Giese, Holger; Lambers, Leen: Towards automatic verification of behavior preservation for model transformation via invariant checking (2012)
  4. Ulbrich, Mattias; Geilmann, Ulrich; El Ghazi, Aboubakr Achraf; Taghdiri, Mana: A proof assistant for alloy specifications (2012)
  5. 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)
  6. Sasturkar, Amit; Yang, Ping; Stoller, Scott D.; Ramakrishnan, C.R.: Policy analysis for administrative role-based access control (2011)
  7. Boronat, Artur; Meseguer, José: An algebraic semantics for MOF (2010)
  8. Hughes, Graham; Bultan, Tevfik: Automated verification of access control policies using a SAT solver (2008)
  9. Zeng, Liangzhao; Ngu, Anne H.H.; Benatallah, Boualem; Podorozhny, Rodion; Lei, Hui: Dynamic composition and optimization of web services (2008)
  10. Frias, Marcelo F.; López Pombo, Carlos G.; Moscato, Mariano M.: Alloy Analyzer+PVS in the analysis and verification of Alloy specifications (2007)
  11. Gheyi, Rohit; Massoni, Tiago; Borba, Paulo: A static semantics for alloy and its impact in refactorings. (2007)
  12. Shlyakhter, Ilya: Generating effective symmetry-breaking predicates for search problems (2007)
  13. Taghdiri, Mana; Jackson, Daniel: Inferring specifications to detect errors in code (2007)
  14. Walsh, James D’arcy; Bordeleau, Francis; Selic, Bran: Domain analysis of dynamic system reconfiguration (2007)
  15. Freitas, Leo; Woodcock, Jim; Cavalcanti, Ana: State-rich model checking (2006)
  16. Freitas, Leo; Woodcock, Jim; Cavalcanti, Ana: State-rich model checking (2006)
  17. Li, Xiaoming; Shannon, Daryl; Walker, Jabari; Khurshid, Sarfraz; Marinov, Darko: Analyzing the uses of a software modeling tool. (2006)
  18. Gheyi, Rohit; Massoni, Tiago; Borba, Paulo: An abstract equivalence notion for object models. (2005)
  19. Gogolla, Martin; Bohling, Jørn; Richters, Mark: Validating UML and OCL models in use by automatic snapshot generation (2005)
  20. Gogolla, Martin; Bohling, Jørn; Richters, Mark: Validating UML and OCL models in use by automatic snapshot generation (2005)

1 2 next