Workshop Topic
Today’s software is large, complex, and error-prone. Although testing can help to detect errors, this is never sufficient to claim the delivered software is bug-free, and thus there remains the risk that errors will occur when the software is already in use. Program verification is a different technique to improve software quality: it allows one to mathematically prove properties about a program. Such formal verification techniques are challenging to develop and to use, but what they promise is highly valuable. During this symposium several novel program verification techniques will be presented, which have the potential to bring us much closer to reliable software.
Registration
The workshop is free of charge, including coffee, tea and lunch. Participants must register by sending an email to Ida Hamer (secr-fmt-ewi@utwente.nl).
Location
Room number 1333, Carre building, University of Twente
Drienerlolaan 5, 7522 NB
Enschede, The Netherlands
Schedule
| 09:00 | Reception/Welcome | |
| 09:30 | Bart Jacobs | Modular Termination Verification |
| 10:15 | Arend Rensink | Graph Transformation-Based Program Verification |
| 11:00 | Break | |
| 11:15 | Anton Wijs | Towards Formal Verification of Model-To-Model Transformations |
| 12:00 | Marina Zaharieva-Stojanovski | Verifying Functional Behaviour of Concurrent Programs |
| 12:45 | Closing | |
| 13:00 | Lunch |
Modular Termination Verification
Speaker: Bart Jacobs, University of Leuven, Belgium.
Abstract
We propose an approach for the modular specification and verification of total correctness properties of object-oriented programs. We start from an existing program logic for partial correctness based on separation logic and abstract predicate families. We extend it with call permissions qualified by an arbitrary ordinal number, and we define a specification style that properly hides implementation details, based on the ideas of using methods and bags of methods as ordinals, and exposing the bag of methods reachable from an object as an abstract predicate argument. These enable each method to abstractly request permission to call all methods reachable by it any finite number of times, and to delegate similar permissions to its callees. We illustrate the approach with several examples.
We then extend the approach to a concurrent setting, by incorporating an existing approach for verifying deadlock-freedom of channels and locks. Our main contribution here is to achieve information hiding by using method bags for lock ordering. We also show how our approach prevents infinite thread creation and enables verification of termination of fine-grained concurrent algorithms involving compare-and-swap loops.
We explain how our approach can be used also to verify liveness properties of non-terminating programs.
Graph Transformation-Based Program Verification
Speaker: Arend Rensink, University of Twente, The Netherlands.
Abstract
I will argue that graph transformation offer an excellent, insightful way to
specify programming language semantics, and gives rise to a very usable method
for program verification. I will illustrate the steps involved on the basis of a
toy language, using the graph transformation tool GROOVE.
Towards Formal Verification of Model-To-Model Transformations
Speaker: Anton Wijs, Eindhoven University of Technology, The Netherlands.
Abstract
I will present techniques to define behavioural transformations applicable on formal models of concurrent systems, reason about semantics preservation and the preservation of safety and liveness properties of such transformations, and apply them on models. Behavioural transformations allow to change the potential behaviour of systems. This is useful for model-driven development approaches, where systems are designed and created by first developing an abstract model, and iteratively refining this model until it is concrete enough to automatically generate source code from it. Properties that hold on the initial model and should remain valid throughout the development in later models can be maintained, by which the effort of verifying those properties over and over again is avoided. The approach has been implemented in a tool that integrates with the existing model checking toolsets mCRL2 and CADP, resulting in a complete model checking approach for model-driven system development.
Verifying Functional Behaviour of Concurrent Programs
Speaker: Marina Zaharieva-Stojanovski, University of Twente, The Netherlands.
Abstract
Modular verification of the functional behaviour of a concurrent program remains a challenge. We propose a new way to achieve this, using histories, modelled as process algebra terms, to keep track of local changes. When threads terminate or synchronise in some other way, local histories are combined into global histories, and by resolving the global histories, the reachable state properties can be determined. Our logic is an extension of permission-based separation logic, which supports expressive and intuitive specifications. We discuss soundness of the approach, and illustrate it on several examples.