Thorsten Bormer

Marc Brockschmidt

Dino Distefano

Gidon Ernst

Jean-Christophe Filliâtre

Radu Grigore

Marieke Huisman

Vladimir Klebanov

Claude Marché

Rosemary Monahan

Wojciech Mostowski

Nadia Polikarpova

Christoph Scheben

Gerhard Schellhorn

Bogdan Tofan

Julian Tschannen

Mattias Ulbrich

The COST IC0701 Verification Competition 2011 Extended Version ⋆

This paper reports on the experiences with the program verification competition held during the FoVeOOS conference in October 2011. There were 6 teams participating in this competition. We discuss the three different challenges that were posed and the solutions developed by the teams. We conclude with a discussion about the value of such competitions and lessons learned from them.

Introduction

A program verification competition was organized as part of the Formal Verification of Object-Oriented Software (FoVeOOS) conference held in Torino, Italy in October 2011. The conference was initiated by the COST Action IC0701, whose topic is advancing formal verification of object-oriented software. One of the tasks pursued by the Action is to set common goals and to develop common benchmarks for program verification tools. The competition aimed-in contrast to larger comparative case studies-to evaluate the usability of verification tools in a relatively controlled experiment that could be easily repeated by others.

The competition was organized by Marieke Huisman, University of Twente, Netherlands, Vladimir Klebanov, Karlsruhe Institute of Technology, Germany, and Rosemary Monahan, National University of Ireland Maynooth, Ireland. All three organizers have an extensive background in program specification and verification, and they have actively contributed to the development of different verification tools.

The competition was inspired by, and had a format similar to, the VSComp competition [START_REF] Klebanov | The 1st Verified Software Competition: Experience report[END_REF] held at VSTTE 2010: up to 3 people could form a team, all participants had to be physically present, and teams could use any verification system of their choice. The event took place the afternoon before the conference officially started. Challenges were given in natural language and required a solution that consisted of a formal specification and an implementation, where the specification was formally verified w.r.t. the implementation. In contrast to the VSComp event, a fixed time slot was assigned for each of the three challenges provided. This setup was chosen in order to increase precision of the tool comparisons.

The three different challenges were the following: (1) MaxElim: finding the maximum in an array by elimination, (2) TreeMax: finding the maximum in a tree, and (3) TwoEq: finding two duplets in an array. In addition, a fourth challenge (Cycle) was presented for teams to address outside the competition. This challenge was to determine if a given linked list contains a cycle. The challenges were chosen with the idea that they should be tough, but doable within the given time frames. Thorsten Bormer and Mattias Ulbrich, both Karlsruhe Institute of Technology, Germany, helped select and test the challenges.

For this report, participants were also given the possibility to improve their solutions. A record of all submitted solutions as well as an extended version of this report is available at the competition web site (see front page).

The remainder of this report is structured as follows. First the different teams and tools that participated in the competition are briefly introduced in Section 2. Then, Sections 3, 4, and 5 present the different challenges and the solutions provided by the different teams. Finally, Section 8 presents an overview of solutions submitted both during and after the competition, gathers most interesting observations and conclusions that were made by the organizers and participants, and makes some suggestions about running verification competitions in the future.

Participating Teams and Tools

The six participating teams used six different verification tools: the KeY system 1 [2], Dafny2 [START_REF] Leino | Dafny: An automatic program verifier for functional correctness[END_REF], KIV3 [START_REF] Reif | Structured specifications and interactive proofs with KIV[END_REF], jStar 4 [7], Why3 [START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF] (with the Krakatoa frontend [START_REF] Filliâtre | The Why/Krakatoa/Caduceus platform for deductive program verification[END_REF]), and AProVe [START_REF] Giesl | AProVE 1.2: Automatic termination proofs in the dependency pair framework[END_REF]. This section briefly describes these tools, and the background of the team members.

Team KeY The KeY system [START_REF]Verification of Object-Oriented Software: The KeY Approach[END_REF] is a highly automated, explicit-proof-object theorem prover for Java programs based on Dynamic Logic. Recently, the KeY system started its second life -the current development version is based on explicit heap representations and dynamic frames [START_REF] Kassios | Dynamic frames: Support for framing, dependencies and sharing without restrictions[END_REF][START_REF] Schmitt | Dynamic frames in Java dynamic logic[END_REF]. In this version of KeY, program specifications are written using JML* -a KeY-specific modification of JML to accommodate the idea of dynamic frames. This was the main version of the KeY system used in the competition, however, an older version of KeY based on static frames was also successfully used in solving the first challenge.

The KeY team consisted of two members: Wojciech Mostowski (postdoc at University of Twente) and Christoph Scheben (PhD student at Karlsruhe Institute of Technology). Mostowski is an active developer and user of the KeY system for the last 10 years. In particular, he implemented extensions to deal with Java Card peculiarities in the KeY logic and verified several realistically-sized case studies [START_REF] Mostowski | Formalisation and verification of Java Card security properties in Dynamic Logic[END_REF]. Scheben is a recently started PhD student developing the theory and extending the KeY system to reason about information flow properties in Java programs.

Team Dafny Dafny [START_REF] Leino | Dafny: An automatic program verifier for functional correctness[END_REF] is a programming language with built-in specification constructs. A Dafny program consists of classes, which contain variables and methods. Methods can be equipped with annotations in the form of pre-and postconditions, inline assertions, loop invariants and termination measures for loops and recursion. Specifications may contain user-defined recursive functions, as well as ghost variables and ghost code. Language features such as sets, sequences, and inductive data types are useful both in specifications and in executable code.

The Dafny verifier statically checks all user-supplied annotations, as well as memory safety properties (such as the absence of null dereferences or array accesses out of bounds), well-foundedness of recursive functions and termination of methods. The verifier is built on top of the Boogie [START_REF] Barnett | Boogie: A modular reusable verifier for object-oriented programs[END_REF] platform and works by generating verification conditions, which are discharged by a proof engine of choice, usually the SMT solver Z3 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF].

At the competition, the Dafny team consisted of two PhD students from ETH Zürich: Julian Tschannen and Nadia Polikarpova. Both team members are novice users of Dafny, however with extensive experience in other Boogie-based verification tools.

Team KIV KIV [START_REF] Reif | Structured specifications and interactive proofs with KIV[END_REF] is a tool for formal system development and interactive verification. It is based on many-sorted higher-order logic and structured algebraic specifications. KIV supports reasoning about programs written in two languages: 1) abstract programs that contain while loops, nondeterminism and recursive procedures, which operate on arbitrary algebraic data types, and 2) Java programs. The calculus is based on sequents and symbolic execution/wp-calculus for programs. KIV also implements a temporal logic.

KIV has a user-friendly interface with specification graphs and explicit proof trees. Proof automation is achieved by a set of heuristics (e.g., for quantifier instantiation) and efficient compiled rewriting.

Team KIV consisted of two PhD students -Gidon Ernst and Bogdan Tofan, who have both worked with the KIV tool for about two years -and Gerhard Schellhorn, who is one of the main developers of the tool, with many years of experience.

