Publications

The following is a list of Alloy-related works written by researchers at MIT and other institutions.

MIT

• Amerson Lin, Mike Bond, and Jolyon Clulow. Modeling Partial Attacks With Alloy. Security Protocols Workshop (SPW'07). April, 2007. To appear in Lecture Notes for Computer Science 2008/2009. (PDF)
• Mana Taghdiri, Robert Seater, and Daniel Jackson. Lightweight Extraction of Syntactic Specifications. In Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE'06). Pages 276-286. Portland, Oregon, USA. November, 2006. (pdf)
• Daniel Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press. Cambridge, MA. March 2006. ISBN 0-262-10114-9 (on MIT press) (on Amazon.com)
• Daniel Jackson. Dependable Software by Design. Scientific American. June 2006. (link)
• Felix Sheng-Ho Chang and Daniel Jackson. Symbolic Model Checking of Declarative Relational Models. International Conference on Software Engineering, May 2006, Shanghai, China. (PDF)
• Viktor Kuncak and Daniel Jackson. Relational Analysis of Algebraic Datatypes. Joint 10th European Software Engineering Conference and 13th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2005), Lisbon, Portugal, September 5-9, 2005. (PDF) (PS)
• Robert Seater. Core Extraction and Non-Example Generation: Debugging and Understanding Logical Models. MIT Masters Thesis, November 2004. (PDF)
• Mana Taghdiri. Inferring Specifications to Detect Errors in Code. 19th International Conference on Automated Software Engineering (ASE 2004). September 2004, Linz, Austria. Best paper award. (PS) (PDF)
• Jonathan Edwards, Daniel Jackson and Emina Torlak. A Type System for Object Models. Foundations of Software Engineering, Newport Beach, CA, November 2004. (PS) (PDF)
• Greg Dennis, Robert Seater, Derek Rayside, Daniel Jackson. Automating Commutativity Analysis at the Design Level. International Symposium on Software Testing and Analysis, Boston, MA, July 2004. (PS) (PDF)
• Jonathan Edwards, Daniel Jackson, Emina Torlak, Vincent Yeung. Subtypes for Constraint Decomposition. International Symposium on Software Testing and Analysis, Boston, MA, July 2004. (PS) (PDF)
• Ilya Shlyakhter, Robert Seater, Daniel Jackson, Manu Sridharan, Mana Taghdiri. Debugging Overconstrained Declarative Models Using Unsatisfiable Cores. 18th IEEE International Conference on Automated Software Engineering (ASE 2003). Montreal, Quebec, Canada. October 2003. Best Paper Award. (PS) (PDF)
• Ilya Shlyakhter, Manu Sridharan, Robert Seater, and Daniel Jackson. Exploiting Subformula Sharing in Automatic Analysis of Quantified Formulas. 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), Portofino, Italy. May 2003. (PS) (PDf)
• Mana Taghdiri and Daniel Jackson. A Lightweight Formal Analysis of a Multicast Key Management Scheme. Proc. of the 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems ( FORTE). pp 240-256, October 2003. LNCS 2767. (PS) (PDF)
• Mandana Vaziri and Daniel Jackson. Checking Heap-Manipulating Procedures with a Constraint Solver. TACAS'03, Warsaw, Poland, 2003. (PS) (PDF)
• Konstantine Arkoudas, Sarfraz Khurshid, Darko Marinov, Martin Rinard. Integrating Model Checking and Theorem Proving for Relational Reasoning. 7th International Seminar on Relational Methods in Computer Science (RelMiCS 2003). (PDF remote copy)
• Ilya Shlyakhter, Manu Sridharan, and Daniel Jackson. Analyzing Distributed Algorithms with First Order Logic. Unpublished manuscript, January 2002. (PDF) (PS)
• Mana Taghdiri. Lightweight Modelling and Automatic Analysis of Multicast Key Management Schemes. MIT Masters Thesis, December 2002. (PS) (PDF) (Summary)
• Tina Nolte. Exploring Filesystem Synchronization with Lightweight Modeling and Analysis. MIT Masters thesis, August 2002. (PS) (PDF)
• Darko Marinov and Sarfraz Khurshid. VAlloy: Virtual Functions Meet a Relational Language. 11th International Symposium of Formal Methods Europe (FME 2002), Copenhagen, Denmark. July 2002. (PS) (PDF)
• John Zao, Hoetech Wee, Jonathan Chu, and Daniel Jackson. RBAC Schema Verification Using Lightweight Formal Model and Constraint Analysis. MIT, 2002. (PDF)
• Sarfraz Khurshid and Darko Marinov. Aaree: A Recipe for Analyzing Object-Oriented Models. (in preparation), December 2001. (PS) (PDF)
• Daniel Jackson, Ilya Shlyakhter and Manu Sridharan. A Micromodularity Mechanism. Proceedings of the ACM SIGSOFT Conference on the Foundations of Software Engineering / European Software Engineering Conference (FSE / ESEC '01), September 2001. (PS) (PDF)
• Allison Waingold. Automated Extraction of Abstract Object Models. MIT Masters Thesis, May 2001. (PS) (PDF)
• Daniel Jackson and Allison Waingold. Lightweight Extraction of Object Models from Bytecode. IEEE Transactions on Software Engineering, February 2001. (PS) (PDF)
• Daniel Jackson. Automating First-Order Relational Logic. Proc. ACM SIGSOFT Conf. Foundations of Software Engineering, November 2000. (PS) (PDF)
• Sarfraz Khurshid and Daniel Jackson. Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint Analyzer. 15th IEEE International Conference on Automated Software Engineering (ASE 2000), September 2000. (PS) (PDF)
• Daniel Jackson and Mandana Vaziri. Finding Bugs with a Constraint Solver. ISSTA'00, Portland, OR, 2000. (PS) (PDF)

Other Institutions

• Ian Warren, Jing Sun, Sanjev Krishnamohan and Thiranjith Weerasinghe. An Automated Formal Approach to Managing Dynamic Reconfiguration. 21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), Tokyo, Japan, September 18-22, 2006. (PDF)
• Xiaoming Li, Daryl Shannon, Jabari Walker, Sarfraz Khurshid, and Darko Marinov. Analyzing the Uses of a Software Modeling Tool. Proc. Sixth Workshop on Language Descriptions, Tools and Applications (LDTA'06). April 2006. Vienna, Austria. (PDF)
• Fadi Zaraket, Adnan Aziz, and Sarfraz Khurshid}, Sequential Encoding for Relational Analysis. 2006. (In preparation.) (PDF)
• Petr C. Smolik. NAMBO Metamodeling Environment. Doctoral Thesis, Brno University of Technology. 2006. (PDF remote)
• Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press.
• Wael Hassan and Luigi Logrippo. Governance Policies for Privacy Access Control and their Interactions. Feature Interactions in Telecommunications and Software Systems VIII. IOS Press, June 2005. ISBN 1-58603-524-X. (PDF remote) (PDF local)
• Behzad Bordbar and Kyriakos Anastasakis. UML2ALLOY: A tool for light-weight modelling of discrete event systems. To appear in the proceeding of IADIS Applied Computing 2005, Algarve, Portugal, 2005. (html)
• Rohit Gheyi, Tiago Massoni, and Paulo Borba. Basic Laws of Object Modeling. Specification and Verification of Component-Based Systems (SAVCBS), a workshop affilitated with FSE. (PDF)
• Lee Momtahan. Towards a Small Model Theorem for Data Independent Systems in Alloy. To appear in proceedings of AVOCS04, Elsevier ENTCS. August 2004. (PS remote) (PS local)
• Rohit Gheyi. Basic Laws of Object Modeling. Master's thesis, Informatics Center, Federal Universisty of Pernambuco, Recife, Brazil. February 2004.
• Rohit Gheyi, Tiago Massoni, and Paulo Borba. Basic laws of object modeling. Third Specification and Verification of Component-Based Systems (SAVCBS), affiliated with ACM SIGSOFT 2004/FSE-12, pages 18-25, Newport Beach, United States. (PDF)
• Sanjai Narain, Telcordia Technologies, Inc. (narain@research.telcordia.com). Network Configuration Management via Model Finding. ACM Workshop On Self-Managed Systems, October 31-November 1, 2004, Newport Beach, CA. Proceedings of USENIX Large Installation System Administration (LISA) Conference, San Diego, December 4-9, 2005. (PDF) (PDF remote) (TXT abstract)
• Michael Huth. Mathematics for the Exploration of Requirements. (DOC)
• Frias M., Lopez Pombo C. and Aguirre N. An Equational Calculus for Alloy, to appear in Proceedings of ICFEM04, International Conference on Formal Engineering Methods. Seattle, USA, LNCS, Springer, 2004. (PDF) (PS)
• Maria Augusta Vieira Nelson. A Problem-Oriented Approach to Description Analysis of Geographic Requirements Waterloo PhD thesis. (PDF)
• Jin Song Dong, Jing Sun and Hai Wang. Checking and Reasoning about Semantic Web through Alloy. 12th International Symposium on Formal Methods Europe (FM'03). LNCS, pages 796-813, Springer-Verlag, Pisa, Italy, Sep 2003. (PDF)
• Christie Bolton. Using Alloy to Automatically Verify the Soundness of the Simulation Rules for Reasoning about State-Based and Event-Based Models. Oxford University Computing Laboratory, April 2003. (PS) (ALS)
• Chris Wallace. Using Alloy in Process Modelling. Process Modelling Workshop, University of the West of England, Bristol. January 2003. (PDF)
• Michael Huth and Shekhar Pradhan. An Ontology for Consistent Partial Model Checking. Submitted for publication. January 2003. (PS)
• Rohit Gheyi and Paulo Borba. Basic laws of object modeling. Refactoring Alloy Specifications. Sixth Workshop on Formal Methods, Campina Grande, Brazil 2003.
• Jin Song Dong, Jing Sun, and Hai Wang. Checking and Reasoning about Semantic Web through Alloy. National University of Singapore, September 2002. (PDF) (Summary)
• Andreas Schaad and Jonathan Moffett. A Framework for Organisational Control Principles. 18th Annual Computer Security Applications Conference, December 2002. (PDF)
• Andreas Schaad and Jonathan Moffett. A Lightweight Approach to Specification and Analysis of Role-based Access Control Extensions. 7th ACM Symposium on Access Control Models and Technologies (SACMAT 2002), June 2002. (PDF)
• Andreas Schaad and Jonathan Moffett. Delegation of Obligations. 3rd International Workshop on Policies for Distributed Systems and Networks (POLICY 2002), June 2002. (PDF)
• Andreas Schaad A Framework for Organisational Control Principles. PhD Thesis, Department of Computer Science, University of York, 2003 (PDF)
• Andrey Naumenko. Triune Continuum Paradigm: a paradigm for General System Modeling and its applications for UML and RM-ODP. PhD Thesis number 2581, Swiss Federal Institute of Technology - Lausanne (EPFL), June 2002. (PDF) (Summary)
• Nicodemos Damianou. A Policy Framework for Management of Distributed Systems. University of London Ph.D. Thesis, February 2002. (PDF) (Summary)
• Andrey Naumenko and Alain Wegmann. RM-ODP part 2: Foundations in Alloy. EPFL-DSC technical report No. DSC/2001/041, August 2001. (PDF) (Summary)
• Andrey Naumenko and Alain Wegmann. A Formal Foundation of the RM-ODP Conceptual Framework EPFL-DSC technical report No. DSC/2001/040, July 2001. (PDF) (Summary)
• Andrey Naumenko, Alain Wegmann, Guy Genilloud, William Frank. Proposal for a formal foundation of RM-ODP concepts, Proceedings of ICEIS 2001, Workshop On Open Distributed Processing - WOODPECKER`2001, Setubal, Portugal, July 2001, pp. 81-97. (PDF)