Computer Science and
Artificial Intelligence Laboratory
SDG Publications 1999-2008
2008 Papers
- 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. To appear.
- 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).
- 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
- 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)