Welcome to the [[now defunct]] MulSaw project on software reliability.

[[This is a slightly edited state of the MulSaw project web page as found some time in 2004, with the comments in double square brackets added in 2007.]]
[[[[A new update in quadruple brackets added in 2010.]]]]

[[The MulSaw project was initiated (somewhere around March 2001) and led by Sarfraz Khurshid and Darko Marinov who were at the time PhD students in the MIT LCS (now CS & AI Lab). Sarfraz defended his PhD in December 2003 and joined the UT Austin ECE department in January 2004. Darko defended his PhD in December 2004 and joined the UIUC CS department in January 2005. The MulSaw project then officially stopped, although Sarfraz and Darko have continued their successful collaboration.]]

[[In numbers, the MulSaw project resulted in 13 publications (2 PhD dissertations, 1 journal paper, 7 conference papers, 2 workshop papers, and 1 technical report) and involved in various capacities 17 more people (2 PhD advisors, 1 postdoc, 1 researcher from an industrial lab, 4 other PhD students, and 9 undergraduate and M.Eng. students). In words, the MulSaw project was a lot of fun!]]

The goal of our project is to design and implement a specification language for object-oriented programs and tools for checking code conformance, i.e., tools for checking that programs correctly implement their specifications. Although we do our research in the context of the Java programming language, most of our results can easily be applied to other languages. Our initial research focuses on developing a general specification language and tools for checking code conformance for fairly complete behavioral specifications. [[Most of our results were on testing, and actually both of our PhD dissertations were on testing, Sarfraz's on the TestEra approach and Darko's on the Korat approach.]]

People
Themes
Publications
Extensions

People

Project leaders

[[We are thankful to our advisors who gave us all the freedom to run the MulSaw project and supported us in every way (including with RAs) throughout the project.]]

Sarfraz Khurshid (advisor: Daniel Jackson)
Darko Marinov (advisor: Martin Rinard)

Collaborators

[[We were fortunate to collaborate with two other PhD students (Chandra and Ilya), a postdoc (Kostas), and a researcher from MSR (Lintao) on various parts of the MulSaw project. We have not published anything with Viktor or Alex (who were also PhD students), but our work greatly benefited from extensive discussions with them.]]
[[[[Update in 2010: Meanwhile we collaborated with Viktor and published a joint paper. We hope to work with Alex at some point in the future.]]]]

Konstantine Arkoudas
Chandrasekhar Boyapati
Viktor Kuncak
Alexandru Salcianu
Ilya Shlyakhter
Lintao Zhang

Supervised students

[[We were fortunate to work with nine undergraduate and M.Eng. students in the MulSaw project, mostly on Advanced Undergraduate Projects (AUP) and through the Undergraduate Research Opportunities Program (UROP).]]

Omar Abdala [[UROP]]
Basel Al-Naffouri [[AUP, also M.Eng., thesis not supervised]]
Alexandr Andoni [[UROP]]
Faisal Anwar [[UROP]]
Suhabe Bugrara [[UROP]]
Dumitru Daniliuc [[UROP]]
Ang-Chih (Brendan) Kao [[M.Eng., thesis not supervised]]
Jelani Nelson [[UROP]]
Lev Teytelman [[AUP]]

Themes

AAL

The Alloy Annotation Language (AAL) is a language (under development) for annotating Java code based on the Alloy modeling language. It offers a syntax similar to the Java Modeling Language (JML), and the same opportunities for generation of run-time assertions. In addition, however, AAL offers the possibility of fully automatic compile-time analysis. Several kinds of analysis are supported, including: checking the code of a method against its specification; checking that the specification of a method in a subclass is compatible with the specification in the superclass; and checking properties relating method calls on different objects, such as that the equals methods of a class (and its overridings) induce an equivalence. Using partial models in place of code, it is also possible to analyze object-oriented designs in the abstract: investigating, for example, a view relationship amongst objects.

The paper gives examples of annotations and such analyses. It presents (informally) a systematic translation of annotations into Alloy, a simple first-order logic with relational operators. By doing so, it makes Alloy's automatic analysis, which is based on state-of-the-art SAT solvers, applicable to the analysis of object-oriented programs, and demonstrates the power of a simple logic as the basis for an annotation language.

Korat

