Date Added: May 2010
The authors present an approach for describing tests using non-deterministic test generation programs. To write such programs, the authors introduce UDITA, a Java-based language with non-deterministic choice operators and an interface for generating linked structures. They also describe new algorithms that generate concrete tests by efficiently exploring the space of all executions of non-deterministic UDITA programs. The authors implemented their approach and incorporated it into the official, publicly available repository of Java PathFinder (JPF), a popular tool for verifying Java programs.