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 24 articles , 1 standard article )

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

1 2 next

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

1 2 next