A Translator of Java Programs to TADDs
Artur Rataj, Bożena Woźna-Szcześniak, Andrzej Zbrzezny · Fundamenta Informaticae · 2009
The model checking tools Uppaal and VerICS accept a description of a network of Timed Automata with Discrete Data (TADDs) as input. Thus, to verify a concurrent programwritten in Java by means of these tools, first a TADD model of the program must be