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.