software design group

• home
• people
• projects
• publications
  • papers: 2009
  • papers: 2008
  • papers: 2007
  • papers: 2006
  • papers: 2005
  • papers: 2004
  • papers: 2003
  • papers: 2002
  • papers: 2001
  • papers: 2000
  • papers: 1999
  • theses
• wiki
• contact us

SDG Publications 1999-2011

2011 Papers

• Joseph P. Near, Aleksandar Milicevic, Eunsuk Kang and Daniel Jackson. A Lightweight Code Analysis and its Role in Evaluation of a Dependability Case. 33rd International Conference on Software Engineering (ICSE), Waikiki, Honolulu, Hawaii, May 2011 (PDF).
• Aleksandar Milicevic, Derek Rayside, Kuat Yessenov and Daniel Jackson. Unifying Execution of Imperative and Declarative Code. 33rd International Conference on Software Engineering (ICSE), Waikiki, Honolulu, Hawaii, May 2011 (PDF).

2010 Papers

• Daniel Jackson and Eunsuk Kang. Separation of Concerns for Dependable Software Design. Workshop on the Future of Software Engineering Research (FoSER), co-located with FSE, Santa Fe, 2010 (PDF).
• Eunsuk Kang and Daniel Jackson. Dependability Arguments with Trusted Bases. 18th International Conference on Requirements Engineering (RE), Sydney, 2010 (PDF).
• Eunsuk Kang and Daniel Jackson. Patterns for Dependable Systems with Trusted Bases. Pattern Languages of Programs Conference (PLOP), Reno, NV, 2010 (PDF).
• Joseph P. Near. From Relational Specifications to Logic Programs. 26th International Conference on Logic Programming, 2010 (PDF).
• Joseph P. Near and Daniel Jackson. An Imperative Extension to Alloy. 2nd Conference on ASM, Alloy, B, and Z (ABZ 2010). Orford, QC, Canada. February 2010 (PDF).

2009 Papers

