Social processes, program verification and all that

DOI10.1017/S0960129509990041MaRDI QIDQ3643359zbMATH OpenFDO

Authors Andrea Asperti, Herman Geuvers, Raja Natarajan

Publication date 11 November 2009

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0960129509990041

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

• Program verification. Fundamental issues in computer science
• Foreword to the special focus on formal proofs for mathematics and computer science
• Verification is experimentation!
• scientific article; zbMATH DE number 1759598
• Proving and programming

Cites work

• scientific article; zbMATH DE number 3521895 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• A Modular Formalisation of Finite Group Theory
• A formally verified proof of the prime number theorem
• A proof of the Kepler conjecture
• A symmetric lambda calculus for classical program extraction
• A syntactic approach to foundational proof-carrying code
• About the Formalization of Some Results by Chebyshev in Number Theory
• An axiomatic basis for computer programming
• Don't eliminate cut
• On a cultural gap
• On the proof of correctness of a calendar program
• OpenMath
• Operating system verification---an overview
• Proof assistants: history, ideas and future
• Proving the correctness of client/server software
• Solvability of groups of odd order

Cited in

(6)

• 2011 North American Annual Meeting of the Association for Symbolic Logic, University of California at Berkeley, Berkeley, CA, USA, March 24--27, 2011
• Social software
• Program verification. Fundamental issues in computer science
• scientific article; zbMATH DE number 2085178 (Why is no real title available?)
• scientific article; zbMATH DE number 7526292 (Why is no real title available?)
• A vindication of program verification

Describes a project that uses

Uses Software

• Nuprl
• Isar

This page was built for publication: Social processes, program verification and all that

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