Alcoa swMATH ID: 9481 Software Authors: Jackson, D.; Schechter, I.; Shlyakhter, I. Description: 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. Homepage: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=870482 Related Software: Alloy; SPIN; Chaff; Z; TestEra; NuSMV; JML; OEIS; Circus; ProBE; MOCHA; FDR2; Z/EVES; Casper; ProofPower; CZT; JACK; SPARK; ArgoUML; Java PathFinder Cited in: 20 Publications all top 5 Cited by 49 Authors 3 Huth, Michael R. A. 2 Jagadeesan, Radha 2 Khurshid, Sarfraz 2 Marinov, Darko 2 Rinard, Martin C. 2 Schmidt, David A. 2 Shlyakhter, Ilya 1 Al-Yahya, Tasniem Nasser 1 Alencar, Paulo S. C. 1 Arkoudas, Konstantine 1 Beckert, Bernhard 1 Borba, Paulo 1 Bugrara, Suhabe 1 Cherkaoui, Omar 1 Cowan, Donald D. 1 Deca, Rudy 1 DeLisi, Michael 1 El-bachir Menai, Mohamed 1 Fokkink, Willem Jan 1 Gheyi, Rohit 1 Gopalakrishnan, Ganesh Lalitha 1 Guelev, Dimitar P. 1 HallĂ©, Sylvain 1 Heule, Marijn J. H. 1 Ioustinova, Natalia 1 Jackson, Daniel 1 Joosten, Sebastiaan J. C. 1 Kesseler, Ernst 1 Kirby, Robert M. II 1 Koch, Manuel 1 Li, Guodong 1 Massoni, Tiago 1 Myreen, Magnus O. 1 Nelson, Torsten 1 Parisi-Presicce, Francesco 1 Pradhan, Shekhar 1 Ramakrishnan, C. R. 1 Ryan, Mark Dermot 1 Sasturkar, Amit 1 Stoller, Scott D. 1 Tan, Yong Kiam 1 Trentelman, Kerry 1 Usenko, Yaroslav S. 1 van de Pol, Jan Cornelis 1 Villemaire, Roger 1 Yang, Ping 1 Yushtein, Yuri A. 1 Zhang, Lintao 1 Zhang, Nan all top 5 Cited in 6 Serials 1 Discrete Applied Mathematics 1 Theoretical Computer Science 1 Science of Computer Programming 1 Journal of Computer Science and Technology 1 MSCS. Mathematical Structures in Computer Science 1 Journal of Logical and Algebraic Methods in Programming Cited in 2 Fields 20 Computer science (68-XX) 4 Mathematical logic and foundations (03-XX) Citations by Year