Proving Theorems About JML Classes

DOI10.1007/978-3-540-75221-9_11zbMath1151.68348OpenAlexW1559377248MaRDI QIDQ3526934

Leo Freitas, J. C. P. Woodcock

Publication date: 25 September 2008

Published in: Formal Methods and Hybrid Real-Time Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-75221-9_11

zbMATH Keywords

formal specificationZsoftware verificationJMLmechanical theorem provingZ/Evesgrand challenge in verified softwareverified software repositoryJava modeling languageJava collections frameworkJava HashMap classlinking theories

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (2)

Formalizing workflows partitioning over federated clouds: multi-level security and costs ⋮ POSIX file store in Z/Eves: An experiment in the verified software repository

Uses Software

• JML
• Z/EVES

This page was built for publication: Proving Theorems About JML Classes