The solutions of the KIV team with full proofs are available online 5 .

Team jStar jStar is a verification tool based on separation logic that aims at verifying object-oriented programs written in Java. It verifies that programs meet specifications which are provided by the user in the form of method pre-and postconditions. Loop invariants are computed automatically by means of abstract interpretation. The jStar tool is geared towards reasoning about the heap and defers all other reasoning (such as arithmetic reasoning) to the SMT solver Z3.

The jStar tool is built on top of coreStar, a generic language-independent back-end intended for building verification tools based on separation logic. The two essential components that jStar brings together are: a theorem prover for separation logic which embeds an abstraction module for defining abstract interpretations; and a symbolic execution module for separation logic. Both of these components are tailored to object-oriented verification.

Reasoning about arrays was built into jStar only the day before the competition (and thus had not been thoroughly evaluated). As a result, the jStar team did not develop complete solutions to the challenges considering arrays -but used the experience from the competition to find out how they had to improve their support for arrays.

At the competition, the jStar team consisted of Dino Distefano and Radu Grigore from Queen Mary, University of London. Distefano has been working on the development of jStar since 2008, while Grigore is a postdoctoral research assistant working on the project since 2010.

Team Why/Krakatoa The Why platform [START_REF] Filliâtre | The Why/Krakatoa/Caduceus platform for deductive program verification[END_REF] is an environment for deductive program verification. It provides a rich specification language for modeling program behavior, and a verification condition generator. The verification conditions are passed to various backends (involving formula transformers/simplifiers, type encoders and pretty-printers) allowing a large set of automated or interactive external provers to be called. It also provides several front-ends to deal with input programs written in mainstream languages such as C (via the Jessie plugin of Frama-C [START_REF] Moy | The Jessie plugin for Deduction Verification in Frama-C -Tutorial and Reference Manual[END_REF]) and Java (with the Krakatoa front-end 6 ).

During the competition, the team used Why3 [START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF], the last major version of Why, and the Krakatoa front-end. The team had only one member, Claude Marché, INRIA Saclay and LRI, France. Marché is an active developer of the C and Java front-ends of Why and Why3 since 2004. Improved solutions were written after the competition together with J.-C. Filliâtre, and are available as part of the ProVal Web gallery of certified programs7 .

Team AProVe AProVE [START_REF] Giesl | AProVE 1.2: Automatic termination proofs in the dependency pair framework[END_REF] is a fully automated termination and complexity analysis system with front-ends for several programming languages such as Haskell, Prolog and Java. It builds upon the power of techniques developed for termination analysis of term rewriting systems (TRS) over the past 30 years by using a non-termination-preserving translation from the input problem to a TRS.

For the competition, the team used AProVE's Java frontend [START_REF] Brockschmidt | Modular termination proofs of recursive Java Bytecode programs by term rewriting[END_REF], which can also be accessed online 8 . The system currently only analyzes full programs, so each challenge solution needed to be accompanied by a routine to generate (random) inputs corresponding to the given pre-conditions. Please note that AProVE only proved termination properties for the presented examples.

The termination prover AProVE was used by Marc Brockschmidt, a PhD student working primarily on static analysis of Java programs in AProVE. Challenge: Verify that the index returned by the method max() given in Fig. 1 points to an element maximal in the array. Motivation: This challenge is an instance of Kaldewaij's Search by Elimination [START_REF] Kaldewaij | Programming: the derivation of algorithms[END_REF], where an element with a given property is located by eliminating elements that do not have that property. The challenge was selected as it involves a relatively simple but interesting invariant, expressing that the maximal element is in the remaining search space rather than maintaining the maximal element found so far. Results: Teams using tools that supported array data structures found the solution to this problem straightforward. Teams KeY, Dafny, KIV and Why/Krakatoa successfully specified and verified the pre-and postcondition of the max method. Not surprisingly, they stated that the input array has to contain at least one element, that the result index is within the bounds of the array, and finally, the top-level property that the result index in fact points to the greatest element. They successfully stated a loop invariant for the main while loop. The first part of the invariant is simple: it relates the search space bounds x and y and the bounds of the input array a. The second part of the loop invariant, concerned with maximality, was more difficult to express and verify. Fig. 2 gives an overview of this invariant part, showing quite some variations. Apart from the invariant, all teams have found the right termination measure yx.

Team KeY The KeY tools implements an improved rule for loop invariants [START_REF] Beckert | An improved rule for while loops in deductive program verification[END_REF], which requires a heap frame specification for the loop but allows one not to encode unchanged state in the invariant. This fact did not make a difference for the challenges of the competition, though.

One particular thing the KeY team found difficult to get right in the invariant was the disjunction of the two cases under each quantifier. The first intuition was that both conditions always hold. However, since it is difficult to establish in the loop invariant which of the two indices is changed by the loop, a disjunction, rather than a conjunction, is correct and at the same time sufficient to prove the final property. The KeY system proves this program fully correct (including integer overflow checks)9 in around 10 seconds.

Team Dafny The first challenge did not present any problems for the Dafny team. The initial solution was achieved in 25% of the allotted time. It contained five loop invariants, which were essentially a more verbose version of the revised solution that was developed after the competition. It also specified a termination measure through a decreases clause, which turned out to be redundant, as Dafny can infer simple termination measures automatically. Team KIV The solution of the KIV team models the underlying array data structure as an algebraic array, by actualizing the parameter type of arrays in the KIV library with natural numbers. Array indices are natural numbers too, rather than integers.

(\forall int i; i>=0 && i<=x; a[i]<=a[x] || a[i]<=a[y]) && (\forall int j; j>y && j<a.length; a[j]<=a[x] || a[j]<=a[y]); KeY invariant ∀ i • 0 ≤ i ≤ x =⇒ a [ i ] ≤ a [ x ] ∨ a [ i ] ≤ a [ y ]; invariant ∀ i • y ≤ i ≤ a . Length -1 =⇒ a [ i ] ≤ a [ x ] ∨ a [ i ] ≤ a [ y ]; Dafny original invariant ∀ i • 0 ≤ i < a . Length ∧ a [ i ] > a [ x ] ∧ a [ i ] > a [ y ] =⇒ x < i < y ; Dafny revised ∃k. x ≤ k ∧ k < y ∧ k < #ar ∧ ar [k] = max (ar ) KIV \forall integer i; 0 <= i < x || y < i < a.length ==> a[i] <= max(a[x],a[y]);
After some proof attempts, the team found that the invariant simply needs to state that the maximum of the full array is always at some position k between the search bounds. The proof requires user interaction to supply the invariant and to apply the two axioms required for the auxiliary function max .

After the competition, the team also solved this challenge using KIV's Java calculus [START_REF] Stenzel | A formally verified calculus for full Java Card[END_REF]. The program is encoded in compilable Java and the proof additionally shows that during execution of the program, no ArrayIndexOutOfBounds-Exception occurs. The proof structure is identical to the abstract proof, but formulas look slightly more complex, since additional information regarding type and heap access safety is necessary.

