translator of Java programs to TADDs
FREE-DOWNLOAD A Rataj, B Wozna… – Fundamenta Informaticae, 2009
Abstract. 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 program written in
Java by means of these tools, first a TADD model of the program must be build. Therefore,