A Java code annotation approach for model checking software systems
Glauber Ferreira, Emerson Loureiro, Elthon Allex da Silva Oliveira · 2007
Many works related to the verification of software systems using model checking integrated to development environments have been proposed. JPF [7] and Bandera [1] are examples of such works that abstract the model to be verified from the Java code. An alternative way for JPF and Bandera approaches is to provide mechanisms for describing the model during the programming task. Thus, it is possible to integrate such mechanisms to the development environment and hide the model checking task from the programmer.