Data processing: software development – installation – and managem – Software program development tool – Programming language
Reexamination Certificate
2007-02-20
2007-02-20
Khatri, Anil (Department: 2191)
Data processing: software development, installation, and managem
Software program development tool
Programming language
C717S108000, C717S116000
Reexamination Certificate
active
09720616
ABSTRACT:
In a method for verifying the safety properties of Java byte code programs, the functioning of the byte code program to be verified is modeled on a finite state transition system M, and the state space of the Java Virtual Machine (JVM) on a finite set of states in M. Once entered into a model checker, the data of finite state transition system M are compared to the data entered in the model checker as conditional set S to determine properties characterizing an acceptable byte code program. The byte code program to be checked is released for further processing only when the state transition system M fulfills all conditions of conditional set S.
REFERENCES:
patent: 5615137 (1997-03-01), Holzmann et al.
patent: 6110226 (2000-08-01), Bothner
patent: 6151703 (2000-11-01), Crelier
patent: 6170083 (2001-01-01), Adl-Tabatabai
patent: 6289502 (2001-09-01), Garland et al.
patent: 6353896 (2002-03-01), Holzmann et al.
patent: 6481006 (2002-11-01), Blandy et al.
patent: 6578020 (2003-06-01), Nguyen
patent: 6651186 (2003-11-01), Schwabe
patent: 6691306 (2004-02-01), Cohen et al.
patent: 6718539 (2004-04-01), Cohen et al.
patent: 6810519 (2004-10-01), Hicks
patent: 6883163 (2005-04-01), Schwabe
patent: 6981245 (2005-12-01), Schwabe
patent: 6986132 (2006-01-01), Schwabe
patent: 0 685 792 (1995-12-01), None
Knoblock et al, “Type elaboration and subtype completion for java bytecode”, ACM POPL pp. 228-242, 2000.
Corett, “Constructing compact models of concurrent java programs”, ACM ISSTA, pp. 1-10, 1998.
Freund et al, “A type system for object initialization in the java bytecode languages”, ACM OOPSLA, pp. 310-328, 1998.
Dwyer et al, “Tool supported program abstraction for finite state verification”, IEEE, pp. 177-187, 2001.
Lindholm, T. et al., “The Java Virtual Machine Specification,” Sun Microsystem; Addison-Wesley, 1996.
McMillan, K.L., “Symbolic Model Checking,” Kluwer Academic Publishers, 1993.
Posegga Joachim
Vogt Harald
Deutsche Telekom AG
Kenyon & Kenyon LLP
Khatri Anil
LandOfFree
Method for verifying safety properties of java byte code... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Method for verifying safety properties of java byte code..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method for verifying safety properties of java byte code... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3891771