Weakest pre-condition reasoning for Java programs with JML annotations
From MaRDI portal
Publication:1881666
DOI10.1016/j.jlap.2003.07.005zbMath1073.68024MaRDI QIDQ1881666
Publication date: 14 October 2004
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlap.2003.07.005
68N15: Theory of programming languages
Related Items
The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML, A proof outline logic for object-oriented programming, Specification and verification challenges for sequential object-oriented programs
Uses Software
Cites Work
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- Source code verification of a secure payment applet
- Programming as a Discipline of Mathematical Nature
- A case study in class library verification: Java's vector class
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item