A case study in class library verification: Java's vector class

DOI10.1007/S100090100047MaRDI QIDQ5953451zbMATH OpenOpenAlexWikidataFDO

Authors Marieke Huisman, Bart Jacobs, Joachim van den Berg

Publication date 23 January 2002

Published in International Journal on Software Tools for Technology Transfer. STTT (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2066/18844

zbMATH Keywords

Java's standard library

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2090026
• Computer Aided Verification
• FM 2005: Formal Methods
• scientific article; zbMATH DE number 1706337
• Verifying a class: combining testing and proving

Cited in

(9)

• Coalgebras and monads in the semantics of Java
• Weakest pre-condition reasoning for Java programs with JML annotations
• Verifying a class: combining testing and proving
• scientific article; zbMATH DE number 2013592 (Why is no real title available?)
• scientific article; zbMATH DE number 2090026 (Why is no real title available?)
• FM 2005: Formal Methods
• Java's integral types in PVS.
• Integrating ADTs in KeY and their application to history-based reasoning about collection
• Integrating ADTs in KeY and Their Application to History-Based Reasoning

Describes a project that uses

Uses Software

• JML
• PVS

This page was built for publication: A case study in class library verification: Java's vector class

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