Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
Recent advances in deductive program verification correlate with the evolution of logics for modular reasoning about complex programs. Verification techniques built upon these logics require automation to help to verify practically essential rich program properties that summarize data structures via quantification or some form of abstraction. However, many such properties are higher-order (e.g., data structure comprehensions like sequence-fold), precluding automation. Furthermore, some rich properties (e.g., reachability between dynamically interlinked objects) are non-compositional; that is, one cannot compose the property of a data structure based solely on the properties of its disjoint sub-structures. However, compositionality is a prerequisite of automated modular reasoning (due to the problem commonly known as framing). If compositionality holds, the programmer can independently reason about each method in an application without considering the implementation of other methods, e.g., library code. The goal of this thesis is to develop compositional — i.e., automated and modular — techniques for verifying rich program properties. We build on top of separation logic, a prominent program logic that enables modular reasoning about heap-transforming, concurrently executed programs. The specification language of separation logic expresses memory safety properties, but complementary techniques for handling rich properties are underdeveloped, especially in an automated setting. The two classes of rich properties that we consider are data structure comprehensions and heap reachability properties. An additional goal of the thesis is to develop techniques for automated verification debugging, aiding the programmer in authoring formal specifications and verified programs. Our first contribution is a technique for reasoning about the class of (higher-order, compositional) comprehensive properties. These properties summarize data structures containing potentially unbounded (and statically unknown) object sets via a ...