Team Why/Krakatoa The first challenge did not provide any difficulties for the Why/Krakatoa team. Around 15 minutes were enough to write the Why3 version and to prove it correct. Another 15 minutes were sufficient to transform it into a solution for the annotated Java code.

Team AProVe

To analyze the given problem, the AProVE team added a routine to create a random integer array. Then, AProVE could directly prove the resulting program to terminate in under 5 seconds. To achieve this, the max routine is automatically translated into a TRS with built-in integers [START_REF] Fuhs | Proving termination of integer term rewriting[END_REF] consisting of two rules (here simplified for presentation):

f(Array(l), x, y) → f(Array(l), x + 1, y) | x ≥ 0 ∧ y ≥ 0 ∧ y < l ∧ x < l ∧ x = y f(Array(l), x, y) → f(Array(l), x, y -1) | x ≥ 0 ∧ y ≥ 0 ∧ y < l ∧ x < l ∧ x = y
In term rewriting, a rule ℓ → r can be applied to a term t if there is a substitution σ such that ℓσ = t ′ for some subterm t ′ of t. Then the application of the rewrite rule results in a variant of t where the subterm t ′ is replaced by rσ.

For the example, the two generated rules closely match the two possible loop traversals. The first argument of f represents the input array, for which only the length l is encoded here. Termination is easily, and automatically, proven using a polynomial interpretation corresponding to the measure 2lx + y, which decreases in each rule.

Interestingly enough, the loop invariant x < y is not needed to show termination, as x and y are used as array indices and are thus implicitly bounded by 0 and the length of the array. You may represent empty trees as null references or as you consider appropriate. Motivation: The challenge was constructed by the organizers to explore how tools handle heap data structures that are not lists. The challenge, nonetheless, did admit a reasonably simple specification with an abstract sequence, map, or similar data type, as it did not involve properties such as the ordering of elements in a tree. Another aspect not tested was data structure mutation. Results: Within the time slot allocated during the competition, only the KIV team provided a full solution to the problem (and the AProVe team showed termination). However, after the competition, all teams worked out a solution to TreeMax.

Team KeY In KeY, the solution to TreeMax is based on dynamic frames [START_REF] Kassios | Dynamic frames: Support for framing, dependencies and sharing without restrictions[END_REF][START_REF] Schmitt | Dynamic frames in Java dynamic logic[END_REF]. Due to the linked structure of the tree and the recursive implementation of the max method, the KeY team chose to specify both the heap structure of the tree, and a flat representation of it. The heap structure definition states that trees cannot be cyclic, while the flat representation of the tree as a finite sequence of integers disallows infinite trees.

Figure 3 shows the relevant part of the resulting JML* specification. The heap structure is specified with the ghost field fp, which denotes the set of locations making up the footprint of the tree, and an invariant that structures this footprint correspondingly. The accessible clause provides a measure proving well-foundedness of the recursively defined invariant.

The integer payload of the tree is packed into a sequence in a natural way: the head of the sequence is the node of the tree, the left sub-tree follows, and then the right. The length of the sequence is the measure proving that the recursive call to the method max terminates.

What turned out to be the most challenging part of this task for the KeY team was the actual proof. The boundedness of the invariant and the structure of the footprint is proved automatically and very quickly. The first part of the top-level specification, a universal quantifier stating that the result is greater than or equal to all the elements in the tree is also quite straightforward. Up to this point, the KeY system finds all proofs automatically and within one minute. However, the system has difficulty with the second main property: the existential quantifier that states the presence of the result in the tree. In the automated proof search mode the proof starts to grow uncontrollably regardless of the prover settings used. In the end, substantial manual interaction was required to guide the prover through the important cases (left and right sub-trees being null or not) and to give it the right instantiations for the existential quantifier. This manual interaction with the prover (over 200 interactions in total) was where most of the time was spent on this challenge. The rest of the proof was done automatically and took less than a minute to finish.

public
Team Dafny Memory footprints of linked data structures are commonly described in Dafny using dynamic frames [START_REF] Kassios | Dynamic frames: Support for framing, dependencies and sharing without restrictions[END_REF]. According to this idiom, the Tree class is extended with a ghost field Repr, which stores the set of all nodes in the subtree with root this (Listing 1.1). The ghost field serves multiple purposes: on the one hand, it is used to describe footprints of functions and methods, thus taking care of the frame problem; on the other hand, it serves as a termination measure for any recursion on subtrees. For the latter use, the data structure is required to be acyclic. Dafny does not support class invariants, where the acyclicity property could be stated. Class invariants are simulated by defining a predicate valid, and using it in pre-and postconditions of class methods. To facilitate functional specifications, another ghost field Values is defined to denote the set of all values stored in the subtree. Using this field, it is easy to specify that method max returns a value from the tree that is larger than all other values. A straightforward recursive implementation for max was provided; the only auxiliary annotation needed to verify this implementation was the termination measure.

In the rush of the competition the Dafny team forgot to specify that the return value must be present in the tree. The team added the omitted piece of specification in the final version, and Dafny was able to verify it without any further modifications. The final version also contains a constructor: a method that establishes the valid predicate without requiring it. Adding such a method to any class is important in order to ensure consistency of the class invariant.

Team KIV The difficult task in the second challenge is to specify a proper tree structure within a heap H. The KIV team used a lightweight embedding of separation logic into HOL. This is part of the KIV library. The embedding encodes heap assertions as heap predicates of type heap → bool. It contains a straightforward specification of binary trees in the heap, using a recursive function tr : ref × tree → (heap → bool). The heap predicate tr(r, t) states that pointer r is the root of a binary heap tree that corresponds to an algebraic tree t. Algebraic trees are a free data type with two constructors: leaf and branch(t 0 , a, t 1 ). Predicate tr is specified as tr(r, leaf)(H) ↔ emp(H) ∧ (r = null) tr(r, branch(t 0 , a, t 1 ))(H) ↔ ∃ r 0 , r 1 . (r → node(r 0 , a, r 1 ) * tr(r 0 , t 0 ) * tr(r 1 , t 1 ))(H)

Predicate emp is true for the empty heap only, and maplet r → node(r 0 , a, r 1 ) defines a singleton heap consisting of exactly one node at address r, which holds an element a (actualized with integers in the following) and pointers r 0 and r 1 to the left and right subtree respectively. Crucially, separation logic's star operator * enforces that each tree node resides in a different part of the heap, which ensures the tree shape of the heap structure. With these preliminaries, total correctness of a recursive procedure MAX(r; i, H) was proven. This procedure returns the maximum value of the tree stored under reference r, in output variable i (the semicolon separates input parameters from reference/output parameters). The proof obligation is:

r = null ∧ (tr(r,t) * p)(H) → |MAX(r; i,H)| ((tr(r,t) * p)(H) ∧ i = max(t))
In the formula, |α| ϕ is KIV notation for the weakest precondition wp(α, ϕ) of program α for postcondition ϕ. Therefore, the goal asserts that all executions of MAX terminate without changing the input tree and that i stores max(t) at the end. The maximum function max(t) was defined by structural recursion over the algebraic tree. Predicate p is a universally quantified predicate variable allowing an abstraction from everything else on the heap beyond the tree structure (p can, e.g., be instantiated with the empty heap emp). Thus, the generalized goal is directly provable by induction over the size of t. When applying the induction hypothesis for the right (left) subtree, p is instantiated with the original p plus the root cell plus the left (right) subtree. KIV's heuristic applies one instance of the induction hypothesis automatically, the second instance has to be given manually. The proof is simple and has six interactive steps out of 39 steps in total.

