MulSaw: Automated Checking of Code Conformance
We are developing novel techniques for automating testing of object-oriented programs. We have designed two complementary frameworks, TestEra and Korat, to automate specification-based testing of Java programs. TestEra uses specifications given in Alloy and uses the Alloy Analyzer, as an enabling technology, for test case generation and correctness checking. Korat uses specifications given in the Java Modeling Language and provides a novel technique for generating inputs from Java predicates. To test a method, TestEra and Korat automatically generate all non-isomorphic test cases (within a given size) from the method's pre-condition and check its correctness using its post-condition as a test oracle. We have used TestEra and Korat to check several programs including data structure implementations from the Java Collections Framework on inputs that give full statement coverage.
For more information, visit the MulSaw hompage or email khurshid@lcs.mit.edu.
Members
- Sarfraz Khurshid
- Darko Marinov
- Alexandr Andoni
- Chandrasekhar Boyapati