Harald Søndergaard

In 1970, Dana Scott proposed his highly influential “mathematical theory of computation” to define the relationship between the text of a program and what the program computes (or denotes)—the “semantics” of the program. Scott used a complete lattice based on the “information ordering”, with the bottom element representing undefined—a program failing to terminate normally, thus producing no information. The top element, however, was unused. Hence most subsequent applications of denotational semantics have used mathematical structures that avoid top elements. We suggest that the information ordering is relevant not only to semanticists but also to working programmers as a basis for determining if a program component or a computation is correct according to their intentions. We also suggest that a return to the use of complete lattices is called for, to broaden formal semantics and allow it to encompass programmer intentions. That is because often those intentions permit more than one runtime behaviour for a given input. In this paper we explore the connections between the information ordering, correctness of computations and programs, and debugging. We present a general theory and describe several instances where the intention for what our logic/functional code computes plus what it actually computes can be described by elements in a complete lattice. For correct code, the information order relates (1) what is intended and what is computed, (2) successive states of a computation, and (3) the left and right sides of program component definitions. For bugs, the information order is violated. The technical results are a reasonably straightforward extension to previous denotational semantics work, but the scheme aligns much better with practical programming and software tools. The theory extends both the theoretical basis and practical flexibility of declarative debugging and reasoning about partial correctness and gives an attractive mathematical framework that encompasses our intentions, our programs and what they compute.

In 1970, Dana Scott proposed his highly influential ''mathematical theory of computation'' to define the relationship between the text of a program and what the program computes (or denotes) --- the ''semantics'' of the program. Scott used a complete lattice based on the ''information ordering'', with the bottom element representing undefined --- a program failing to terminate normally, thus producing no information. The top element, however, was unused. Hence most subsequent applications of denotational semantics have used mathematical structures that avoid top elements. We suggest that the information ordering is relevant not only to semanticists, but also to working programmers, as a basis for determining if a program component or a computation is correct according to their intentions. We also suggest that a return to the use of complete lattices is called for if we wish to broaden formal semantics to allow it to encompass programmer intentions. That is because often those intentions permit more than one runtime behaviour for a given input. For example, several declarative debugging tools allow a programmer to declare that a runtime call is ''inadmissible'', loosely meaning the called program component should never be used with such input. If the input is garbage, the programmer does not care what garbage is output --- all results are acceptable, which can be modeled by the top element of a complete lattice. In this paper we explore the connections between the information ordering, correctness of computations and programs, and debugging. We present a general theory and describe several instances where the intention for what our logic/functional code computes plus what it actually computes can be described by elements in a complete lattice. This extends both the theoretical basis and practical flexibility of declarative debugging and reasoning about partial correctness and gives an attractive mathematical framework that encompasses our intentions, our programs and what they compute.

Precondition inference is a non-trivial problem with important applications in program analysis and verification. We present a novel iterative method for automatically deriving preconditions for the safety and unsafety of programs. Each iteration maintains over-approximations of the set of safe and unsafe initial states, which are used to partition the program’s initial states into those known to be safe, known to be unsafe and unknown. We then construct revised programs with those unknown initial states and iterate the procedure until the approximations are disjoint or some termination criteria are met. An experimental evaluation of the method on a set of software verification benchmarks shows that it can infer precise preconditions (sometimes optimal) that are not possible using previous methods.

Zones and Octagons are popular abstract domains for static program analysis. They enable the automated discovery of simple numerical relations that hold between pairs of program variables. Both domains are well understood mathematically but the detailed implementation of static analyses based on these domains poses many interesting algorithmic challenges. In this article, we study the two abstract domains, their implementation and use. Utilizing improved data structures and algorithms for the manipulation of graphs that represent difference-bound constraints, we present fast implementations of both abstract domains, built around a common infrastructure. We compare the performance of these implementations against alternative approaches offering the same precision. We quantify the differences in performance by measuring their speed and precision on standard benchmarks. We also assess, in the context of software verification, the extent to which the improved precision translates to better verification outcomes. Experiments demonstrate that our new implementations improve the state of the art for both Zones and Octagons significantly.

Dynamic symbolic execution (DSE) is a non-standard execution mechanism which, loosely, executes a program symbolically and, simultaneously, on concrete input. DSE is attractive because of several uses in software engineering, including the generation of test data suites with large coverage relative to test suite size. However, DSE struggles in the face of execution path explosion, and is often unable to cover certain kinds of difficult-to-reach program points. Invariant inlay is a technique that aims to improve a DSE tool by interspersing code with invariants, generated automatically using off-the-shelf tools for static program analysis using abstract interpretation. To capitalise fully on a static analyzer, invariant inlay applies certain instrumentations and testability transformations to the program source. In this paper we outline the invariant inlay approach, and how we have evaluated the idea, in order to determine its usefulness for programs with complex control flow.