Team jStar The implementation from the jStar team consists of one class whose fields are final, private, and initialized by the constructor. The method max is coded as follows:

int max() { int r = value; if (left != null && left.max() > r) r = left.max(); if (right != null && right.max() > r) r = right.max(); return r; }
The main objective of the specification is to keep track of the maximum of each tree. The predicate Tree(t, {max = m}) denotes that the Java reference t points to a tree whose maximum value is m.

Tree(t, {max = m}) ⇐⇒ (t = nil ∧ m = 0) ∨ (t = nil ∧ NonEmptyTree(t, {max = m})) (1)
NonEmptyTree(t, {max = m}) ⇐⇒ ∃ l lm r rm v, t left -→ l * t right -→ r * t value -→ v * Tree(l, {max = lm}) * Tree(r, {max = rm}) * m = max(v, max(lm, rm)) * v ≥ 0 (2)
In general, one can associate abstract records with objects. In this case, the record has exactly one field, max. Verification is easier if one assumes a lower bound on possible values. In this case, the bound 0 was chosen, but also the smallest representable integer could have been chosen. Background axioms specify the function max.

∀ x y, x ≥ y ⇒ max(x, y) = x (3) ∀ x y, x ≥ y ⇒ max(y, x) = x (4)
Given this setup, jStar verifies the following specifications.

{ v ≥ 0 * Tree(l, {max = lm ′ }) * Tree(r, {max = rm ′ }) } init (v, l, r) { NonEmptyTree(this, {max = max(v, max(lm ′ , rm ′ ))}) } (5) { NonEmptyTree(this, {max = m ′ }) } max() { NonEmptyTree(this, {max = m ′ }) * return = m ′ } (6)
Specification [START_REF] Brockschmidt | Modular termination proofs of recursive Java Bytecode programs by term rewriting[END_REF] ensures that the constructor preserves absence of sharing and value non-negativity when building the tree. More importantly, it keeps track of the maximum value for each tree that is constructed in the program. Specification [START_REF] De Moura | Z3: An efficient SMT solver[END_REF] ensures that the tree remains allocated and that the returned value is indeed the maximum reachable.

During the competition the jStar team was only able to verify [START_REF] Brockschmidt | Modular termination proofs of recursive Java Bytecode programs by term rewriting[END_REF]. After the competition, the team were also able to verify [START_REF] De Moura | Z3: An efficient SMT solver[END_REF]. This could not be proved during the competition as, at that time, jStar could not send extra axioms to Z3, such as the ones for max (3) and ( 4), which are necessary to prove (6).

Team Why/Krakatoa For the Why/Krakatoa team, the tree data structure made the second challenge significantly difficult. As a first step, proving a Why3 version of the problem was very useful, since such a data structure can be defined using an algebraic datatype, as follows:

type tree = Null | Tree int tree tree Predicates for testing membership of a value v in a tree and for checking if a value is greater than or equal to all elements of a tree, can be defined recursively: The postconditions declare that the result is greater than or equal to all the elements of the given tree. This is incomplete, since it is also necessary to express that the result is itself an element of the tree. This is indeed easy to specify using the predicate mem. However, during the competition the team made a mistake, and used conjunctions instead of disjunctions in the definition of mem, thus failing to prove correctness of the fully specified program. The solution presented here is the one that the team developed during the competition. The ProVal gallery provides a different solution that is both simpler (without auxiliary functions) and complete (with a postcondition that the result appears in the tree).

To prove correctness of max_aux's postcondition, the team used the following lemma: lemma trans: forall t:tree, x y:int.x >= y /\ ge tree y t -> ge tree x t Verification conditions are all proved, using a combination of provers, including the interactive prover Coq for the above lemma. Table 1, generated by the Why3 report tool, give the details of which prover proved which VC. Notice that the proof of the postcondition of the auxiliary subprograms was a conjunction and was split in two. The Coq proof script is a few lines long and proceeds by induction over the tree structure.

The ProVal gallery also provides solutions in Java and C. In these cases, complex predicates must be defined in order to specify that the given tree is well-formed, i.e., is a finite tree properly terminated with null pointers as leaves. However, there is no need to specify that there is no sharing in the subtrees: a recursive traversal for finding the maximum is also correct in the case of sharing.

Team AProVe Again, the AProVE team first added a routine to randomly create a tree. Then, AProVE could automatically translate the max method public int max() { int lM = -2147483648; int rM = -2147483648; if (this.left != null) lM = this.left.max(); if (this.right != null) rM = this.right.max(); return max(this.value, max(lM, rM)); } into a TRS. Next, integer comparisons that are not relevant for termination are automatically filtered out, leaving only rules of the form f(Tree(l, r)) → f(l) and f(Tree(l, r)) → f(r). These can easily be proven to terminate, as the size of the considered tree decreases strictly in each step. The fully automatic termination proof takes about 15 seconds, where a majority of the time is spent on proving termination of the routine generating a random tree.

Challenge 3: Finding Two Duplets in an Array

Time: 90 minutes Given: An integer array a of length n + 2 with n ≥ 2. It is known that at least two values stored in the array appear twice (i.e., there are at least two duplets). Challenge: Implement and verify a program that finds two such values. You may assume that the array contains values between 0 and n -1. Motivation: This challenge is a popular "job interview-style" question, but we are not aware of its origin. The challenge was selected as it requires complicated array reasoning, specifications, and invariants. Results: Most teams solved this problem within or shortly after the deadline for the competition. The KeY team provided a complete solution after the competition finished but before the end of the conference.

Team KeY

The key point in the solution of this challenge is to be able to specify the number of occurrences of a value in the array (and reason about it). In JML, this can be done with the help of the \sum operator, a special quantifier that provides an arithmetic sum over the quantified elements. In the KeY system the sum operator is currently limited to quantify only over a single continuous range of an (integer) array.

First, the team defined a method to count the number of occurrences of a given value in the array with the following simple specification: //@ ensures \result == //@ (\sum int i; 0<=i && i<a.length; a[i] == value ? 1 : 0); static int /*@ pure @*/ countAcc(int[] a, int value) {...}

The implementation of the method uses a simple loop annotated with appropriate JML specifications to count the occurrences. KeY proves this method correct automatically within a few seconds.

The team then used this method to both implement and specify the top-level method that finds the two values that are each duplicated in the array. The solution was developed for a slightly more general case, where it was not assumed that the values in the array are all between 0 and n -1. Instead, only the existence of two pairs of duplicates from an arbitrary range of values smin..smax (smin+1<smax) is required by the precondition of the top-level method. Weakening this assumptions allows one to carry around less information through all other annotations (loop invariants). This not only makes the specifications more elegant but also makes the correctness proof easier for the tool to complete.