Korat is a framework for automated testing of Java programs. Given a formal specification for a method, Korat uses the method precondition to automatically generate all nonisomorphic test cases bounded by a given size. Korat then executes the method on each of these test cases, and uses the method postcondition as a test oracle to check the correctness of each output.

To generate test cases for a method, Korat constructs a Java predicate (i.e., a method that returns a boolean) from the method's precondition. The heart of Korat is a technique for automatic test case generation: given a predicate and a bound on the size of its inputs, Korat generates all nonisomorphic inputs for which the predicate returns true. Korat exhaustively explores the input space of the predicate but does so efficiently by monitoring the predicate's executions and pruning large portions of the search space.

We illustrate the use of Korat for testing several data structures, including some from the Java Collections Framework. The experimental results show that it is feasible to generate test cases from Java predicates, even when the search space for inputs is very large. We also compares Korat with a testing framework based on declarative specifications. Contrary to our initial expectation, the experiments show that Korat generates test cases much faster than the declarative framework.

TestEra

TestEra is another framework for automated testing of Java programs. TestEra automatically generates all non-isomorphic test cases, within a given input size, and evaluates correctness criteria. As an enabling technology, TestEra uses Alloy, a first-order relational language, and the Alloy Analyzer. Checking a program with TestEra involves modeling the correctness criteria for the program in Alloy and specifying abstraction and concretization translations between instances of Alloy models and Java data structures. TestEra produces concrete Java inputs as counterexamples to violated correctness criteria. We have applied TestEra's analysis in several case studies: methods that manipulate singly linked lists and red-black trees, a naming architecture, and a part of the Alloy Analyzer.

Prioni

Prioni is a tool that integrates model checking and theorem proving for relational reasoning. Prioni takes as input formulas written in Alloy, a declarative language based on relations. Prioni uses the Alloy Analyzer to check the validity of Alloy formulas for a given scope that bounds the universe of discourse. The Alloy Analyzer can refute a formula if a counterexample exists within the given scope, but cannot prove that the formula holds for all scopes. For proofs, Prioni uses Athena, a denotational proof language. Prioni translates Alloy formulas into Athena proof obligations and uses the Athena tool for proof discovery and checking.

Publications

  1. D. Marinov, S. Khurshid, S. Bugrara, L. Zhang, and M. Rinard
    Optimizations for compiling declarative models into boolean formulas
    International Conference on Theory and Applications of Satisfiability Testing
    (SAT 2005), volume 3569 of LNCS, pages 187-202, St. Andrews, UK, June 2005

  2. D. Marinov
    Automatic testing of software with structurally complex inputs
    PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, December 2004

  3. S. Khurshid and D. Marinov
    TestEra: Specification-based testing of Java programs using SAT
    Automated Software Engineering Journal
    (JASE 2004), 11(4):403-434, October 2004

  4. S. Khurshid
    Generating structurally complex tests from declarative constraints
    PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, December 2003

  5. D. Marinov, A. Andoni, D. Daniliuc, S. Khurshid, and M. Rinard
    An evaluation of [[bounded-]]exhaustive testing for data structures
    Technical Report MIT-LCS-TR-921, MIT CSAIL, Cambridge, MA, September 2003

  6. 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 2003), Malente, Germany, May 2003

  7. S. Khurshid, D. Marinov, I. Shlyakhter, and D. Jackson
    A case for efficient solution enumeration
    Sixth International Conference on Theory and Applications of Satisfiability Testing
    (SAT 2003), Santa Margherita Ligure, Italy, May 2003

  8. S. Khurshid, D. Marinov, and D. Jackson
    An analyzable annotation language
    17th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications
    (OOPSLA 2002), pages 231-245, Seattle, WA, November 2002

  9. D. Marinov and S. Khurshid
    VAlloy: Virtual functions meet a relational language
    International Symposium of Formal Methods Europe, Getting IT Right
    (FME 2002), volume 2391 of LNCS, pages 234-251, Copenhagen, Denmark, July 2002

  10. C. Boyapati, S. Khurshid, and D. Marinov
    Korat: Automated testing based on Java predicates
    International Symposium on Software Testing and Analysis
    (ISSTA 2002), pages 123-133, Rome, Italy, July 2002
    (This paper won an ACM SIGSOFT Distinguished Paper Award.)

  11. D. Marinov and S. Khurshid
    TestEra: A novel framework for testing Java programs
    16th IEEE Conference on Automated Software Engineering
    (ASE 2001), pages 22-31, San Diego, CA, November 2001
    (This paper was nominated for the best paper award.)

  12. S. Khurshid and D. Marinov
    Checking Java implementation of a naming architecture using TestEra
    Electronic Notes in Theoretical Computer Science, 55(3), July 2001

