Invited speakers

  • Wan Fokkink
    • Vrije Universiteit Amsterdam, NL
    • Joint invited speaker with EXPRESS 2011

Program Committee

Contact email

  • ps AT ecs DOT soton DOT ac DOT uk

Organisers

Website

sos2011.ecs.soton.ac.uk

Programme

Joint SOS/Express invited talk
9:00 - 10:00 Wan Fokkink. Why Modal Characterizations of Process Semantics Totally Rock.
I will give a survey of recent results on the relation between structural operational semantics, modal logic, and process algebra. The following three topics will be discussed.
  1. Given a modal characterization of a semantics, one can derive a congruence format for this semantics in the context of structural operational semantics.
  2. Given transition rules for a process operator, one can derive requirements on modal characterizations to guarantee that the corresponding semantics is a congruence for this operator.
  3. Necessary and sufficient requirements have been given on modal characterizations to guarantee that the corresponding semantics is sound for the proof principle AIP.
First morning session
10:00 - 10:30 David Romero Hernández and David Frutos Escrig. On the Unification of Process Semantics: Logical Semantics.
We continue with the task of obtaining a unifying view of process semantics by considering in this case the logical characterization of the semantics. We start by considering the classic linear time-branching time spectrum developed by R.J. van Glabbeek. He provided a logical characterization of most of the semantics in his spectrum but, without following a unique pattern. In this paper, we present a uniform logical characterization of all the semantics in the enlarged spectrum. The common structure of the formulas that constitute all the corresponding logics gives us a much clearer picture of the spectrum, clarifying the relations between the different semantics, and allows us to develop generic proofs of some general properties of the semantics.
Coffee break
10:30 - 11:00
Second morning session
11:00 - 11:30 Asiri Rathnayake and Hayo Thielecke. Regular expression matching and operational semantics.
Many programming languages and tools, ranging from grep to the Java String library, contain regular expression matchers. Rather than first translating a regular expression into a deterministic finite automaton, such implementations typically match the regular expression on the fly. Thus they can be seen as virtual machines interpreting the regular expression much as if it were a program with some non-deterministic constructs such as the Kleene star. We formalize this implementation technique for regular expression matching using operational semantics. Specifically, we derive a series of abstract machines, moving from the abstract definition of matching to increasingly realistic machines. First a continuation is added to the operational semantics to describe what remains to be matched after the current expression. Next, we represent the expression as a data structure using pointers, which enables redundant searches to be eliminated via testing for pointer equality. From there, we arrive both at Thompson's lockstep construction and a machine that performs some operations in parallel, suitable for implementation on a large number of cores, such as a GPU. We formalize the parallel machine using process algebra and report some preliminary experiments with an implementation on a graphics processor using CUDA.
11:30 - 12:00 Luca Aceto, Georgiana Caltais, Eugen-Ioan Goriac and Anna Ingolfsdottir. Axiomatizing GSOS with Predicates.
In this paper, we introduce an extension of the GSOS rule format with predicates such as termination, convergence and divergence. For this format we generalize the technique proposed by Aceto, Bloom and Vaandrager for the automatic generation of ground-complete axiomatizations of bisimilarity over GSOS systems. Our procedure is implemented in a tool that receives SOS specifications as input and derives the corresponding axiomatizations automatically. This paves the way to checking strong bisimilarity over process terms by means of theorem-proving techniques.
12:00 - 12:30 Ken Madlener, Sjaak Smetsers and Marko Van Eekelen. Formal Component-Based Semantics.
One of the proposed solutions for improving the scalability of semantics of programming languages is Component-Based Semantics, introduced by Peter D. Mosses. It is expected that this framework can also be used effectively for modular meta theoretic reasoning. This paper presents a formalization of Component-Based Semantics in the theorem prover Coq. It is based on Modular SOS, a variant of SOS, and makes essential use of dependent types, while profiting from type classes. This formalization constitutes a contribution towards modular meta theoretic formalizations in theorem provers. As a small example, a modular proof of determinism of a mini-language is developed.
End of workshop and lunch

