The seventeenth meeting of the Wes= sex Theory Seminar will take place at Queen Mary, University of London = on 20th September 2012.

=20The talks will be held in room BR3.01 of QMUL http://goo.gl/map= s/vBkgo

=2011:00 coffee at the Hub, next to the conference room

=2011:30 **Radu Grigore** (Queen Mary), Register Automata and =
Java

12:15 **Stefan Kiefer** (Oxford), On the equivalence proble=
m for probabilistic automata

13:00 lunch (not provided, but we suggest the Curve or Drapers)

=2014:15 **Tony Tan** (Warsaw), An Automata Model for Trees wi=
th Ordered Data Values

15:00 **Nobuko Yoshida** (Imperial), Multiparty Session Aut=
omata and their application in large distributed systems

15:45 coffee at the Hub

=2016:15 **Jules Villard** (UCL), The Ramifications of Sharing=
in Data Structures

17:00 **Nick Benton** (Microsoft Research), High-Level Sepa=
ration Logic for Low-Level Code

17:45 pub/dinner

=20Is it possible to use register automata to specify Java programs with dy= namic allocation of resources? Intuitively the answer should be affirmative= . Register automata denote languages over infinite alphabets, and program e= xecutions are traces of events, which may mention an unbounded number of re= sources. However, details sometimes hide devils. Would such specifications = be convenient and useful? I will try to convince you that the answer is ind= eed affirmative, with examples and details. I introduce TOPL automata, whic= h are equally expressive to register automata, but more convenient for this= task. I will demonstrate how they are used for runtime verification. Final= ly, I will show some preliminary work on how to use TOPL automata for stati= c analysis. This is joint work with Dino Distefano, Rasmus Lerchedahl Peter= sen, and Nikos Tzevelekos.

=20Deciding equivalence of probabilistic automata is a key problem for esta= blishing various behavioural and anonymity properties of probabilistic syst= ems. In particular, it is at the heart of the tool APEX, an analyser for pr= obabilistic programs. APEX is based on game semantics and analyses a broad = range of anonymity and termination properties of randomised protocols and o= ther open programs.

=20In recent experiments a randomised equivalence test based on polynomial = identity testing outperformed deterministic algorithms. We show that polyno= mial identity testing yields efficient algorithms for various generalisatio= ns of the equivalence problem. First, we provide a randomized NC procedure = that also outputs a counterexample trace in case of inequivalence. Second, = we consider equivalence of probabilistic cost automata. In these automata t= ransitions are labelled with integer costs and each word is associated with= a distribution on costs, corresponding to the cumulative costs of the acce= pting runs on that word. Two automata are equivalent if they induce the sam= e cost distributions on each input word. We show that equivalence can be ch= ecked in randomised polynomial time. Finally we show that the equivalence p= roblem for probabilistic visibly pushdown automata is logspace equivalent t= o the problem of whether a polynomial represented by an arithmetic circuit = is identically zero.

=20Data trees are trees in which each node, besides carrying a label from a= finite alphabet, also carries a data value from an infinite domain. They h= ave been used as an abstraction model for reasoning tasks on XML and verifi= cation. However, most existing approaches consider the case where only equa= lity test can be performed on the data values.

=20In this paper we study data trees in which the data values come from a l= inearly ordered domain, and in addition to equality test, we can test wheth= er the data value in a node is greater than the one in another node. We int= roduce an automata model for them which we call ordered-data tree automata = (ODTA), provide its logical characterisation, and prove that its emptiness = problem is decidable in 3-NEXPTIME. We also show that the two-variable logi= c on unranked trees, studied by Bojanczyk, Muscholl, Schwentick and Segoufi= n in 2009, corresponds precisely to a special subclass of this automata mod= el.

=20Then we define a slightly weaker version of ODTA, which we call weak ODT= A, and provide its logical characterisation. The complexity of the emptines= s problem drops to NP. However, a number of existing formalisms and models = studied in the literature can be captured already by weak ODTA. We also sho= w that the definition of ODTA can be easily modified, to the case where the= data values come from a tree-like partially ordered domain, such as string= s.

=20Communicating finite state machines (CFSMs for short) abstract processes= which communicate by asynchronous exchanges of messages via FIFO channels.= Their major impact has been in characterising essential properties of comm= unications such as freedom from deadlock and communication error, and buffe= r boundedness. CFSMs are known to be computationally hard: most of these pr= operties are undecidable even in restricted cases. On the other hand, multi= party session types are a recent typed framework whose main features are it= s ability to efficiently enforce these properties for mobile processes and = programming languages.