Suggested extensions for future work

[[Many of the topics proposed here have been addressed meanwhile, by other researchers or by us.]]

We list here some project suggestions related to our previous work in the MulSaw project. Some of these suggestions are entry-level and suitable for undergraduates, while others can lead to Master's and even Ph.D. theses. We would like to hear from you if you are interested in collaborating with us on some of these or other ideas. You can send us an email. [[We are still interested in collaborations, but this email address is not the best way to reach us; even though it seems that forwarding still works (and we get some spam through it ocassionally), you should email us directly at the addresses found on the Sarfraz's and Darko's home web pages.]]

Alloy Annotation Language (AAL)

Implement dynamic checking

Translate AAL annotations to Java assertions that can be checked at runtime.

Extend AAL

This project would extend AAL with primitive types, arrays, and Java method invocations.

Translate JML to AAL

The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules. A translation from JML to AAL would enable using the Alloy Analyzer to provide static checking of JML specifications.

Translate AAL to JML

The JML toolset provides dynamic checking of Java programs annotated with JML. A translation from AAL to JML would enable using the existing JML toolset to provide dynamic checking of Java programs annotated with AAL.

Use Korat search for AAL

This project would consider using Korat to generate structures for the Java predicates that are produced by the AAL to Java translation.

Implement static checking

This project involves translating Java code and AAL annotations into Alloy. [[This was the topic of Mandana Vaziri's PhD dissertation.]]

Verification

Extend Alloy analysis for verification

The analysis of the Alloy Analyzer is valid only for instances within the given bounds. This project would explore cases where results of this analysis can be generalized to hold for instances of any size. [[Viktor Kuncak did work on this.]]

Korat

Reimplement Korat

The current Korat prototype uses modified javac compiler to instrument source code. This project would instead use byte-code instrumentation which would enable using Korat when source code is not available. [[Aleksandar Milicevic and Sasa Misailovic did this.]]

Reimplement Ferastrau

Ferastrau is a framework for mutation testing of Java programs. This project would optimize mutant execution of the current prototype.

Use Korat search for Alloy specs

This project explores "directly" solving for instances of Alloy-like specifications, using state-space pruning of Korat.

Use Korat for white-box testing

We have so far used Korat for specification-based, or black-box, testing. We would like to use Korat to "directly" generate inputs that satisfy a specified coverage criteria, such as statement or branch coverage, while also satisfying the precondition, such as acyclicity.

Use genetic algorithms to guide Korat search

This project would explore using genetic algorithms to guide Korat's search of a predicate's input space; the genetic search can use a fitness measure based on the predicate's executions.

Add symbolic execution to Korat search

Korat currently treats data, such as integer variables, by enumerating the range of possible values specified by the finitization. We would like to add symbolic execution to Korat's search and use it in conjunction with off-the-shelf constraint solvers.

Test TSAFE implementation

The Tactical Separation Assisted Flight Environment (TSAFE) is a decision support tool for air traffic controllers. This project would use Korat to test the TSAFE prototype under development in LCS.

Use model checking for generating inputs

This project would evaluate using a model checker for generating structures from sequences of method invocations. The model checker can use the method preconditions to constrain these invocation sequences so that they produce only valid structures. [[There have been a few projects along this line.]]

Translate repOk to Alloy

This project would evaluate an alternative approach to finding inputs that satisfy repOk: translate repOk to Alloy and then use the Alloy Analyzer. There are several ways to translate repOk, for example:
  1. translate repOk to Alloy using finite scope
  2. extract structural invariants in Alloy
  3. translate to Alloy using Daikon, i.e., use test inputs generated from repOk and feed them to Daikon to detect structural invariants

TestEra

Generate test inputs from algebraic specifications (a-la-TestEra)

Generate instances of data structure abstractions and use each instance to build one or several concrete inputs.