|
|
|
SearchNavigationUser login |
MIT-SDGAlloy4 Tutorial and FAQWhen Published: Jul 9 2008 A step-by-step walkthrough and tutorial of Alloy4 is Alloy Analyzer 4.1.10latestversion: 03/19/2009 Version 4 of the Alloy Analyzer is a complete rewrite, offering improvements in robustness, performance and usability. Kodkod: constraint solver for relational logiclatestversion: 03/17/2009 Kodkod is an efficient SAT-based analysis engine for first order logic with relations, transitive closure, and partial instances. Alloy Analyzer 3.0latestversion: 05/21/2006 The Alloy Analyzer is a tool developed by the Software Design Group Alloy Analyzer 2.0latestversion: 07/12/2002 The Alloy Analyzer is a tool developed by the Software Design Group Formal Modeling and Analysis of a Flash Filesystem in AlloyPublication Venue: 1st International Conference on ASM, B, and Z (ABZ 2008) When Published: Sep 15 2008 Finding Minimal Unsatisfiable Cores of Declarative SpecificationsPublication Venue: 15th International Symposium on Formal Methods (FM'08), Turku, Finland. When Published: May 26 2008 Boolean Compilation of Relational SpecificationsPublication Venue: Technical Report MIT-LCS-735 When Published: Dec 1 1997 Isomorph-free Model Enumeration: A New Method for Checking Relational SpecificationsPublication Venue: ACM Transactions on Programming Languages and Systems, Vol. 20, No. 2, March 1998, pp. 302-343 When Published: Mar 1 1998 A Comparison of Object Modelling Notations: Alloy, UML and ZPublication Venue: Unpublished Manuscript When Published: Aug 1 1999 Some Shortcomings of OCL, the Object Constraint Language of UMLPublication Venue: Response to Object Management Group's Request for Information on UML 2.0 When Published: Dec 1 1999 Enforcing Design Constraints with Object LogicPublication Venue: Static Anaysis Symposium 2000, Santa Barbara, CA, June/July 2000. Springer Verlag, LNCS 1824 When Published: Jun 29 2000 Finding Bugs with a Constraint SolverPublication Venue: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA'00) When Published: Aug 21 2000 Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint AnalyzerPublication Venue: 15th International Conference on Automated Software Engineering (ASE), Grenoble, France When Published: Sep 11 2000 Automating First-Order Relational LogicPublication Venue: ACM SIGSOFT Foundations of Software Engineering (FSE 2000) When Published: Nov 1 2000 Lightweight Extraction of Object Models from BytecodePublication Venue: IEEE Transactions on Software Engineering When Published: Feb 1 2001 Testing an Intentional Naming Scheme Using Genetic AlgorithmsPublication Venue: 7th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2001) When Published: Apr 2 2001 Automated Extraction of Abstract Object ModelsPublication Venue: MIT Masters Thesis When Published: May 1 2001 Checking Java Implementation of a Naming Architecture Using TestEraPublication Venue: CAV Workshop on Software Model Checking. Electronic Notes in Theoretical Computer Science (ENTCS 55(3)) When Published: Jul 1 2001 A Micromodularity MechanismPublication Venue: ACM SIGSOFT Conference on the Foundations of Software Engineering / European Software Engineering Conference (FSE / ESEC '01) When Published: Sep 10 2001 Lightweight Analysis of Object InteractionsPublication Venue: 4th International Symposium on Theoretical Aspects of Computer Software, Sendai, Japan When Published: Oct 1 2001 TestEra: A Novel Framework for Automated Testing of Java ProgramsPublication Venue: 16th International Conference on Automated Software Engineering (ASE), San Diego, USA When Published: Nov 26 2001 Correcting a Naming Architecture Using Lightweight Constraint AnalysisPublication Venue: Tech Report, MIT Lab for Computer Science, December 2001 When Published: Dec 1 2001 . Alloy: A Lightweight Object Modelling NotationPublication Venue: ACM Transactions on Software Engineering and Methodology (TOSEM'02), volume 11, issue 2, pages 256-290 When Published: Apr 1 2002 VAlloy: Virtual Functions Meet a Relational LanguagePublication Venue: 11th International Symposium of Formal Methods Europe (FME), Copenhagen, Denmark When Published: Jul 22 2002 Exploring Filesystem Synchronization with Lightweight Modeling and AnalysisPublication Venue: MIT Masters thesis When Published: Aug 1 2002 Module Dependencies in Software DesignPublication Venue: Post-workshop Proceedings of the 2002 Monterey Workshop: Radical Innovations of Software and Systems Engineering in the Future. Venice, Italy When Published: Oct 7 2002 An Analyzable Annotation LanguagePublication Venue: 17th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'02) When Published: Nov 4 2002 Lightweight Modelling and Automatic Analysis of Multicast Key Management SchemesPublication Venue: MIT Masters Thesis When Published: Dec 1 2002 TestEra: A Novel Framework for Automated Testing of Java ProgramsPublication Venue: Invited submission to Automated Software Engineering Journal, December 2002 (Journal version of the ASE 2001 paper) When Published: Dec 1 2002 TSAFE: Building a Trusted Computing Base for Air Traffic Control SoftwarePublication Venue: MIT Masters Thesis When Published: Jan 1 2003 Generating Structurally Complex Tests from Declarative ConstraintsPublication Venue: MIT PhD Thesis When Published: Feb 1 2003 Debugging Overconstrained Declarative Models Using Unsatisfiable CoresPublication Venue: 18th IEEE International Conference on Automated Software Engineering (ASE 2003) (Best Paper Award) When Published: Oct 6 2003 Lightweight Formal Analysis of a Multicast Key Management SchemePublication Venue: Proceedings of the 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2003) When Published: Sep 29 2003 A Case for Efficient Solution EnumerationPublication Venue: 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003) When Published: May 5 2003 Exploiting Subformula Sharing in Automatic Analysis of Quantified FormulasPublication Venue: 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003) When Published: May 5 2003 Checking Heap-Manipulating Procedures with a Constraint SolverPublication Venue: 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2003) When Published: Apr 7 2003 Finding Bugs in Software with a Constraint SolverPublication Venue: MIT PhD Thesis When Published: Feb 1 2004 Automating Commutativity Analysis at the Design LevelPublication Venue: International Symposium on Software Testing and Analysis (ISSTA), Boston, MA When Published: Jul 1 2004 Subtypes for Constraint DecompositionPublication Venue: International Symposium on Software Testing and Analysis (ISSTA), Boston, MA When Published: Jul 1 2004 Inferring Specifications to Detect Errors in CodePublication Venue: 19th International Conference on Automated Software Engineering (ASE), Linz, Austria (Best paper award) When Published: Sep 20 2004 TestEra: Specification-based Testing of Java Programs Using SATPublication Venue: Automated Software Engineering Journal, Volume 11, Number 4, October 2004. (Journal version of ASE 2001 paper) When Published: Oct 1 2004 Core Extraction and Non-Example Generation: Debugging and Understanding Logical ModelsPublication Venue: MIT Masters Thesis When Published: Nov 1 2004 A Type System for Object ModelsPublication Venue: Foundations of Software Engineering (FSE), Newport Beach, CA When Published: Nov 1 2004 Declarative Symbolic Pure Logic Model CheckingPublication Venue: MIT PhD Thesis When Published: Feb 1 2005 Relational Analysis of Algebraic DatatypesPublication Venue: Joint 10th European Software Engineering Conference and 13th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2005), Lisbon, Portugal, 2005 When Published: Sep 5 2005 Declarative Configuration Applied to Course SchedulingPublication Venue: MIT MEng Thesis When Published: May 1 2006 Symbolic Model Checking of Declarative Relational ModelsPublication Venue: 28th International Conference on Software Engineering (ICSE), Shanghai, China When Published: May 20 2006 Dependable Software by DesignPublication Venue: Scientific American When Published: Jun 1 2006 Scientific American. June 2006. The link to the article is here 
|
The development of this site is supported by the National Science Foundation under Computing Research Infrastructure Grant No. 0707612.
Theme originally designed by Chris Herberte