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