Aim

Structural operational semantics (SOS) provides a framework for giving operational semantics to programming and specification languages. A growing number of programming languages from commercial and academic spheres have been given usable semantic descriptions by means of structural operational semantics. Because of its intuitive appeal and flexibility, structural operational semantics has found considerable application in the study of the semantics of concurrent processes. It is also a viable alternative to denotational semantics in the static analysis of programs, and in proving compiler correctness. Moreover, it has found application in emerging areas of computing such as probabilistic systems and systems biology.

Structural operational semantics has been successfully applied as a formal tool to establish results that hold for classes of process description languages. This has allowed for the generalization of well-known results in the field of process algebra, and for the development of a meta-theory for process calculi based on the realization that many of the results in this field only depend upon general semantic properties of language constructs.

This workshop aims at being a forum for researchers, students and practitioners interested in new developments, and directions for future investigation, in the field of structural operational semantics. One of the specific goals of the series of SOS workshops is to establish synergies between the concurrency and programming language communities working on the theory and practice of SOS.

Specific topics of interest include (but are not limited to)

  • programming languages, process algebras and higher-order formalisms
  • foundations of SOS
  • category theoretic approaches
  • conservative extensions and translations of SOS specifications
  • congruence results and their meta-theory
  • modal logics, program logics and SOS
  • ordered, modular, and other variants of SOS
  • SOS of probabilistic, timed, stochastic and hybrid systems
  • SOS and rewriting systems, reactive systems and other forms of operational specification
  • comparisons between denotational, axiomatic and structural operational semantics
  • software tools that automate, or are based on, SOS.
Reports on applications of SOS to other fields, including:
  • modelling and analysis of biological systems
  • security of computer systems
  • programming, modelling and analysis of embedded systems
  • specification of middle-ware and coordination languages
  • programming language semantics and implementation
  • static analysis
  • software and hardware verification
  • semantics for domain-specific languages and model-based engineering,
are also most welcome.

History

The first SOS Workshop took place in London as one of the satellite workshops of CONCUR 2004. Subsequently, SOS 2005 occurred in Lisbon as a satellite workshop of ICALP 2005, SOS 2006 in Bonn as a satellite workshop of CONCUR 2006, SOS 2007 in Wroclaw as a satellite workshop of LICS and ICALP 2007, and SOS 2008 in Reykjavik as a satellite workshop of ICALP 2008. SOS 2009 was held as a satellite workshop of CONCUR 2009 in Bologna. Finally, SOS 2010 was held as a satellite workshop of CONCUR 2010 in Paris.

A special issue of the Journal of Logic and Algebraic Programming on Structural Operational Semantics appeared in 2004; a special issue of Theoretical Computer Science dedicated to SOS 2005 appeared in 2007, and a special issue of Information & Computation on Structural Operational Semantics inspired by SOS 2006-2007 appeared in 2009.

Paper submission

We solicit unpublished papers reporting on original research on the general theme of SOS. Prospective authors should submit a paper via Easychair by Friday, 3rd June 2010. (If you do not have an Easychair account, you can create it by following the link). Papers should take the form of a pdf file in EPTCS format, whose length should not exceed 15 pages (not including an optional "Appendix for referees" containing proofs that will not be included in the final paper). We will also consider 5-page papers describing tools to be demonstrated at the workshop.

Proceedings

Preliminary proceedings will be available at the meeting. The final proceedings of the workshop will appear as a volume in the EPTCS series. If the quality and quantity of the submissions warrant it, the co-chairs plan to arrange a special issue of an archival journal devoted to full versions of selected papers from the workshop.

Important dates:

  • Submission of abstract: Friday 27 May 2011
  • Submission: Friday 3 June 2011
  • Notification: Friday 1 July 2011
  • Final version: Friday 15 July 2011
  • Workshop: Monday 5 September 2011