Deductive Verification for Graph Transformation Systems
Graphs are ubiquitous in computer science because they model complex structures and relations—including pointers, object structures, network topologies, and software architectures—in a natural and intuitive way. The dynamic behaviour and evolution of these structures can also be expressed at this same high level of abstraction using graph transformation, which fuses the strengths of graphs (e.g. visual modelling) and rule-based rewriting (e.g. algebraic characterisations of transformations) into a single computational model.
Applications of graph transformation systems to defining analyses and semantics of languages and systems (such as shape safety analyses for pointer operations, or the semantics of model transformations, visual specification languages, and concurrent asynchronous programming abstractions) particularly motivate the question of how to formally reason about and verify their correctness. One approach is to translate them down to formats that classical verification techniques can handle; but the task easily blows up for inherently symmetric and dynamic problems. Another approach is to lift classical verification techniques to the domain of graphs and graph transformation and tailor verification directly to them, exploiting the symmetries and algebraic characterisations.
Our work takes the latter approach: we focus in particular on developing a rich theory to underpin deductive reasoning (e.g. Hoare logics) directly at the abstraction level of graphs, rules, and morphisms. Our contributions thus far include graph-based assertion logics for attribute expressions and monadic second-order structure (e.g. arbitrary-length paths, acyclity, connectedness, bipartiteness); effective weakest precondition constructions for rules; sound and (relatively) complete proof systems for programs constructed over rules; and some case studies. Ongoing work aims to simplify the theory, develop support for automation, and explore its role in complementary verification techniques, e.g. model checking, CEGAR.
Verification of Concurrent, Asynchronous, Distributed Programs
To harness the power of multi-core and distributed architectures, developers must program with concurrency, asynchronicity, and parallelism in mind. Classical thread-based approaches to concurrent programming, however, are difficult to master and error prone. To address this, a number of programming APIs, libraries, and languages have been proposed that provide safer and simpler-to-use models of concurrency, such as the block-dispatch model of Apple’s Grand Central Dispatch, or the message-passing-based model of Eiffel’s SCOOP.
Despite such abstractions, programs can still exhibit rich, complex behaviours—impossible to fully explore through testing—motivating the development of (semi-)algorithms for automated verification. These languages, however, typically pose several challenges for verification to overcome: intricate runtime features such as waiting queues, locks, and asynchronous remote calls; limited or absent formal models; and frequently evolving execution semantics as language designers discover, for example, more efficient strategies for realising the abstractions, or ones that safely permit more concurrency.
Our work attacks these challenges with a formal modelling and analysis approach built on top of GROOVE: a state-of-the-art model checker for graph-based semantics. Programs are automatically translated into input for the tool, which it analyses with respect to modular runtime models of the language. GROOVE’s powerful graph-based modelling formalism is able to model complex, high-level language behaviours as atomic steps (e.g. SCOOP’s simultaneous acquisition of multiple resources); is underpinned by algebraic theory, usable for soundness proofs (when formal semantics exist); and is inherently visual, thus easily checked by domain experts (when they don’t). Moreover, the modularity of our models allows them to adapt to change: alternative semantics of runtime components (e.g. the scheduler, memory handler, synchronisation handler) can simply be “plugged in” and the resulting execution traces compared. Ongoing work aims to address scalability through under- and over-approximation techniques, such as heuristic-guided approaches for counterexample finding, or model-to-model translations (e.g. to Petri nets) to benefit from other tools.
Leveraging Contracts for Safer Concurrency and Parallelism
A strategy for developing more reliable object-oriented programs is to annotate them with contracts: executable preconditions, postconditions, and class invariants, together specifying the properties that should hold before and after the execution of methods. In languages supporting contracts (e.g. Eiffel, D, Java with JML, C# with Code Contracts), these annotations can form the basis of various static and dynamic analyses, ranging from ones that require interaction and expertise (e.g. auto-active verification, abstract interpretation), to others that are fully automatic and require just the pushing of a button (e.g. runtime contract checking, automatic test case generation).
This is at least the case for sequential programs. When concurrency or parallelism is involved, such analyses are often limited, completely absent, or require substantially more expert-level annotations to generalise. With multi-threaded concurrency, for example, even the very simplest analysis for sequential programs—runtime contract checking—does not easily generalise due to the possibility of interference from other threads. Furthermore, concurrent and parallel programs have important correctness properties that sequential contract languages cannot express, such as temporal behaviours; or properties that cannot be efficiently checked, such as those of data-parallel algorithms operating on prohibitively large amounts of data.
In light of these challenges, our work aims to find new ways that contracts can be used to help ensure the correctness of concurrent and parallel applications, and currently has two distinct axes. First, we are investigating whether lightweight contracts can be leveraged by heuristic state-space exploration tools in order to find concurrency faults more effectively, in particular, by guiding the search to boundaries of contract satisfaction (see our position paper). Second, we are investigating the application of contracts to a new domain: general-purpose GPU programming for data-parallel algorithms. Our main contribution here is SafeGPU, a library-based approach for writing modular, contract-equipped GPU programs in an object-oriented language. The library generates and optimises low-level CUDA kernels automatically, and efficiently executes contracts on the GPU with little overhead—even for large amounts of data.
Some Side Projects
I occasionally dip my toes into interesting projects outside of the main research themes identified above. Here are a couple of recent examples:
- Faking Bidirectional Model Transformations—Mike Dodds, Richard Paige, Arend Rensink and I have been investigating bidirectional model transformations: solutions to the problem of maintaining consistency between two related and concurrently modified models. The inherent complexity that they must typically encode, however, means that they have limited support in practice (or support-with-caveats). We propose a practical, lightweight alternative to full bidirectional model transformations using the Epsilon platform, and a way in which consistency-preservation can still be proven. Here is a position paper about this early work.
- Formal Methods in Teaching—I am interested, firstly, in how formal methods themselves can be better taught; and secondly, in how (possibly lightweight) formal methods can be used to support the teaching of other concepts (e.g. programming, concurrency). Thus far, most effort has been expended on the first of these two angles through our annual Master’s course on Software Verification. We recently wrote up some general lessons learnt after using our auto-active verifier for Eiffel in the course’s take-home project, highlighting some key issues for educators and verification tool designers to address. See our paper.