VPT 2014 EASYCHAIR PROCEEDINGS: PAPERS WITH ABSTRACTS
Editors: Alexei Lisitsa and Andrei Nemytykh
| Authors, Title and Abstract | Paper | Talk |
|---|---|---|
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 |  | |
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. | | Jul 18 08:45 |
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 \textit{prog} as a predicate {\tt incorrect} defined
by a CLP program $P$, and we show that
\textit{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 \textit{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. | | Jul 17 11:30 |
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. | | Jul 18 11:30 |
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. | | Jul 18 12:15 |
{Regular paper}
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. | | Jul 17 12:15 |
{Regular paper}
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. | | Jul 18 10:45 |
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. | | Jul 17 10:45 |
In previous work~\cite{sewell2013translation} 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~\cite{Klein_EHACDEEKNSTW_09} 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. | | Jul 18 17:30 |