Related papers: Automatic Function Annotations for Hoare Logic
I present a new method for specifying and verifying the partial correctness of sequential programs. The key observation is that, in Hoare logic, assertions are used as selectors of states, that is, an assertion specifies the set of program…
Hoare logics are proof systems that allow one to formally establish properties of computer programs. Traditional Hoare logics prove properties of individual program executions (such as functional correctness). Hoare logic has been…
We present a so-called labelling method to insert cost annotations in a higher-order functional program, to certify their correctness with respect to a standard compilation chain to assembly code including safe memory management, and to…
A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tableau for partial correctness can be transformed into an…
We show that a partial-correctness assertion about an iterative program is provable in Hoare Logic iffit is provable in standard second-order logic with comprehension restricted to first-order predicates. This equivalence was claimed twice…
We present simple new Hoare logics and refinement calculi for hybrid systems in the style of differential dynamic logic. (Refinement) Kleene algebra with tests is used for reasoning about the program structure and generating verification…
Foundational verification considers the functional correctness of programming languages with formalized semantics and uses proof assistants (e.g., Coq, Isabelle) to certify proofs. The need for verifying complex programs compels it to…
Higher-order functions and imperative states are language features supported by many mainstream languages. Their combination is expressive and useful, but complicates specification and reasoning, due to the use of yet-to-be-instantiated…
Dynamically typed object-oriented languages enable programmers to write elegant, reusable and extensible programs. However, with the current methodology for program verification, the absence of static type information creates significant…
This paper presents an extension to Hoare logic for pointer program verification. Logic formulas with user-defined recursive functions are used to specify properties on the program states before/after program executions. Three basic…
Programs must be correct with respect to their application domain. Yet, the program specification and verification approaches so far only consider correctness in terms of computations. In this work, we present a two-tier Hoare Logic that…
Hoare-style program logics are a popular and effective technique for software verification. Relational program logics are an instance of this approach that enables reasoning about relationships between the execution of two or more programs.…
We present a tool for verification of hybrid systems expressed in the sequential fragment of HCSP (Hybrid Communicating Sequential Processes). The tool permits annotating HCSP programs with pre- and postconditions, invariants, and proof…
Verifying a real-world program's functional correctness can be decomposed into (1) a refinement proof showing that the program implements a more abstract high-level program and (2) an algorithm correctness proof at the high level.…
We propose a probabilistic Hoare logic aHL based on the union bound, a tool from basic probability theory. While the union bound is simple, it is an extremely common tool for analyzing randomized algorithms. In formal verification terms,…
We consider the problem of how to verify the security of probabilistic oblivious algorithms formally and systematically. Unfortunately, prior program logics fail to support a number of complexities that feature in the semantics and…
Separation logic is a Hoare-style logic for reasoning about programs with heap-allocated mutable data structures. As a step toward extending separation logic to high-level languages with ML-style general (higher-order) storage, we…
We present a Hoare logic that extends program specifications with regular expressions that capture behaviors in terms of sequences of events that arise during the execution. The idea is similar to session types or process-like behavioral…
Hoare logic is a foundation of axiomatic semantics of classical programs and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to…
We propose a general framework to allow: (a) specifying the operational semantics of a programming language; and (b) stating and proving properties about program correctness. Our framework is based on a many-sorted system of hybrid modal…