Welcome to the MulSaw project on software reliability.

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.

People
Themes
Papers
Extensions

People

Project leader

Darko Marinov (advisor: Martin Rinard)

Project co-founder

Sarfraz Khurshid (advisor: Daniel Jackson; Sarfraz joined the UT Austin ECE department in January 2004)

Collaborators

Kostas Arkoudas
Chandrasekhar Boyapati
Viktor Kuncak
Alexandru Salcianu
Ilya Shlyakhter

M.Eng. students

Basel Al-Naffouri

Undergraduate students

Alexandr Andoni
Dumitru Daniliuc

Alumni

Omar Abdala
Faisal Anwar
Ang-Chih (Brendan) Kao
Jelani Nelson
Lev Teytelman

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.

Papers

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

  2. 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

  3. 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

  4. 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

  5. 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

  6. 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.)

  7. 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.)

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