=20This talk ties the links between the two frameworks to achieve a two-fol= d goal. On one hand, we present a generalised variant of multiparty session= types that have a direct semantical correspondence to CFSMs. Our calculus = can treat expressive forking, merging and joining protocols that are absent= from existing frameworks, and the typing system can ensure properties such= as safety, boundedness and liveness on distributed processes in polynomial= time.

=20On the other hand, multiparty session types generate a new class of CFSM= s that automatically enjoy the aforementioned properties. This solves an op= en question on CFSMs, generalising Gouda et al's work in 1984, which covere= d the two-machine case and presented polynomial time algorithms.Our framewo= rk works with an arbitrary number of machines, still offering a polynomial = time algorithm.

=20I also talk about a summary of our recent collaborations based on multip= arty session automata, with industry partners and a major, long-term, NSF-f= unded program which provides a ultra large scale cyberinfrustracture for 25= -30 years of sustained ocean measurements to study climate variability, oce= an circulation and ecosystem dynamics.

=20Programs manipulating mutable data structures with intrinsic sharing pre= sent a challenge for modular verification. Deep aliasing inside data struct= ures dramatically complicates reasoning in isolation over parts of these ob= jects because changes to one part of the structure (say, the left child of = a dag node) can affect other parts (the right child or some of its descenda= nts) that may point into it. The result is that finding intuitive and compo= sitional proofs of correctness is usually a struggle. We propose a composit= ional proof system that enables local reasoning in the presence of sharing.=

=20While the AI "frame problem" elegantly captures the reasoning required t= o verify programs without sharing, we contend that natural reasoning about = programs with sharing instead requires an answer to a different and more ch= allenging AI problem, the "ramification problem": reasoning about the indir= ect consequences of actions. Accordingly, we present a Ramify proof rule th= at attacks the ramification problem head-on and show how to reason with it.= Our framework is valid in any separation logic and permits sound compositi= onal and local reasoning in the context of both specified and unspecified s= haring. This talk will be illustrated by proofs of examples manipulating da= gs, graphs, and overlaid data structures.

=20Separation logic is a powerful tool for reasoning about structured, impe= rative programs that manipulate pointers. However, its application to unstr= uctured, lower-level languages such as assembly language or machine code re= mains challenging. In this paper we describe a separation logic tailored fo= r this purpose that we have applied to x86 machine code programs.

=20The logic is built from an assertion logic on machine states over which = we construct a specification logic that encapsulates uses of frames and ste= p indexing. The traditional notion of Hoare triple is not applicable direct= ly to unstructured machine code, where code and data are mixed together and= programs do not in general run to completion, so instead we adopt a contin= uation-passing style of specification with preconditions alone. Nevertheles= s, the range of primitives provided by the specification logic, which inclu= de a higher-order frame connective, a novel read-only frame connective, and= a `later=C2=BF modality, support the definition of derived forms to suppor= t basic-block-style reasoning for common cases, in which standard rules for= Hoare triples are derived as lemmas. Furthermore, our encoding of assembly= language labels in terms of the more primitive code pointers lets us encap= sulate local usage of labels and the definition and rules for assembly-lang= uage `macros=C2=BF such as while loops and conditionals.

=20We have applied the framework to a model of x86 machine code built entir= ely within the Coq proof assistant, including tactic support based on compu= tational reflection.

=20This is joint work with Jonas Jensen and Andrew Kennedy.

=20From Bath:

=20- =20
- John Power =20
- Cai Wingfield =20

From Birmingham:

=20- =20
- Liang-Ting Chen =20
- Martin Escardo =20
- Olle Fredriksson =20
- Dan Ghica =20
- Chuangjie Xu =20

From Imperial:

=20- =20
- Runa Jesmin =20
- Nobuko Yoshida =20

From Microsoft Research:

=20- =20
- Nick Benton =20

From Oxford:

=20- =20
- Stefan Kiefer =20

From Queen Mary:

=20- =20
- Yasin Anbar =20
- Rob Arthan =20
- Tzu-Chun Chen =20
- Nhat Anh Dang =20
- Dino Distefano =20
- Luca Fossati =20
- Radu Grigore =20
- Jules Hedges =20
- Paulo Oliva =20
- Quoc San Phan =20
- Edmund Robinson =20
- Nikos Tzevelekos =20
- Graham White =20

From Rennes:

=20- =20
- Delphine Demange =20

From University College London:

=20- =20
- Jules Villard =20

From Warsaw:

=20- =20
- Tony Tan =20