VPT 2014: Papers with AbstractsPapers 

Abstract. We argue that formal methods such as B can be used to conveniently express a wide range of constraint satisfaction problems. We also show that some problems can be solved quite eectively by existing formal methods tools such as Alloy or ProB. We illustrate our claim on several examples. Our approach is particularly interesting when a high assurance of correctness is required. Indeed, validation and double checking of solutions is available for certain formal methods tools and formal proof can be applied to establish important properties or provide unambiguous semantics to problem specications. The experiments also provide interesting insights about the eectiveness of existing formal method tools, and highlight interesting avenues for future improvement. 1  Abstract. Some security properties go beyond what is expressible in terms of an individual execution of a single program. In particular, many security policies in cryptography can be naturally phrased as relational properties of two open probabilistic programs. Writing and verifying proofs of such properties is an errorprone task that calls for automation and tool support. One of the main difficulties in automating these proofs lies in finding adequate relational invariants for loops and specifications for program holes. In this talk we show how to automate proofs of relational properties of open probabilistic programs by adapting techniques for the automatic generation of universally quantified invariants in a nonrelational setting.  Abstract. The transformation of constraint logic programs (CLP programs) has been shown to be an effective methodology for verifying properties of imperative programs. By following this methodology, we encode the negation of a partial correctness property of an imperative program prog as a predicate incorrect defined by a CLP program P, and we show that prog is correct by transforming P into the empty program through the application of semantics preserving transformation rules. Some of these rules perform replacements of constraints that encode properties of the data structures manipulated by the program prog. In this paper we show that Constraint Handling Rules (CHR) are a suitable formalism for representing and applying constraint replacements during the transformation of CLP programs. In particular, we consider programs that manipulate integer arrays and we present a CHR encoding of a constraint replacement strategy based on the theory of arrays. We also propose a novel generalization strategy for constraints on integer arrays that combines the CHR constraint replacement strategy with various generalization operator for linear constraints, such as widening and convex hull. Generalization is controlled by additional constraints that relate the variable identifiers in the imperative program and the CLP representation of their values. The method presented in this paper has been implemented and we have demonstrated its effectiveness on a set of benchmark programs taken from the literature.  Abstract. Nested Petri nets (NPnets) is an extension of the Petri nets formalism within the “netswithinnets” approach, when tokens in a marking are themselves Petri nets which have autonomous behavior and synchronize with the system net. The formalism of NP nets allows modeling multilevel multiagent systems with dynamic structure in a natural way. In this paper we define branching processes and unfoldings for conservative NP nets, i.e. for NPnets with a persistent set of agents. We prove that NPnets unfoldings satisfy the fundamental property of unfoldings, and thus can be used for verification of conservative NPnets in line with classical unfolding methods.  Abstract. A program transformation technique should terminate, return efficient output programs and be efficient itself.
For positive supercompilation ensuring termination requires memoisation of expressions, and these are subsequently used to determine when to perform generalization and folding. For a firstorder language, every infinite sequence of transformation steps must include function unfolding, so it is sufficient to memoise only those expressions immediately prior to a function unfolding step.
However, for a higherorder language, it is possible for an expression to have an infinite sequence of transformation steps which do not include function unfolding, so memoisation prior to a function unfolding step is not sufficient by itself to ensure termination. But memoising additional expressions is expensive during transformation and may lead to less efficient output programs due to auxiliary functions. This additional memoisation may happen explicitly during transformation or implicitly via a preprocessing transformation as outlined in previous work by the first author.
We introduce a new technique for local driving in higherorder positive supercompilation which obliviates the need for memoising other expressions than function unfolding steps, thereby improving efficiency of both the transformation and the generated programs. We exploit the fact, due to the second author in the setting of typefree lambdacalculus that every expression with an infinite sequence of transformation steps not involving function unfolding must have somthing like the term Omega = (lambda x. x x) (lambda x . x x) embedded within it in a certain sense. The technique has proven useful on a host of examples.  Abstract. The paper presents two examples of nontraditional using of program specialization by Turchin's supercompilation method. In both cases we are interested in syntactical properties of residual programs produced by supercompilation. In the first example we apply supercompilation to a program encoding a word equation and as a result we obtain a program representing a graph describing the solution set of the word equation. The idea of the second example belongs to Alexandr V. Korlyukov. He considered an interpreter simulating the dynamic of the well known missionariescannibals puzzle. Supercompilation of the interpreter allows us to solve the puzzle. The interpreter may also be seen as an encoding of a nondeterministic protocol.  Abstract. As a rule, program transformation methods based on semantics unfold a semantic tree of a given program. Sometimes that allows to optimize the program or to prove its certain properties automatically. Unfolding is one of the basic operations, which is a metaextension of one step of the abstract machine executing the program. This paper is interested in unfolding for programs based on pattern matching and manipulating the strings. The corresponding computation model originates from Markov's normal algorithms and extends this theoretical base. Even though algorithms unfolding programs were being intensively studied for a long time in the context of variety of programming languages, as far as we know, the associative concatenation was stood at the wayside of the stream. We define a class of term rewriting systems manipulating with strings and describe an algorithm unfolding the programs from the class. The programming language defined by this class is algorithmic complete. Given a word equation, one of the algorithms suggested in this paper results in a description of the corresponding solution set.  Abstract. The paper describes a verification technique based on program transformation with unfolding that allows to find short attacks on multiparty pingpong protocols in the DolevYao intruder model. Protocols are modelled by prefix grammars, and questions of model optimization and complexity are considered.  Abstract. In previous work [Sewell, Myreen and Klein, 2013] we have implemented a translation validation mechanism for checking that a C compiler is adhering to the expected semantics of a verified program. We used this apparatus to check the compilation of the seL4 verified operating system kernel [Klein et.al. 2009] by GCC 4.5.1. To get this result, we carefully chose a problem representation that worked well with certain highly optimised SMT solvers. This raises a question of correctness. While we are confident the result is correct, we still aim to replay this result with the most dependable tools available.
In this work we present a formalisation of the proof rules needed to replay the translation check within the theorem prover Isabelle/HOL. This is part of an ongoing effort to bring the entire translation validation result within a single trusted proof engine and derive a single correctness theorem, thus reaching the gold standard level of trustworthiness for program verification.
We had hoped to present the formal rule set in action through a worked example. Unfortunately while we have all the theory we need, the mechanisms for selecting and applying the rules and discharging certain side conditions remain a work in progress, and our example proof is incomplete. 