The implementation of the top-level method is different from that of other teams in that it iterates over all potential array values (given a priori by the smin..smax range) and not over the array elements. For each potential value, it calls countAcc to get the count of the value's occurrences, and terminates once a second duplicated value has been found. The most difficult part is expressing the invariant for the iteration loop. It makes a case distinction over how many duplicate values have been found so far and specifies a corresponding condition about the elements yet-to-be found. The proof for the top-level method requires some minor interactions (more or less obvious quantifier instantiations), while the rest is done automatically within 10 seconds.

Team Dafny

The main difficulty of the third challenge was to express the precondition that the array has at least two duplicate pairs, and to get the verifier to make use of this fact so that it concludes that the program always succeeds. The team went for a functional approach to specification and formulated the precondition as follows: the array has a duplicate pair, and if that pair is removed from the array, it still has a duplicate pair (Listing 1.2). To this end, recursive functions has duplicates and first duplicate are defined on sequences. method find_two_duplicates ( a : seq < int >) returns ( x : int , y : int ) requires has_duplicates ( a ); requires has_duplicates ( removed (a , first_duplicate ( a ))); ensures occurrences (a , x ) > 1; ensures occurrences (a , y ) > 1; ensures x = y ; { . . . } Listing 1.2. Dafny specification of the main method in Challenge 3

For the reason of time constraints, the team decided to write the implementation in terms of these functions as well. Dafny makes this possible through a construct called function method : a recursive function that must be free of specification-only constructs and thus can be used in executable code.

Note that the implementation uses sequences instead of arrays, because the former are easier for Dafny to reason about. In the opinion of the team, this is not a limitation, as the implementation is still executable.

The postcondition of the program is expressed more abstractly: through the number of occurrences of both results in the initial sequence. To make the program verify, three inductive lemmas were needed. Those lemmas connect the number of occurrences of an element in a sequence to the notions membership, duplicates and removal from a sequence, respectively.

Team KIV The KIV team first understood (incorrectly) that the task was to compute two indices m, n with a duplicate element in the array (ar[m] = ar[n]). Therefore, the total correctness of an algorithm FINDDUP(ar; m, n) that finds such a pair of indices was proved initially.

The algorithm uses two nested loops to find the right positions. The outer loop runs through the array using an index m. The inner loop sets done to true if it finds an index n > m with a duplicate. The invariant of the outer loop asserts that no duplicate exists below m, and that the done flag of the inner loop indicates ar[m] = ar[n]. To verify the inner loop, the precondition is generalized (weakened) from n = m + 1 to "no duplicate for ar[m] below n". Then well-founded induction over #arn and symbolic execution of one inner loop body is sufficient to finish the proof.

After verifying this algorithm, the team realized that the intended task was rather to verify an algorithm that computes two duplicate values of the input array. Fortunately, both the first implementation and its correctness proof could be reused to come up with the right solution.

A second procedure FINDDUPSND(ar, k; m, n) was then defined, which gets an additional input value k and computes the indices m, n of a duplicate value different from ar[k]. The program and the proof for this second algorithm are almost identical to the first. The final theorem that solves the challenge then just combines the two results to prove that executing both procedures sequentially finds the two required duplicates.

Team Why/Krakatoa The solution that the Why/Krakatoa team implemented during the competition first defines an auxiliary function that given an array a and an optional value o, returns the two indexes of a duplet in a whose value differs from o (if any). The main program first calls the auxiliary program without the optional argument o, and then calls it a second time with the argument o initialized to the value found during the first call. The solution is correct whatever the values stored in the array (they do not have to be between 0 and n -1).

The code is too large to be presented here; it is found in the ProVal gallery. The code for the auxiliary program consists of two nested loops and is not intended to be computationally optimal. Suitable loop invariants can be found without major difficulty. The proofs are obtained using automatic provers. During the competition, the fully proved Why3 program was obtained in around 60 minutes. Java and C versions, as well as an alternative solution in Why3, were implemented after the competition.

Team AProVe The AProVE team solved the problem by enumerating all pairs of values of the array using two nested loops (using counters i and j bounded by the array length) and then searching for duplets. AProVE could translate the method to rules of the form f(Array(l), i, j) → f(Array(l), i + 1, i + 2) | l ≤ j ∧ l > i + 1 and f(Array(l), i, j) → f(Array(l), i, j + 1) | l > j ∧ l > i. The second rule corresponds to one iteration in the inner loop, in which j is incremented while it is smaller than the array size. The first rule corresponds to the case that the counter j of the inner loop has reached its bound. The rule then encodes that i is incremented, j is reset to i + 1 and then a first iteration of the inner loop is performed. Termination of the generated TRS can be proven easily and automatically. Challenge: Implement and verify the method cyclic() to return true when the data structure is cyclic (i.e., this Node can be reached by following next links) and false when it is not.

Team KIV We have solved the fourth challenge (cycle detection), by verifying Floyd's and Brent's standard algorithms for cycle detection adapted to heap structures (see the web presentation [START_REF]KIV web site[END_REF] for the actual algorithms). Both proofs are rather tricky. They are based on the following definition of a cyclic heap structure. A cycle is reachable from a start location r in a heap H following next references iff some reference r 0 can be reached from r on paths with different length m and n respectively. cyclic(r, H) ≡ ∃ m,n,r 0 . m < n ∧ reach(H,m,r,r 0 ) ∧ reach(H,n,r,r 0 ) Both proofs have two cases: the case where a cycle exists, and the case where the structure is linear. The total correctness proof for both non-cyclic cases induces over the difference of the length of the list minus the number of steps of the faster pointer. Floyd's algorithm needs well-founded induction since it decreases by two in every iteration. For the cyclic case we first derive two equivalent characterizations of cyclicity, which are needed to show termination of the algorithms. For Floyd's algorithm we need that cyclicity is equivalent to ∃ n, r 0 . n = 0 ∧ reach(H,n,r,r 0 ) ∧ reach(H,n + n,r,r 0 ) A pointer r 0 exists, that is reachable in both n and 2n steps. In Floyd's algorithm, the distance to n decreases. For Brent's algorithm, it is crucial that the slower pointer always points to a reference, that is reachable from r in 2 n -1 steps (this was the hard part to figure out). Therefore, we need the following characterization of cyclicity:

∃ n, m, r 0 . m = 0 ∧ m ≤ 2 n ∧ reach(H,2 n -1,r,r 0 ) ∧ reach(H,m,r 0 ,r 0 )
A pointer is reachable in 2 n -1 steps, where a cycle with at most 2 n elements starts. The termination argument is that 2 n -1 + m minus the steps of the faster pointer decreases by one in each loop iteration.

Since the variants of both proofs require existentially quantified variables from the invariant, the proof does not work by simply applying the invariant rule. Instead, we generalize the precondition to the invariant (the existential quantifier can be dropped) and then use structural induction. The proof proceeds by exiting the loop in the base case. For the recursive case, the loop is symbolically executed once, then the induction hypothesis is applied. The proof is moderately complex with 86 interactions. This number could be further reduced.

