VSL 2014: VIENNA SUMMER OF LOGIC 2014
VPT ON FRIDAY, JULY 18TH, 2014
Days:
previous day
all days

View: session overviewtalk overviewside by side with other conferences

08:45-10:15 Session 86P: Invited speaker (A. Rybalchenko)
Location: FH, Dissertantenraum E104
08:45
Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk)
SPEAKER: unknown

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.

10:15-10:45Coffee Break
10:45-13:00 Session 90BF: Contributed Talks
Location: FH, Dissertantenraum E104
10:45
On Unfolding for Programs Using Strings as a Data Type

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.

11:30
Branching Processes of Conservative Nested Petri Nets
SPEAKER: Daniil Frumin

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.

12:15
Local Driving in Higher-Order Positive Supercompilation via the Omega-theorem
SPEAKER: unknown

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.

13:00-14:30Lunch Break
14:30-16:00 Session 96BG: Invited talk by Josep Silva (joint with WWV)
Location: FH, Seminarraum 107
14:30
Automatic Detection of Webpage Candidates for Site-Level Web Template Extraction
SPEAKER: Josep Silva
16:00-16:30Coffee Break
17:30-18:00 Session 102C: Joint session with WWV
Location: FH, Seminarraum 107
17:30
Formal Replay of Translation Validation for Highly Optimised C
SPEAKER: Thomas Sewell

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.