Paper Accepted at F-IDE 2015

Standard

The AutoProof Verifier: Usability by Non-Experts and on Standard Code by Carlo A. Furia, myself, and Julian Tschannen was accepted for publication at the Formal Integrated Development Environment Workshop (F-IDE 2015).

Formal verification tools are often developed by experts for experts; as a result, their usability by programmers with little formal methods experience may be severely limited. In this paper, we discuss this general phenomenon with reference to AutoProof: a tool that can verify the full functional correctness of object-oriented software. In particular, we present our experiences of using AutoProof in two contrasting contexts representative of non-expert usage. First, we discuss its usability by students in a graduate course on software verification, who were tasked with verifying implementations of various sorting algorithms. Second, we evaluate its usability in verifying code developed for programming assignments of an undergraduate course. The first scenario represents usability by serious non-experts; the second represents usability on “standard code”, developed without full functional verification in mind. We report our experiences and lessons learnt, from which we derive some general suggestions for furthering the development of verification tools with respect to improving their usability.

Paper postprint (.pdf)

Paper postprint (.pdf)

Presentation slides (.pdf)

Presentation slides (.pdf)

Petri Nets and True Concurrency

Standard

One of the first keynotes I had the pleasure of listening to as a doctoral student was given by Javier Esparza at SPIN/ICGT 2010. As a joint (or rather, parallel) meeting of the model checking and graph transformation communities, his lecture – A False History of True Concurrency – presented the key insights and developments in the history of a research area that was interesting for both: the so-called unfolding approach to model checking.

Unfoldings are a mathematical formalism that give a truly concurrent semantics to a system; that is to say, a partial-order semantics that identifies immaterial orderings of events – orderings that would otherwise be forced in concurrency defined by interleaving. They were interesting for the SPIN community as a means to alleviate state space explosion; interesting too for those at ICGT, with the technique having an analogous use in automatically verifying graph grammars. As a fresh-faced doctoral student, I was fascinated by the theory and applications that the talk examined; although I never got a chance to explore them in my own work.

A Petri net unfolding

A Petri net unfolding

I was delighted however to be able to revisit some of these ideas in the concurrency course that I teach at ETH (jointly with Sebastian Nanz and Bertrand Meyer). The second half of the course has traditionally focused on formal models and process calculi for concurrency, but has never covered the important mathematical modelling language of Petri nets; an omission that this year we addressed. In addition to covering the intuition needed for constructing and interpreting Petri nets, we also used them as a vehicle to compare a semantics based on interleaving and a semantics based on true concurrency, applying the unfolding technique directly to nets and discussing the implications for automatic analysis. Though the lecture is only short, and omits many important details (such as how to search for an appropriate finite prefix), I hope that it still might serve as a useful gentle introduction to Petri nets and true concurrency; hence this post to share it!