Team jStar Our implementation is the following.

and jStar verifies the following specifications.

{ this next -→ x ′ * ls(x ′ , nil) } • • • { ¬return } (8) { this next -→ x ′ * ls(x ′ , this) } • • • { return } (9)
Note that there are three kinds of list shapes, I-lists, o-lists, and ρ-lists. Strictly speaking, the task asks for a method that returns true for o-lists and false for all others. Our specification ensures that the result is true for o-lists, false for I-lists, and that the method can never be called on ρ-lists.

The loop invariant is inferred in each case by a very simple abstraction that is built in jStar. If the current state is P * Q and state P was already seen, then P * Q is abstracted to P . This abstraction is sound in intuitionistic separation logic, but not in the classical version. The invariant is

∃ x ′ , this next -→ x ′ * ls(n, z), ( 10
)
where z is nil for [START_REF] Filliâtre | The Why/Krakatoa/Caduceus platform for deductive program verification[END_REF], and this for [START_REF] Fuhs | Proving termination of integer term rewriting[END_REF] During the competition we did not look at this last task.

Team Why/Krakatoa The fourth and extra problem of the competition has been solved using Why3 after the competition, see http://proval.lri.fr/ gallery/tortoise_and_hare.en.html.

Solution Verbosity Statistics

Verbosity metrics were collected with a Perl script initially released in connection with [START_REF] Leino | VACID-0: Verification of ample correctness of invariants of data-structures[END_REF]. The script tokenizes the input, taking into account the lexical conventions of C-derived programming and specification languages. The tokens are assigned to one of the above categories according to the mark-up inserted into the files by solution authors. The results of the measurement are given in Table 2. The script and the marked-up solutions are available on the competition web site.

Wrap-up, Conclusions and Future Competitions

Solution Overview This report discusses the three challenges and the solutions developed during the verification competition organized as part of the FoVeOOS conference in October 2011. Figure 4 summarizes the outcome of the competition.

The "revised" column of Figure 4 also records solutions to the 4th, "takehome" challenge (Cycle), which is mentioned in the introduction. After the competition, the teams Dafny, KIV and Why/Krakatoa submitted solutions for this challenge 10 .

One of the main developers of Dafny, Rustan Leino, has also attempted the challenges, out of competition. He reported that the first three caused him no particular problems (spending approximately 20, 40 and 90 minutes on them, respectively). Studying the solution of the Why/Krakatoa team to TreeMax inspired him to simplify his own. Leino also solved Cycle in about 8 hours. His solutions are now available as part of the Dafny test suite. We encourage others in the verification community to try the challenges and report back to the competition organizers.

The solutions to Cycle submitted by team KIV, team Why, and by Leino verify the efficient "tortoise and hare" algorithm (attributed by Knuth to Floyd). Team KIV also verified Brent's algorithm, which is another efficient cycle detection method. Participants' Observations All teams reported that participating in the competition had been a positive experience and an incentive to continue development of the tools. Taking part in the competition allowed them to get a good overview of the power and usability of verification systems other than the ones with which they were most familiar. Also, because of the requirement to be physically present, the competition provided a good opportunity to interact with developers of competing tools.

During the competition several teams realized the importance of obtaining good feedback from the tool, both upon syntax and specification errors, as well as on failed proof attempts. Developing the solutions under a certain time pressure made these requirements much more obvious than usual.

For the jStar team, the competition gave a clear indication on parts of the tool that had to be improved: jStar's libraries are very basic, and the support for arrays has to be developed further, as the current implementation seems to have some unwanted interactions with Z3.

For the AProVE team, the challenges addressed during the competition were atypical (AProVE usually addresses more complex termination problems). However, the experience of the competition inspired the team to explore how AProVE's fully automated nature might be used to find termination measures that are usable for other tools.

Organizers' Observations

The organizers observed the importance of gathering a bank of challenges well in advance of the competition so that they could be evaluated with respect to their difficulty and their suitability for a wide selection of verification tools. This evaluation was particularly important when determining the length of time to allocate to each challenge.

With respect to the solutions submitted to each of the challenges, the organizers were surprised at the variation of loop invariants used in MaxElim and were interested to see that most teams completed the challenge in less than three quarters of the allotted time. TreeMax brought greater difficulty to teams, with user interaction required by many of the tools and only one team achieving a solution within the allotted time. This re-affirmed the suspicion that verification of programs involving linked data structures is still not a straightforward task for many verification tools. In TwoEq, it was no surprise that most teams divided the challenge into subproblems and took advantage of their tool's support for modular verification to compose the overall solution.

When evaluating the different solutions, the organizers observed that expert non-users of tools can understand the solutions. However, they also observed the importance and the difficulty of communicating program verification proofs. Most tools try to do something in this respect: Why3 supports the user in producing a L A T E X report with key lemmas and some statistics; KIV can process proofs for browsing on the web, however the proofs could be more informative; KeY offers a nicely annotated proof tree, but in the tool only; and Dafny has a very clean annotation syntax 11 . All these aspects help to make the understanding of the proof easier. However, it would be a worthwhile exercise for tool developers to come together to combine and extend the different approaches.

The competition also made it clear that certain tool features help to specify programs and construct proofs. For example, both KIV and Why3 can define and reason easily about arbitrary ADTs, while Dafny has very good built-in support for sets and sequences. However, it is evident that techniques such as systematic refinement between abstract and implemented data types, and invariant generation are not yet adopted in mainstream program verification tools.

Design of Future Verification Competitions

The competition also provided some further ideas about the format of future verification competitions. Unsurprisingly, the outcome of this kind of verification competition depends heavily on the ability and experience of the human proof engineer(s). While this cannot be avoided completely, it is helpful (a) trying to balance the experience and skills between teams, (b) encouraging participation of several teams with the same tool, and (c) trying to attract non-developer teams. On the other hand, it needs to be stressed that tool performance must be measured in terms of usability and not just raw deduction power alone. A suggestion that we consider worth investigating is to record the participants as they interact with their tools and later collect their comments on the solution-finding process.

The teams and the organizers appreciated that dedicated time slots were given to challenges. Teams felt that this forced them to work on the problems together, which was beneficial, because sharing ideas reduces the probability of getting stuck on a wrong path. Moreover, it also gives the possibility to pursue two alternative approaches to the same problem in parallel, when one is not sure which one will work.

One of the risks of a verification competition is that the choice of challenges favors a particular tool or approach (in fact, the Dafny team remarked that the challenges did not address modifying the state of complex data structures, which are more difficult to handle in Dafny). An alternative format that would address this issue, would be to ask that each participating team contribute a challenge that they can handle well, and that they believe might be a challenge for the other participants. This would ensure that each team could submit at least one solution to a challenge, and these solutions would provide a good benchmark with which to compare other team solutions.

We conclude that program verification tools are mature enough now to have verification competitions. However, because of the more open nature of program verification problems, and the importance of the experience of the team members, it will be complicated to standardize such a competition. Instead, we believe that it is worth investigating different formats. As the tools will develop further, also verification competitions will develop further.