• Daniel Jackson. A Direct Path To Dependable Software. Communications of the Association for Computing Machinery (CACM), April 2009, pp. 78-88 (PDF).
• Daniel Jackson. A Direct Path To Dependable Software (Fuller version of the published paper). Communications of the Association for Computing Machinery (CACM), April 2009 (PDF).
• Derek Rayside, Aleksander Milicevic, Kuat Yessenov, Greg Dennis and Daniel Jackson. Agile Specifications (Onward'09). (PDF).
• C. A. R. Hoare. Edited and introduced by Daniel Jackson. The Michael Jackson Design Technique: A study of the theory with applications. ICSE Workshop: A Tribute to Michael Jackson, Vancouver, May 2009 (PDF).
• Daniel Jackson and Eunsuk Kang. Property-part diagrams: A dependence notation for software systems. ICSE Workshop: A Tribute to Michael Jackson, Vancouver, May 2009 (PDF).
• Derek Rayside, Zev Benjamin, Rishabh Singh, Joseph P. Near, Aleksandar Milicevic and Daniel Jackson. Equality and Hashing for (almost) Free: Generating Implementations from Abstraction Functions. 31st International Conference on Software Engineering (ICSE'09). (PDF)
• Derek Rayside and H.-Christian Estler A Spreadsheet-like User Interface for Combinatorial Multi-Objective Optimization. (CASCON'09). (PDF).
• Derek Rayside, H.-Christian Estler, and Daniel Jackson. A Guided Improvement Algorithm for Exact, General Purpose, Many-Objective Combinatorial Optimization. MIT-CSAIL-TR-2009-033 (http://hdl.handle.net/1721.1/46322)
• Eunsuk Kang and Daniel Jackson. Designing and Analyzing a Flash File System with Alloy. International Journal of Software and Informatics (IJSI), 2009 (PDF).

2008 Papers

• Greg Dennis, Kuat Yessenov, Daniel Jackson. Bounded Verification of Voting Software. Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08). Toronto, Canada, October 2008. (PDF)
• Eunsuk Kang and Daniel Jackson. Formal Modeling and Analysis of a Flash Filesystem in Alloy. 1st Conference on ASM, B, and Z (ABZ 2008). London, UK. September 2008. (PDF)
• Emina Torlak, Felix Sheng-Ho Chang and Daniel Jackson. Finding Minimal Unsatisfiable Cores of Declarative Specifications. 15th International Symposium on Formal Methods (FM'08). Turku, Finland. May 2008. (PDF)

2007 Papers

• Daniel Jackson, Martyn Thomas, and Lynette I. Millett, Editors. Software for Dependable Systems: Sufficient Evidence? National Academies, Washington, DC, May 2007. (link).
• Jonathan Edwards. No Ifs, Ands, or Buts: Uncovering the Simplicity of Conditionals. 22nd annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). October 2007, Montreal, Canada. (PDF)
• Derek Rayside and Lucy Mendel. Object Ownership Profiling: A Technique for Finding and Fixing Memory Leaks. International Conference on Automated Software Engineering (ASE'07). (paper) (slides)
• Derek Rayside, Felix Chang, Greg Dennis, Robert Seater, and Daniel Jackson. Automatic Visualization of Relational Logic Models. First Workshop on the Layout of (Software) Engineering Diagrams (LED'07). (PDF)
• Emina Torlak and Daniel Jackson. Kodkod: A Relational Model Finder. Tools and Algorithms for Construction and Analysis of Systems (TACAS). Braga, Portugal. April 2007. (PDF)
• Robert Seater, Daniel Jackson, and Rohit Gheyi. Requirement Progression in Problem Frames: Deriving Specifications from Requirements. Requirements Engineering Journal (REJ'07). 2007. (PDF) (PS)

2006 Papers

• 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)
• Daniel Jackson & Michael Jackson. Separating Concerns in Requirements Analysis: An Example. M. Butler, C. Jones, A. Romanovsky, E. Troubitsyna (editors). Chapter of Rigorous development of complex fault tolerant systems. Springer-Verlag. (PDF)
• Emina Torlak and Greg Dennis. Kodkod for Alloy Users. First Alloy Workshop, co-located with the 14th ACM/SIGSOFT Symposium on Foundations of Software Engineering (FSE'06). Portland, Oregon, November 2006. (PDF)
• Robert Seater and Daniel Jackson. Requirement Progression in Problem Frames Applied to a Proton Therapy System. 14th IEEE International Requirements Engineering Conference (RE'06). September 2006. Minneapolis, MN. (PDF) (PS)
• Greg Dennis, Felix Sheng-Ho Chang, and Daniel Jackson. Modular Verification of Code with SAT. International Symposium on Software Testing and Analysis, Portland, ME, July 2006. (PS) (PDF)
• Felix Sheng-Ho Chang and Daniel Jackson. Symbolic Model Checking of Declarative Relational Models. International Conference on Software Engineering, May 2006, Shanghai, China. (PDF)
• Robert Seater and Daniel Jackson. Problem Frame Transformations: Deriving Specifications from Requirements. Second International Workshop on Applications and Advances in Problem Frames (IWAAPF'06), associated with the International Conference on Software Engineering (ICSE'06). Shanghai, China. May, 2006. (PDF) (PS)
• Derek Rayside, Lucy Mendel, and Daniel Jackson. A Dynamic Analysis for Revealing Object Ownership and Sharing. Fourth International Workshop on Dynamic Analysis (WODA 2006), associated with the International Conference on Software Engineering (ICSE'06). Shanghai, China. May, 2006. Best paper award (as voted by workshop participants). (PDF)

2005 Papers

• 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)
• Jonathan Edwards. Subtext: Uncovering the Simplicity of Programming. 20th annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). October 2005, San Diego, California. (PDF)
• Neeraj Sangal, Ev Jordan, Vineet Sinha, and Daniel Jackson. Using Dependency Models to Manage Complex Software Architecture. 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems (OOPSLA 2005). (PDF).
• Derek Rayside, Lucy Mendel, Robert Seater, and Daniel Jackson. An Analysis and Visualization for Revealing Object Sharing. Eclipse Technology Exchange (ETX) Workshop at OOPSLA'05. (PDF)
• Andrew Rae, Daniel Jackson, Prasad Ramanan, Jay Flanz, and Didier Leyman. Critical feature analysis of a radiotherapy machine. Reliability Engineering & System Safety Volume 89, Issue 1, Elsevier Science, July 2005, Pages 48-56. (link)

2004 Papers

• Mana Taghdiri. Inferring Specifications to Detect Errors in Code. 19th International Conference on Automated Software Engineering (ASE). 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. Journal of Automated Software Engineering. 2004.
• Jonathan Edwards. Example Centric Programming. Companion to the 19th annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) Onward!. Vancouver, BC, Canada 2004. (PS) (PDF)
• S. Khurshid and D. Marinov. TestEra: Specification-based Testing of Java Programs Using SAT. Automated Software Engineering Journal, Volume 11, Number 4. October 2004. (Journal version of ASE'2001 paper.) (PDF)

2003 Papers

• 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)
• K. Arkoudas, S. Khurshid, D. Marinov and M. Rinard. Integrating model checking and theorem proving for relational reasoning. 7th International Seminar on Relational Methods in Computer Science (RelMiCS 7), Malente, Germany. May 2003. (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). Montreal, Quebec, Canada. October 2003. Best Paper Award. (PS) (PDF)
• Andrew Rae, Prasad Ramanan, Daniel Jackson, and Jay Flanz. Critical feature analysis of a radiotherapy machine. International Conference of Computer Safety, Reliability and Security (SAFECOMP), Edinburgh, September 2003. Jounral Version: (PS) (PDF)
• Sarfraz Khurshid, Darko Marinov, Ilya Shlyakhter and Daniel Jackson. A Case for Efficient Solution Enumeration. 6th International Conference on Theory and Applications of Satisfiability Testing (SAT), Portofino, Italy. May 2003. (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), Portofino, Italy. May 2003. (poster) (PS) (PDF)
• Sarfraz Khurshid, Corina Pasareanu, Willem Visser. Generalized Symbolic Execution for Model Checking and Testing. 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Warsaw, Poland. April 2003. (PS) (PDF)
• Mandana Vaziri, Daniel Jackson. Checking Heap-Manipulating Procedures with a Constraint Solver. International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Warsaw, Poland, 2003. (PS) (PDF)

2002 Papers

• Daniel Jackson. Alloy: A Lightweight Object Modelling Notation. ACM Transactions on Software Engineering and Methodology (TOSEM'02). Volume 11, Issue 2 (April 2002), pp. 256-290. (PDF)
• Sarfraz Khurshid and Darko Marinov. TestEra: A Novel Framework for Automated Testing of Java Programs. Invited submission to Automated Software Engineering Journal, December 2002. (PS) (PDF)
  [A previous version appeared at the 16th IEEE International Conference on Automated Software Engineering (ASE) and was nominated for the best paper award by the program committee. (PS) (PDF)]
• Sarfraz Khurshid, Darko Marinov and Daniel Jackson. An Analyzable Annotation Language. 17th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Seattle, WA. November 2002. (PS) (PDF)
• Daniel Jackson. Module Dependencies in Software Design. Post-workshop Proceedings of the 2002 Monterey Workshop: Radical Innovations of Software and Systems Engineering in the Future. Venice, Italy October 7-11, 2002. Springer Verlag, 2003. (PS) (PDF)
• Alexandr Andoni, Dumitru Daniliuc, Sarfraz Khurshid, and Darko Marinov. Evaluating the "Small Scope Hypothesis". (Submitted for publication.) September 2002. (PS) (PDF)
• Chandrasekhar Boyapati, Sarfraz Khurshid and Darko Marinov. Korat: Automated Testing Based on Java Predicates. ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), Rome, Italy. July 2002.
  [This paper won an ACM SIGSOFT Distinguished Paper Award] (PS) (PDF)
• Darko Marinov and Sarfraz Khurshid. VAlloy: Virtual Functions Meet a Relational Language. 11th International Symposium of Formal Methods Europe (FME), Copenhagen, Denmark. July 2002. (PS) (PDF)
• Patrice Godefroid, Sarfraz Khurshid, Exploring Very Large State Spaces Using Genetic Algorithms. 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2002. (PS) (PDF)
  Pre-selected for a special issues of the Software Tools and Technology Transfer Journal: (PS) (PDF)
• Ilya Shlyakhter, Manu Sridharan and Daniel Jackson. Analyzing Distributed Algorithms with First Order Logic. Unpublished manuscript, January 2002. (PDF) (PS)

2001 Papers

• Sarfraz Khurshid. Correcting a Naming Architecture Using Lightweight Constraint Analysis. RQE Report, MIT Lab for Computer Science, December 2001. (PS) (PDF)
• Sarfraz Khurshid, Darko Marinov, Aaree: A Recipe for Analyzing Object-Oriented Models. (in preparation), December 2001. (PS) (PDF)
• Darko Marinov, Sarfraz Khurshid, TestEra: A Novel Framework for Automated Testing of Java Programs. 16th IEEE Conference on Automated Software Engineering (ASE). (This paper was nominated for the best paper award by the program committee.), November 2001. (PS) (PDF)
• Daniel Jackson, Ilya Shlyakhter, Manu Sridharan, A Micromodularity Mechanism. Proceedings of the ACM SIGSOFT Conference on the Foundations of Software Engineering / European Software Engineering Conference (FSE/ESEC), September 2001. (PS) (PDF)
• Daniel Jackson and Alan Fekete. Lightweight Analysis of Object Interactions. Fourth International Symposium on Theoretical Aspects of Computer Software, Sendai, Japan, October 2001. (PDF)
• Sarfraz Khurshid, Darko Marinov, Checking Java Implementation of a Naming Architecture Using TestEra. CAV Workshop on Software Model Checking. Electronic Notes in Theoretical Computer Science (ENTCS 55(3)), July 2001. (PS) (PDF)
• Sarfraz Khurshid, Darko Marinov, Using TestEra to Check the Intentional Naming System of Oxygen (Extended Abstract). MIT Student Oxygen Workshop, July 2001. (PS) (PDF)
• Sarfraz Khurshid, Testing an Intentional Naming Scheme Using Genetic Algorithms. 7th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science (LNCS), vol. 2031, eds. T. Margaria and W. Yi, April 2001. (PS) (PDF)
• Daniel Jackson, Allison Waingold, Lightweight Extraction of Object Models from Bytecode. IEEE Transactions on Software Engineering, February 2001. (PS) (PDF)

2000 Papers

• Daniel Jackson. Object Models as Heap Invariants. A chapter in: Essays on Programming Methodology, edited by Carroll Morgan and Annabelle McIver. Springer Verlag, 2000. (PDF)
• Daniel Jackson, Ian Schechter, Ilya Shlakhter. Alcoa: the Alloy Constraint Analyzer. (PS) (PDF)
• Daniel Jackson. Automating First-Order Relational Logic. Proc. ACM SIGSOFT Conf. Foundations of Software Engineering, November 2000. (PS) (PDF)
• Daniel Jackson and Kevin Sullivan. COM Revisited: Tool Assisted Modelling and Analysis of Software Structures. Proceedings of the ACM SIGSOFT Conference on the Foundations of Software Engineering (FSE'00). San Diego, November 2000. (PDF)
• Sarfraz Khurshid, Daniel Jackson, Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint Analyzer. 15th IEEE International Conference on Automated Software Engineering (ASE), September 2000. (PS) (PDF)
• Daniel Jackson, Mandana Vaziri. Finding Bugs with a Constraint Solver. International Symposium on Software Testing and Analysis (ISSTA'00), Portland, OR, 2000. (PS) (PDF)
• Daniel Jackson. Enforcing Design Constraints with Object Logic. Static Anaysis Symposium 2000, Santa Barbara, CA, June/July 2000. Springer Verlag, LNCS 1824. (PDF)
• Daniel Jackson and Martin Rinard. The Future of Software Analysis. A chapter in 'The Future of Software Engineering', editor Anthony Finkelstein, ACM Press, June 2000. (PDF)

1999 Papers & Earlier

• Mandana Vaziri and Daniel Jackson. Some Shortcomings of OCL, the Object Constraint Language of UML. Response to Object Management Group's Request for Information on UML 2.0. December 1999. (PDF)
• Daniel Jackson. A Comparison of Object Modelling Notations: Alloy, UML and Z. Unpublished manuscript. August 1999. (PDF)
• Daniel Jackson, Yuchung Ng, and Jeannette M. Wing. A Nitpick Analysis of Mobile IPv6. Formal Aspects of Computing, Issue 11, Number 6, 1999, pp. 591--615. (PDF)
• Daniel Jackson, Somesh Jha and Craig A. Damon. Isomorph-free Model Enumeration: A New Method for Checking Relational Specifications. ACM Trans. Programming Languages and Systems, Vol. 20, No. 2, March 1998, pp. 302-343. (PDF)
• Daniel Jackson. Boolean Compilation of Relational Specifications. Technical Report MIT-LCS-735, December 1997. (PDF)
• Daniel Jackson and Michael Jackson. Problem Decomposition for Reuse. Software Engineering Journal, Vol. 11, No. 1, January 1996. (PDF)
• Daniel Jackson and Jeannette Wing. Lightweight Formal Methods. IEEE Computer, April 1996. (HTML)
• Daniel Jackson. Structuring Z Specifications With Views. ACM Trans. on Software Engineering and Methodology, Vol. 4, No. 4, October 1995. (PDF)
• Daniel Jackson. Abstract Model Checking of Infinite Specifications. Proc. Formal Methods Europe, Barcelona, October 1994. (PDF)
• Daniel Jackson and Eugene J. Rollins. A New Model of Program Dependences for Reverse Engineering. Proc. SIGSOFT Conf. on Foundations of Software Engineering, New Orleans, December 1994. (PDF)
• Daniel Jackson. Automatic Analysis of Architectural Style. Unpublished manuscript. (PDF)
• Daniel Jackson and Somesh Jha. Faster Checking of Software Specifications By Eliminating Isomorphs. (PDF)
• Robert O'Callahan and Daniel Jackson. Lackwit: Large-Scale Analysis of C Programs Using Polymorphic Type Inference. (PDF)

Theses

• Joseph P. Near. An Imperative Extension to Alloy and a Compiler for its Execution. MIT Masters Thesis. May 2010. (PDF)
• Eunsuk Kang. A Framework for Dependability Analysis of Software Systems with Trusted Bases. MIT Masters Thesis. Jan 2010. (PDF)
• Greg Dennis. A Relational Framework for Bounded Program Verification. MIT PhD Thesis. July 2009. (PDF)
• Kuat Yessenov. A Light-weight Specification Language for Bounded Program Verification. MIT MEng Thesis. May 2009. (PDF)
• Zev Benjamin. Runtime Verification of Object Lifetime Specifications. MIT MEng Thesis. May 2009. (PDF)
• Carlos Pacheco. Directed Random Testing. MIT PhD Thesis. February 2009. (PDF)
• Felix Chang. Generation of Policy-rich Websites from Declarative Models. MIT PhD Thesis. February 2009. (PDF)
• Robert Seater. Building Dependability Arguments for Software Intensive Systems . MIT PhD Thesis. January 2009. (PDF)
• Emina Torlak. A Constraint Solver for Software Engineering: Finding Models and Cores of Large Relational Specifications. MIT PhD Thesis. December 2008. (PDF)
• Mana Taghdiri. Automating Modular Program Verification by Refining Specifications. MIT PhD Thesis. February 2008. (PDF)
• Lucy Mendel. Modeling by Example. MIT MEng Thesis. September 2007. (PDF)
• Vincent S. Yeung. Declarative Configuration Applied to Course Scheduling. MIT MEng Thesis. May, 2006. (PDF)
• Amerson H. Lin. Automated Analysis of Security APIs. MIT MEng Thesis. May 2005. (PDF)
• Ilya Shlyakhter. Declarative Symbolic Pure Logic Model Checking. MIT PhD Thesis. Feb 2005. (PDF)
• Robert Seater. Core Extraction and Non-Example Generation: Debugging and Understanding Logical Models. MIT Masters Thesis, November 2004. (PDF)
• Mandana Vaziri. Finding Bugs in Software with a Constraint Solver. MIT PhD Thesis. Feb 2004. (PDF)
• Emina Torlak. Subtyping in Alloy. MIT Masters Thesis, May 2004. (PDF)
• Sarfraz Kurshid. Generating Structurally Complex Tests from Declarative Constraints. MIT PhD Thesis. Feb 2003. (PDF)
• Greg Dennis. TSAFE: Building a Trusted Computing Base for Air Traffic Control Software. MIT Masters Thesis, January 2003. (PS) (PDF)
• Roshan Gupta. The Design and Implementation of FIG: A Record/Playback Mechanism for ETMS Feeds. MIT Masters Thesis, January 2003. (PS) (PDF)
• Mana Taghdiri. Lightweight Modelling and Automatic Analysis of Multicast Key Management Schemes. MIT Masters Thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, December 2002. (PS) (PDF)
• Tina Nolte. Exploring Filesystem Synchronization with Lightweight Modeling and Analysis. MIT Masters thesis, August 2002. (PS) (PDF)
• Allison Waingold. Automated Extraction of Abstract Object Models. MIT Masters Thesis, May 2001. (PS) (PDF)