SRC Technical Note 1999-002

Checking Java programs via guarded commands

K. Rustan M. Leino, James B. Saxe, and Raymie Stata

This paper defines a simple guarded-command-like language and its semantics. The language is used as an intermediate language in generating verification conditions for Java. The paper discusses why it is a good idea to generate verification conditions via an intermediate language, rather than directly.

Back to the SRC Technical Notes main page.

• PostScript compressed with UNIX compress -- 120 Kbytes
  
• PostScript compressed with GNU compress (gzip) -- 60 Kbytes
  
• PostScript compressed with ZIP -- 60 Kbytes
  
• PostScript -- 216 Kbytes
  
• Portable Document Format (PDF) -- 37 Kbytes