Open Systems Laboratory at Illinois

Test generation through programming in udita

By Milos Gligoric, Tihomir Gvero, Vilas Jagannath, Sarfraz Khurshid, Viktor Kuncak, and Darko Marinov. In ICSE (1), 225–234. ACM, 2010.

Full Text:
Download PDF
Publisher Link:


We present an approach for describing tests using non-deterministic test generation programs. To write such programs, we introduce UDITA, a Java-based language with non-deterministic choice operators and an interface for generating linked structures. We also describe new algorithms that generate concrete tests by efficiently exploring the space of all executions of non-deterministic UDITA programs.

We implemented our approach and incorporated it into the official, publicly available repository of Java PathFinder (JPF), a popular tool for verifying Java programs. We evaluate our technique by generating tests for data structures, refactoring engines, and JPF itself. Our experiments show that test generation using UDITA is faster and leads to test descriptions that are easier to write than in previous frameworks. Moreover, the novel execution mechanism of UDITA is essential for making test generation feasible. Using UDITA, we have discovered a number of bugs in Eclipse, NetBeans, Sun javac, and JPF.


    author = "Gligoric, Milos and Gvero, Tihomir and Jagannath, Vilas
              and Khurshid, Sarfraz and Kuncak, Viktor and Marinov, Darko",
    editor = "Kramer, Jeff and Bishop, Judith and Devanbu, Premkumar
              T. and Uchitel, Sebastián",
    title = "Test generation through programming in UDITA",
    booktitle = "ICSE (1)",
    crossref = "conf/icse/2010-1",
    ee = "",
    keywords = "software engineering",
    pages = "225-234",
    year = "2010",

    editor = "Kramer, Jeff and Bishop, Judith and Devanbu, Premkumar
              T. and Uchitel, Sebastián",
    title = "Proceedings of the 32nd ACM/IEEE International Conference
             on Software Engineering - Volume 1, ICSE 2010, Cape Town, South
             Africa, 1-8 May 2010",
    isbn = "978-1-60558-719-6",
    publisher = "ACM",
    year = "2010",