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. {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.

ABSTRACT. Nested Petri nets (NP-nets) is an extension of the Petri nets formalism with accordance to 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 for 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 show 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. 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.