An axiomatic basis for computer programming

By John Wickerson, M. Dodds. 1969

Subfields: Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Program Analysis & Verification

1. Miltiadis Allamanis
2. Charles Sutton
3. Earl T. Barr
4. Premkumar T. Devanbu
5. Jerry Swan
6. Edmund M. Clarke
7. Parthasarathy Madhusudan
8. Rajeev Alur

Citations in the corpus

• A Survey of Machine Learning for Big Code and Naturalness (2017, background): “, purity of a function [60] or pre-/post- conditions [90]) is hard to do, especially at scale.”
• The software model checker Blast (2007, unknown): “Program verification has been a central problem since the early days of computer science [33, 49, 62, 63].”
• A Software Analysis Perspective (2012, methodology): “The WP plug-in is named after the Weakest Precondition calculus, a technique used to prove program properties initiated by Hoare [32], Floyd [28] and Dijkstra [25].”
• A Temporal Logic of Nested Calls and Returns (2004, background): “Correctness of program blocks with respect to pre and post conditions has been emphasized in the veri cation literature since the early days of logics for structured programs [15], and also forms an integral part of modern interface speci cation languages for object oriented programming such as JML ”
• Counterexample-Driven Genetic Programming: Heuristic Program Synthesis from Formal Specifications (2018, methodology): “Instead of model-checking, the Hoare logic (Hoare, 1969) is used for the specification of the task and verification.”
• Frama-C: A software analysis perspective (2015, methodology): “This way, the overhead of Typed model with respect to Hoare is kept to the places where it is really needed.”
• Modular verification of software components in C (2003, methodology): “The algorithm uses a procedure for computing the weakest precondition WP [11], [46], [47] of a predicate p relative to a given statement.”
• Adding nesting structure to words (2006, background): “More broadly, modeling structured programs and program specifications as languages of nested words generalizes the linear-time semantics that allows integration of Pnueli-style temporal reasoning [Pnueli 1977] and Hoarestyle structured reasoning [ Hoare 1969 ].”
• Linguistic side effects (2005, background): “1989), as well as reasoned about using logical axioms (Hoare 1969).”