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

DOI10.1016/j.scico.2008.09.012zbMath1178.68527OpenAlexW2050774808WikidataQ126190056 ScholiaQ126190056MaRDI QIDQ1004294

Yichi Zhang, Leo Freitas, J. C. P. 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 notationZ/Evesfile APIgrand challenge in verified softwareIBM CICSmechanical proofverification challenge problemsverified software repository

Mathematics Subject Classification ID

Uses Software

• Z/EVES
• Z

Cites Work

• The verified software repository: a step towards the verifying compiler
• Z/Eves and the Mondex Electronic Purse
• Unnamed Item
• Unnamed Item
• Unnamed Item

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