Alcoa: the Alloy constraint analyzer. Alcoa is a tool for analyzing object models. It has a range of uses. At one end, it can act as a support tool for object model diagrams, checking for consistency of multiplicities and generating sample snapshots. At the other end, it embodies a lightweight formal method in which subtle properties of behaviour can be investigated. Alcoa’s input language, Alloy, is a new notation based on Z. Its development was motivated by the need for a notation that is more closely tailored to object models (in the style of UML), and more amenable to automatic analysis. Like Z, Alloy supports the description of systems whose state involves complex relational structure. State and behavioural properties are described declaratively, by conjoining constraints. This makes it possible to develop and analyze a model incrementally, with Alcoa investigating the consequences of whatever constraints are given. Alcoa works by translating constraints to boolean formulas, and then applying state-of-the-art SAT solvers. It can analyze billions of states in seconds.

References in zbMATH (referenced in 24 articles )

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

1 2 next

  1. Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
  2. Hallé, Sylvain; Villemaire, Roger; Cherkaoui, Omar; Deca, Rudy: A logical approach to data-aware automated sequence generation (2012)
  3. 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)
  4. Sasturkar, Amit; Yang, Ping; Stoller, Scott D.; Ramakrishnan, C.R.: Policy analysis for administrative role-based access control (2011)
  5. Hughes, Graham; Bultan, Tevfik: Automated verification of access control policies using a SAT solver (2008)
  6. Zeng, Liangzhao; Ngu, Anne H.H.; Benatallah, Boualem; Podorozhny, Rodion; Lei, Hui: Dynamic composition and optimization of web services (2008)
  7. Shlyakhter, Ilya: Generating effective symmetry-breaking predicates for search problems (2007)
  8. Taghdiri, Mana; Jackson, Daniel: Inferring specifications to detect errors in code (2007)
  9. Walsh, James D’arcy; Bordeleau, Francis; Selic, Bran: Domain analysis of dynamic system reconfiguration (2007)
  10. Freitas, Leo; Woodcock, Jim; Cavalcanti, Ana: State-rich model checking (2006)
  11. Freitas, Leo; Woodcock, Jim; Cavalcanti, Ana: State-rich model checking (2006)
  12. Beckert, Bernhard; Trentelman, Kerry: Second-order principles in specification languages for object-oriented programs (2005)
  13. Gogolla, Martin; Bohling, Jørn; Richters, Mark: Validating UML and OCL models in use by automatic snapshot generation (2005)
  14. Gogolla, Martin; Bohling, Jørn; Richters, Mark: Validating UML and OCL models in use by automatic snapshot generation (2005)
  15. Marinov, Darko; Khurshid, Sarfraz; Bugrara, Suhabe; Zhang, Lintao; Rinard, Martin: Optimizations for compiling declarative models into Boolean formulas (2005)
  16. Zhang, Nan; Ryan, Mark; Guelev, Dimitar P.: Evaluating access control policies through model checking (2005)
  17. Arkoudas, Konstantine; Khurshid, Sarfraz; Marinov, Darko; Rinard, Martin: Integrating model checking and theorem proving for relational reasoning (2004)
  18. Huth, Michael R.A.; Jagadeesan, Radha; Schmidt, David A.: A domain equation for refinement of partial systems (2004)
  19. Koch, Manuel; Parisi-Presicce, Francesco: Visual specifications of policies and their verification (2003)
  20. Fokkink, Wan; Ioustinova, Natalia; Kesseler, Ernst; van de Pol, Jaco; Usenko, Yaroslav S.; Yushtein, Yuri A.: Refinement and verification applied to an in-flight data acquisition unit (2002)

1 2 next