3 Challenge 1 :Fig. 1 .

 11 Fig. 1. Search by eliminationTime: 60 minutes Given: A non-empty integer array a. Challenge: Verify that the index returned by the method max() given in Fig.1points to an element maximal in the array. Motivation: This challenge is an instance of Kaldewaij's Search by Elimination[START_REF] Kaldewaij | Programming: the derivation of algorithms[END_REF], where an element with a given property is located by eliminating elements that do not have that property. The challenge was selected as it involves a relatively simple but interesting invariant, expressing that the maximal element is in the remaining search space rather than maintaining the maximal element found so far. Results: Teams using tools that supported array data structures found the solution to this problem straightforward. Teams KeY, Dafny, KIV and Why/Krakatoa successfully specified and verified the pre-and postcondition of the max method. Not surprisingly, they stated that the input array has to contain at least one element, that the result index is within the bounds of the array, and finally, the top-level property that the result index in fact points to the greatest element. They successfully stated a loop invariant for the main while loop. The first part of the invariant is simple: it relates the search space bounds x and y and the bounds of the input array a. The second part of the loop invariant, concerned

Why

Fig. 2 .

 2 Fig. 2. Invariants for MaxElim (relevant parts)

4 Challenge 2 :

 2 Finding the Maximum in a TreeTime: 90 minutes Given: A non-empty binary tree, where every node carries an integer. Challenge: Implement and verify a program that computes the maximum of the values in the tree. Base your program on the following data structure signature: public class Tree { int value; Tree left; Tree right; }

  predicate mem (v:int) (t:tree) = match t with | Null -> false | Tree x l r -> x=v \/ mem v l \/ mem v r predicate ge tree (v:int) (t:tree) = match t with | Null -> true | Tree x l r -> v >= x /\ ge tree v l /\ ge tree v rGiven this model of trees, one can provide annotated code for the problem. The team decided to code an auxiliary subprogram, having an accumulator as an

