Paper Info
Title
JVer: a java verifier
Abstract
We describe JVer, a tool for verifying Java bytecode programs annotated with pre and post conditions in the style of Hoare and Dijkstra. JVer is similar to ESC/Java [1], except that: (1) it produces verification conditions for Java bytecode, not Java source; (2) it is sound, because it makes conservative assumptions about aliasing and heap modification; (3) it produces verification conditions directly using symbolic simulation, without an intermediate guarded-command language; (4) by restricting predicates to conjunctions of relations between integers, it produces verification conditions that are more efficient to verify than general first-order formulae; (5) it generates independently verifiable proofs using the Kettle proof-generating theorem prover [2].
Year
DOI
Venue
2005
10.1007/11513988_14
CAV
Keywords
Field
DocType
post condition,general first-order formula,verifying java bytecode program,intermediate guarded-command language,conservative assumption,verification condition,kettle proof-generating theorem prover,java verifier,java source,java bytecode,heap modification,theorem prover,first order
Programming language,Java annotation,Computer science,Real time Java,Algorithm,Theoretical computer science,Java bytecode,strictfp,Generics in Java,Java Modeling Language,Java applet,Java
Conference
Volume
ISSN
ISBN
3576
0302-9743
3-540-27231-3
Citations 
PageRank 
References 
5
0.51
4
Authors
5
Name
Order
Citations
PageRank
Ajay Chander121312.60
David Espinosa2322.07
Nayeem Islam3302.40
Peter Lee 00014975147.71
George Necula51186.66