Logo image
Back
Programming with Proofs: Language-Based Approaches to Totally Correct Software
Book chapter   Open access   Peer reviewed

Programming with Proofs: Language-Based Approaches to Totally Correct Software

Aaron Stump
Verified Software: Theories, Tools, Experiments, pp.502-509
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2008
DOI: 10.1007/978-3-540-69149-5_55
url
https://doi.org/10.1007/978-3-540-69149-5_55View
Published (Version of record) Open Access

Abstract

Tremendous progress has been made in automated and semi-automated verification since the seminal works on program verification. Automated deductive techniques like model checking have been highly successful for many verification tasks (e.g., [17, 18, 13]). Impressive advances continue to be made in static analysis, type systems, and static bug finding (e.g., [21, 12]). These approaches aim to verify code or find bugs in existing systems as automatically as possible, with as little developer help as possible. This has been the aim of the research community for many years, possibly due in part to the bad reputation that continues to plague full program verification. Theorem proving approaches to program verification have continued to make advances, but indeed, they still are generally applied only to the most critical applications (e.g., [7, 5, 16, 11]).
 Dynamic Logic Model Check Operational Semantic Theorem Prove Type Theory

Details

Metrics

29 Record Views
Logo image