Invited speakers

Wan Fokkink
 Vrije Universiteit Amsterdam, NL
 Joint invited speaker with EXPRESS 2011
Program Committee
 Luca Aceto
 (Reykjavik, )
 Simon Bliudze
 (CEA LIST, )
 Filippo Bonchi
 (ENS Lyon, )
 Fabio Gadducci
 (Pisa, )
 Matthew Hennessy
 (Dublin, )
 Bartek Klin
 (Warsaw, )
 Keiko Nakata
 (Tallinn, )
 Michel Reniers
 (Eindhoven, , cochair)
 Pawel Sobocinski
 (Southampton, , cochair)
 Sam Staton
 (Cambridge, )
 Daniele Varacca
 (Paris VII, )
Contact email
 ps AT ecs DOT soton DOT ac DOT uk
Organisers

Michel Reniers
 Technical University Eindhoven
 Department of Mechanical Engineering
 P.O. Box 513
 NL5600 MB Eindhoven
 The Netherlands

Pawel Sobocinski
 University of Southampton
 DSSE
Electronics and Computer Science  Southampton SO17 1BJ
 UK
Website
sos2011.ecs.soton.ac.ukProgramme
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.


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 timebranching 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 nondeterministic 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, EugenIoan 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 groundcomplete 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 theoremproving techniques.  
12:00  12:30  Ken Madlener, Sjaak Smetsers and Marko Van Eekelen. Formal ComponentBased Semantics. 
One of the proposed solutions for improving the scalability of semantics of programming languages is ComponentBased 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 ComponentBased 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 minilanguage 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 wellknown results in the field of process algebra, and for the development of a metatheory 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 higherorder formalisms
 foundations of SOS
 category theoretic approaches
 conservative extensions and translations of SOS specifications
 congruence results and their metatheory
 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.
 modelling and analysis of biological systems
 security of computer systems
 programming, modelling and analysis of embedded systems
 specification of middleware and coordination languages
 programming language semantics and implementation
 static analysis
 software and hardware verification
 semantics for domainspecific languages and modelbased engineering,
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 20062007 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 5page 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 cochairs 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