Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository

DOI10.1016/J.SCICO.2008.09.012MaRDI QIDQ1004294zbMATH OpenOpenAlexWikidataFDO

Authors Leo Freitas, Yichi Zhang, Jim Woodcock

Publication date 2 March 2009

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.scico.2008.09.012

zbMATH Keywords

theorem provingZ/Evesfile APIgrand challenge in verified softwareIBM CICSmechanical proofverification challenge problemsverified software repositoryZ notation

Mathematics Subject Classification ID

Theory of software (68N99)

Recommendations

• POSIX file store in Z/Eves: An experiment in the verified software repository
• The verified software repository: a step towards the verifying compiler
• VCS: a verifier for component-based systems

Cites work

• scientific article; zbMATH DE number 42431 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• scientific article; zbMATH DE number 795668 (Why is no real title available?)
• The verified software repository: a step towards the verifying compiler
• Z/Eves and the Mondex Electronic Purse

Cited in

(2)

• POSIX file store in Z/Eves: An experiment in the verified software repository
• The tokeneer experiments

Describes a project that uses

Uses Software

• Z
• Z/EVES

This page was built for publication: Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository

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