TestEra: Specification-based testing of java programs using SAT

Sarfraz Khurshid, Darko Marinov

Research output: Contribution to journalArticlepeer-review


TestEra is a framework for automated specification-based testing of Java programs. TestEra requires as input a Java method (in sourcecode or bytecode), a formal specification of the pre- and post-conditions of that method, and a bound that limits the size of the test cases to be generated. Using the method's pre-condition, TestEra automatically generates all nonisomorphic test inputs up to the given bound. It executes the method on each test input, and uses the method postcondition as an oracle to check the correctness of each output. Specifications are first-order logic formulae. As an enabling technology, TestEra uses the Alloy toolset, which provides an automatic SAT-based tool for analyzing first-order logic formulae. We have used TestEra to check several Java programs including an architecture for dynamic networks, the Alloy-alpha analyzer, a fault-tree analyzer, and methods from the Java Collection Framework.

Original languageEnglish (US)
Pages (from-to)403-434
Number of pages32
JournalAutomated Software Engineering
Issue number4
StatePublished - Oct 2004
Externally publishedYes


  • Alloy
  • Automated test generation
  • Java testing
  • SAT enumeration
  • Software testing
  • Specification-based testing
  • TestEra

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'TestEra: Specification-based testing of java programs using SAT'. Together they form a unique fingerprint.

Cite this