Mechanical software verification: high level control aspects from a user's perspective

DOI10.1016/S1571-0661(04)00282-8MaRDI QIDQ2841237zbMATH OpenOpenAlexFDO

Authors Wolfgang Goerigk

Publication date 24 July 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s1571-0661(04)00282-8

Mathematics Subject Classification ID

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

Recommendations

• Mechanized result verification: An industrial application
• Overview on mechanized theorem proving
• scientific article; zbMATH DE number 2177632
• Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
• scientific article; zbMATH DE number 1746646

Cites work

• scientific article; zbMATH DE number 4195192 (Why is no real title available?)
• scientific article; zbMATH DE number 44976 (Why is no real title available?)
• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 1487489 (Why is no real title available?)
• scientific article; zbMATH DE number 2102699 (Why is no real title available?)
• scientific article; zbMATH DE number 1390248 (Why is no real title available?)
• An axiomatic basis for computer programming
• Compiler specification and verification
• SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
• Weakest relative precondition semantics. Balancing approved theory and realistic translation verification

Cited in

(3)

• Mechanized result verification: An industrial application
• An integrated approach to high integrity software verification
• Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)

Describes a project that uses

Uses Software

• ComLisp
• Piton
• CESAR
• PVS
• ACL2

This page was built for publication: Mechanical software verification: high level control aspects from a user's perspective

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