VPT 2014: Papers with Abstracts

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 error-prone 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 non-relational 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 (NP-nets) is an extension of the Petri nets formalism within the “nets-within-nets” 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 multi-level multi-agent systems with dynamic structure in a natural way. In this paper we define branching processes and unfoldings for conservative NP- nets, i.e. for NP-nets with a persistent set of agents. We prove that NP-nets unfoldings satisfy the fundamental property of unfoldings, and thus can be used for verification of conservative NP-nets 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 first-order 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 higher-order 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 pre-processing transformation as outlined in previous work by the first author.

We introduce a new technique for local driving in higher-order 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 type-free lambda-calculus 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 non-traditional 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 missionaries-cannibals puzzle. Supercompilation of the interpreter allows us to solve the puzzle.
The interpreter may also be seen as an encoding of a non-deterministic 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 meta-extension 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 multi-party ping-pong protocols in the Dolev-Yao 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.