The LOOP compiler for Java and JML

DOI10.1007/3-540-45319-9_21MaRDI QIDQ2769594zbMATH OpenFDO

Authors Joachim van den Berg, Bart Jacobs

Publication date 5 February 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2031/20310299

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99)

Recommendations

• A logic for the Java modeling language JML
• scientific article; zbMATH DE number 2090288
• Computer Aided Verification
• Weakest pre-condition reasoning for Java programs with JML annotations
• A Bytecode Logic for JML and Types

Cited in

(19)

• Coalgebras and monads in the semantics of Java
• Weakest pre-condition reasoning for Java programs with JML annotations
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Source code verification of a secure payment applet
• LOOP
• Algebraic-coalgebraic specification in CoCASL
• A program logic for resources
• A proof outline logic for object-oriented programming
• Are the logical foundations of verifying compiler prototypes matching user expectations?
• A logic for the Java modeling language JML
• Programmed strategies for program verification
• A graph-based implementation for mechanized refinement calculus of OO programs
• Proving Theorems About JML Classes
• JCML: A specification language for the runtime verification of Java card programs
• scientific article; zbMATH DE number 2087575 (Why is no real title available?)
• scientific article; zbMATH DE number 2090026 (Why is no real title available?)
• Specification and runtime verification of Java card programs
• PVS as a proof obligation generator
• A generic complete dynamic logic for reasoning about purity and effects

Describes a project that uses

Uses Software

• PVS
• JML

This page was built for publication: The LOOP compiler for Java and JML

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2769594)