Invited Talk at FMOODS
2003 - 19 November 2003
Java's Integral Types in PVS
by Bart Jacobs
This paper presents an extension of the standard bitvector library of
the theorem prover PVS with multiplication, division and remainder operations, together with associated results. This extension is needed
to give correct semantics to Java's integral types in program verification. Special emphasis is put on Java's widening and narrowing
functions in relation to the newly defined operations on bitvectors.