6 Challenge 4 :

 4 Deciding Cyclicity of a ListGiven: A Java linked data structure with the signature public class Node { Node next; public boolean cyclic() { //... } }

  boolean isCyclic() { Node n = next; while (n != this && n != null) n = n.next; return n == this; } We define the list segment predicate as usual ls(x , z ) ⇐⇒ x = z ∨ (∃ y, x next -→ y * ls(y, z))

Fig. 4 .

 4 Fig. 4. Solution overview

  class Tree { private int value; private /*@ nullable @*/ Tree left, right; Fig. 3. The KeY team's solution for TreeMax (excerpt)

	/*@ ghost \locset fp; invariant fp ==
	\set_union(this.*, \set_union(
	left==null? \empty : \set_union(left.*,left.fp),
	right==null? \empty : \set_union(right.*,right.fp)));
	invariant left != null ==>
	(\disjoint (this.*, left.fp) && left.\inv);
	...
	ghost \seq seq; invariant seq ==
	\seq_concat(\seq_singleton(value), \seq_concat(
	left==null? \seq_empty : left.seq,
	right==null? \seq_empty : right.seq));
	accessible \inv : fp \measured_by seq.length; @*/

Table 1 .

 1 Problem 2 in Why3: Proof summary extra argument, to take care of empty trees:

	Proof obligations	Alt-Ergo 0.93	Coq 8.2pl1	CVC3 2.2	Z3 2.19
	ge trans		0.44
	parameter max aux
	1	0.06		0.02 0.05
	2	0.03		--
	parameter max	0.03		-0.07
			let max (t : tree) =
	{ true }			{ t <> Null }
	match t with			match t with
	| Null -> acc			| Null -> absurd
	| Tree v l r -> max aux			| Tree v l r ->
	l (max aux r (MinMax.max v acc))		max aux l (max aux r v)
	end			end
	{ ge tree result t /\ result >= acc }		{ ge tree result t }

let rec max aux (t : tree) (acc : int) =

Table 2 .

 2 Solution verbosity metrics

	Team				Solution verbosity (tokens)
				code / requirement annotations / aux annotations
		MaxElim	TreeMax	TwoEq			Cycle
	Dafny	68	43 49	93	72	68	153 149 244	-	-	-
	KeY	61	62 93	103 246 109 +	134 232 368 +	-	-	-
	KIV	44 207 42 +	110 402	0 +	201 463	0 +	231 243 816 +
	"+" indicates additional non-textual user interaction.

⋆ The floor brackets mark parts not present in the short version. This text was last updated on February 19, 2013.

http://www.key-project.org

http://research.microsoft.com/projects/dafny/

http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/kiv/

http://www.jstarverifier.org

http://www.informatik.uni-augsburg.de/swt/projects/ cost-competition-2011/

http://krakatoa.lri.fr

http://proval.lri.fr/gallery/cost11comp.en.html

The overflow checking option of the KeY system was only used in this task to show that this is possible. Overflow checks are skipped in the rest.

Available in the extended version of this paper.

Acknowledgements

The competition received generous supported from COST Action IC0701. Huisman and Mostowski are partially supported by ERC grant 258405 for the VerCors project. Mostowski is partially supported by Artemis grant 2008-100039 for the CHARTER project.


Jean-Christophe Filliâtre

Andrei Paskevich

Why3 -Where Programs Meet Provers

We present Why3, a tool for deductive program verification, and WhyML, its programming and specification language. WhyML is a first-order language with polymorphic types, pattern matching, and inductive predicates. Programs can make use of record types with mutable fields, type invariants, and ghost code. Verification conditions are discharged by Why3 with the help of various existing automated and interactive theorem provers. To keep verification conditions tractable and comprehensible, WhyML imposes a static control of aliases that obviates the use of a memory model. A user can write WhyML programs directly and get correct-by-construction OCaml programs via an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. We demonstrate the benefits of Why3 and WhyML on nontrivial examples of program verification.

Introduction

Why3 is a platform for deductive program verification [START_REF]Why3, a tool for deductive program verification[END_REF]. It provides a rich language of specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. The tool comes with a standard library of logical theories (integer and real arithmetic, sets and maps, etc.) and of basic programming data structures. WhyML is used as an intermediate language for the verification of C, Java, or Ada programs [START_REF] Guitton | Why Hi-Lite Ada?[END_REF], in a similar fashion to the Boogie language [START_REF] Barnett | Boogie: A Modular Reusable Verifier for Object-Oriented Programs[END_REF]. Besides, WhyML strives to be comfortable as a primary programming language and inherits numerous high-level features from ML, listed below.

The specification component of WhyML, used to write program annotations and background logical theories, is presented in [START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF], and here we only mention the most essential features. Why3 is based on first-order logic with rank-1 polymorphic types and several extensions: recursive definitions, algebraic data types, and (co-)inductive predicates. Pattern matching, let-expressions, and conditional expressions are allowed both in terms and in formulas. A type, a function, or a predicate can be given a definition or just declared as abstract symbols and then axiomatized. The specification language of Why3 does not depend on any features of the programming language, and can serve as a rich common format for theorem proving problems, readily suitable (via Why3) for multiple automated and interactive provers, such as Alt-Ergo, CVC3, Z3, E, SPASS, Vampire, Coq, or PVS. When a proof obligation is dispatched to a prover that does not support some language features, Why3 applies a series of encoding transformations to, for example, eliminate pattern matching or polymorphic types [START_REF] Bobot | Expressing Polymorphic Types in a Many-Sorted Language[END_REF].

Programming Language

WhyML can be seen as an ML dialect, with two important restrictions. Firstly, in order to generate first-order proof obligations, WhyML is also limited to the first order: Nested function definitions and partial application are supported, but higher-order functions are not. Secondly, in order to keep proof obligations more tractable for provers and more readable (hence debuggable) for users, WhyML uses no memory model and imposes a static control of aliases instead. Every l-value in a program must have a finite set of names and all these names must be known statically, at the time of generation of verification conditions. In particular, recursive data types cannot have mutable components. This restriction is not as limiting as it may seem, and we show in the next section that it does not preclude us from writing and verifying complex algorithms and data structures.

WhyML functions are annotated with pre-and post-conditions for normal and exceptional termination, and WhyML loops are annotated with invariants. Recursive functions and while-loops can be given variants (i.e. values that decrease at each recursive call or iteration) to ensure termination. Statically checked assertions can be inserted at arbitrary points in a program. Verification conditions are generated using a standard weakestprecondition procedure. Every pure type, function or predicate introduced in the logical component can be used in a WhyML program. For instance, the type of integers and basic arithmetic operations are shared between specifications and programs.

The mutable state of a computation is embodied in mutable fields of record data types. Mutable data types can be nested. For example, a polymorphic resizable array can be modeled by a record with a mutable field containing an ordinary fixed-size array:

type rarray 'a = { mutable data: array 'a; mutable size: int } invariant { 0 ≤ size ≤ data.length }
Here, the type is accompanied by an invariant, i.e. a logical property imposed on any value of that type. Why3 assumes that any rarray passed as an argument to a program function satisfies the invariant and it produces a proof obligation every time an rarray is created or modified in a program. Notice that this requires that types with invariants not be used in recursive data structures, just as mutable types.

An important feature of WhyML is ghost code, i.e. computations that only serve to facilitate verification and that can be safely removed from a program without affecting its final result. A ghost expression cannot be used in a non-ghost computation, it cannot modify a non-ghost mutable value, and it cannot raise exceptions that would escape into non-ghost code. However, a ghost expression can use non-ghost values and its result can be used in program annotations. A classical use case for ghost code is that of step counters to prove time complexity of an algorithm. It also serves to equip a data structure with a ghost field containing a pure logical "view" for specification purposes.

Case Studies

We have used WhyML to verify a lot of non-trivial data structures and algorithms. Our gallery (http://proval.lri.fr/gallery/why3.en.html) currently contains 67 case studies. In this section, we illustrate three different kinds of verification.

Verification of an Algorithm. Let us consider the Knuth-Morris-Pratt algorithm for string searching [START_REF] Knuth | Fast pattern matching in strings[END_REF]. A string is simply an array of characters. Arrays are imported from the Why3 standard library. Conversely, the type of characters is declared as an abstract, uninterpreted type character. The Knuth-Morris-Pratt algorithm is then implemented as a function that receives two strings p and t and that returns, if any, the position of the first occurrence of p in t and, otherwise, the length of t: let kmp (p a: array character) where arrays and lists are imported from the Why3 standard library. Field data is declared mutable, in order to allow dynamic resizing, for the case when the array holding the buckets is replaced by a new, larger array. This operation changes the current set of aliases and the type system of WhyML can detect and safely handle it. In particular, after the resize, one cannot use any stale pointer to the old value of data. Also, the new value of data must be fresh. The key point here is modularity: One can implement resizing in a separate function and call it, for instance, from the add function that inserts a new element in the table.

requires { 1 ≤ length p ∧ 0 ≤ length a } ensures { first

Specification of a Data

Structure. There are data structures that cannot be implemented in WhyML. Simply speaking, these are pointer-based data structures where mutable nodes are arbitrarily nested, e.g. doubly-linked lists or mutable trees. Still we can easily model such data structures and then verify the programs that use them. Let us consider, for instance, a program building a perfect maze using a union-find data structure, as proposed in the VACID-0 benchmark [START_REF] Leino | VACID-0: Verification of ample correctness of invariants of data-structures[END_REF]. A union-find can be implemented in WhyML using arrays. However, a more flexible implementation, with chains of pointers, is beyond the scope of WhyML, and is simply modeled as follows:

type uf model { mutable contents: uf _ pure } There are three ideas here. First, the keyword model replaces the equal sign. This means that type uf is not a record, as far as programs are concerned, but an abstract data type. Inside specifications, though, it is a record and its field contents may be accessed. Second, field contents is declared mutable, to account for the fact that uf is a mutable data structure. Last, a pure data type uf _ pure represents the immutable snapshot of the contents of the union-find data structure.

We then declare and specify operations over type uf. For instance, the function find that returns the representative of the class of a given element and may modify the structure (e.g. for path compression) can be specified as follows: val find (u : uf) (x : elt) : elt writes {u} ensures { result = repr u x ∧ same _ repr u (old u) }

The key point here is encapsulation: Though we cannot implement the union-find data structure, we can declare an interface data type to model it and then verify a client code (in this case, a program building a maze). Any implementation of union-find could be used without compromising the proof of the client code.

Future Work

The most immediate direction of our future development is the ability to verify that a given implementation conforms to an interface. This amounts to establishing a refinement relation between WhyML modules, their data types and their functions, be they defined or merely specified. We also plan to introduce some higher-order features in the specification language, e.g. set comprehensions and sum-like operations, together with suitable encodings to first-order logic. A more ambitious goal would be to accept higher-order programs in WhyML, in order to bring it closer to functional programming. Finally, our long-term goal is to merge the specification and programming languages, in the spirit of PVS and ACL2. The challenge is two-fold. We want to allow imperative constructions in pure functions, provided they do not break referential transparency. Even more importantly, we want to state and prove theorems about WhyML programs, beyond what is possible to express using pre-and postconditions.

  _ occur p a result } = ... where first _ occur is a predicate introduced earlier in the specification. To get an executable code, Why3 translates WhyML to OCaml. In the process, uninterpreted WhyML types are either mapped to existing OCaml types or left as abstract data types. In the example above, this results into the following OCaml function:val kmp: character array → character array → Num.twhere array is the OCaml built-in type, character is an abstract data type, and Num.t is the type of arbitrary precision integers from OCaml library. Such a mapping can be customized at the user level. The key point here is genericity. Extracted code is parameterized w.r.t. uninterpreted symbols, such as the character type from the above example. It is then possible to instantiate the extracted code in different ways, for example by wrapping it into an OCaml functor.

Verification of a Data Structure. Let us implement hash tables (associative arrays) in WhyML, using an uninterpreted type key for keys: type t 'a = { mutable size: int;

( * total number of elements * ) mutable data: array (list (key, 'a)); ( * buckets * ) }