Verified squared, does critical software deserve verified tools?

DOI10.1145/1926385.1926387MaRDI QIDQ5408525zbMATH OpenOpenAlexFDO

Authors Xavier Leroy

Publication date 10 April 2014

Published in Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1926385.1926387

zbMATH Keywords

compiler verificationcritical softwareprogram proofstatic analysisverification tools

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verified software toolchain (invited talk)
• Software Verification and Analysis
• The verified software repository: a step towards the verifying compiler
• scientific article; zbMATH DE number 47348
• Panellist position statement: some industrial experience with program verification

Cited in

(11)

• A comparison of tools for teaching formal software verification
• Experience of improving the BLAST static verification tool
• A verification tool developer's vade mecum.
• The verified software repository: a step towards the verifying compiler
• Are the logical foundations of verifying compiler prototypes matching user expectations?
• Verified software toolchain (invited talk)
• Correct code containing containers
• scientific article; zbMATH DE number 2033523 (Why is no real title available?)
• scientific article; zbMATH DE number 1796119 (Why is no real title available?)
• Empirical software metrics for benchmarking of verification tools
• Early verification and validation of mission critical systems

This page was built for publication: Verified squared, does critical software deserve verified tools?

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