Call for Papers for FSEN 2011

I have been asked to distribute this call for papers. Consider submitting to FSEN 2011, thereby supporting a young, good-quality conference in formal approaches to software engineering, broadly construed!

########################################
                         CALL FOR PAPERS

                   Fourth International Conference on
               Fundamentals of Software Engineering 2011
                        Theory and Practice
                               (FSEN '11)

                        http://fsen.ir/2011

                            Tehran, Iran
                          April 20-22, 2011

########################################

About FSEN

FSEN is an international conference that aims to bring together
researchers, engineers, developers, and practitioners from the academia
and the industry, who work in every area of formal methods. This
conference seeks to facilitate the transfer of experience, adaptation of
methods, and where possible, foster collaboration among different groups.
The topics of interest cover all aspects of formal methods, especially
those related to advancing the application of formal methods in the
software industry and promoting their integration with practical
engineering techniques. Following the success of the previous FSEN events
in 2005, 2007 and 2009, the next event in the FSEN series will take place
in Tehran, Iran, April 20-22, 2011.
---------------------------------------------------------------------

In cooperation with

ACM SIGSOFT
IFIP WG2.2
---------------------------------------------------------------------

Important Dates

Abstract Submission:   October 18 , 2010
Paper Submission:      October 25 , 2010
Notification:          December 13, 2010
Camera Ready:          January 10 , 2011
Conference:            April 20-22, 2011
---------------------------------------------------------------------

Keynote Speakers

Carlo Ghezzi, Politecnico di Milano, Italy
Joost-Pieter Katoen, RWTH Aachen University, Germany

(Third speaker to be announced)
---------------------------------------------------------------------

Topics of Interest

The topics of this symposium include, but are not restricted to, the
following:

* Models of programs and systems
* Software specification, validation and verification
* Software architectures and their description languages
* Object and multi-agent systems
* Coordination and feature interaction
* Integration of formal and informal methods
* Integration of different formal methods
* Component-based development
* Service-oriented development
* Model checking and theorem proving
* Software and hardware verification
* CASE tools and tool integration
* Application to industrial cases

The length of each paper including figures and references must not exceed
15 pages and should conform to the Springer LNCS style. All papers must be
submitted in PDF or postscript format. Submissions should explicitly state
their contribution and their relevance to the theme of the conference.
Other criteria for selection will be originality, significance,
correctness, and clarity. Simultaneous or similar submissions to other
conferences or journals are not allowed.
----------------------------------------------------------------------

Proceeding and Special Issues

The post-proceedings of FSEN11 will be published by Springer Verlag in the
LNCS series.  There will also be a pre-proceeding for the accepted papers,
which is printed locally by IPM. This pre-proceeding will be made
available at the conference.

The proceedings of FSEN07 and FSEN09 were published in the LNCS series. A
special issue of Science of Computer Programming is being published,
containing the extended versions of a selection of papers of FSEN09. A
special issue of Fundamenta Informaticae was published, containing the
extended versions of a selection of papers of FSEN07. The proceedings of
FSEN05 was published in the ENTCS series: ENTCS 159 (2006). Two special
issues were published containing the extended versions of a selection of
papers of FSEN05 in Fundamenta Informaticae (FI, vol. 82, 2008) and  in
Journal of Universal Computing (J.UCS, 13(13), 2007).

----------------------------------------------------------------------
General Chair

Hamid Sarbazi-azad - IPM, Iran; Sharif University of Technology, Iran

Program Chairs

Farhad Arbab - CWI, Netherlands; Leiden University, Netherlands
Marjan Sirjani - Reykjavik University, Iceland; University of Tehran, Iran

Steering Committee

Farhad Arbab - CWI, Netherlands; Leiden University, Netherlands
Christel Baier - University of Dresden, Germany
Frank de Boer - CWI, Netherlands; Leiden University, Netherlands
Ali Movaghar - IPM, Iran; Sharif University of Technology, Iran
Hamid Sarbazi-azad - IPM, Iran; Sharif University of Technology, Iran
Marjan Sirjani - Reykjavik University, Iceland; University of Tehran, Iran
Jan Rutten - CWI, Netherlands; Vrije University Amsterdam, Netherlands

Program Committee

Luca Aceto - Reykjavik University, Reykjavik, Iceland
Gul Agha - University of Illinois at Urbana - Champaign, USA
Farhad Arbab - CWI, Netherlands; Leiden University, Netherlands
Jos Baeten - Eindhoven University of Technology, Netherlands
Christel Baier - University of Dresden, Germany
Frank de Boer - CWI, Netherlands; Leiden University, Netherlands
Marcello Bonsangue - Leiden University, Netherlands
Mario Bravetti - University of Bologna
James C. Browne - University of Texas at Austin, USA
Einar Broch Johnsen - University of Oslo, Norway
Michael Butler - University of Southampton, UK
David Clarke - CWI, Netherlands; K.U.Leuven, Belgium
Wan Fokkink - Vrije Universiteit Amsterdam, Netherlands
Masahiro Fujita - University of Tokyo, Japan
Maurizio Gabbrielli - University of Bologna, Italy
Radu Grosu - State University of New York at Stony Brook, USA
Jan Friso Groote - Technical University of Eindhoven, Netherlands
Joost Kok - Leiden University, Netherlands
Ramtin Khosravi - University of Tehran, Iran
Kim Larsen - Aalborg University, Denmark
Zhiming Liu - United Nations University, Macao, China
Seyyed Hassan Mirian - Sharif University of Technology, Iran
Sun Meng - Peking University, China
Ugo Montanari - University of Pisa, Italy
Peter Mosses - Swansea University, UK
Mohammad Reza Mousavi - Technical University of Eindhoven, Netherlands
Ali Movaghar - IPM, Iran; Sharif University of Technology, Iran
Andrea Omicini - University of Bologna, Italy
Saeed Parsa - Iran University of Science & Technology, Iran
Hiren Patel - University of Waterloo, Canada
Jan Rutten - CWI, Netherlands; Vrije University Amsterdam, Netherlands
Davide Sangiorgi - University of Bologna, Italy
Marjan Sirjani - Reykjavik University, Iceland; University of Tehran, Iran
Carolyn Talcott - SRI International, USA

CNRS Bronze Medal to Thomas Colcombet

Thomas Colcombet of LIAFA, Université Paris Diderot - Paris 7, has been awarded a CNRS bronze medal. See here for the full list of awardees. As you can see, Thomas is the only recipient of the award in the field of computer science. It is good for TCS at large to see one of its researchers receive such a prestigious national award.

This has been quite a year for researchers working on the classic theory of automata, logic and their applications. Earlier in 2010, one of Thomas' collaborators, viz. Mikolaj Bojanczyk, received the first Presburger Award and Anca Muscholl was awarded a CNRS silver medal.

Congrats to all of them!

SOS 2010

On August 30, Pawel Sobocinski and I co-chaired SOS 2010, an affiliated workshop of CONCUR 2010. The workshop programme was interesting and we had 18 participants. (It was hard to compete with EXPRESS 2010, which had 35 registered participants.) The proceedings for the workshop are available as an EPTCS volume.

Apart from five contributed talks touching on a fairly wide variety of topics, the workshop featured two invited presentations. MohammadReza Mousavi kicked off the workshop in style with a talk entitled How to cook a security-enabled semantics. In his talk, which was partly based on this paper, Mohammad introduced notions such as restricted revocable delegation and studied their consequences in language-based security. Listening to Mohammad speak I felt, not for the first time, that language-based security is one of the (alas, many) topics that I should make an effort to understand better.

The second invited talk was joint with EXPRESS, and was delivered by Catuscia Palamidessi. Catuscia had a very large audience for a workshop, and fortunately we had decided to move to a lecture hall that could hold about 100 people before her talk :-). Catsucia's talk, which was entitled Compositionality of Secure Information Flow, dealt with ways in which one can quantify the amount of leakage of confidential information through public outputs in computer systems. Catuscia discussed a proposal for measuring the amount of leakage that is based on the Bayes risk, namely (the converse of) the probability of guessing the right value of the secret, once we have observed the output. In her talk, Catuscia presented a process calculus for the specification of systems composed by concurrent and probabilistic processes, and investigated "safe constructs", namely constructs which do not increase the leakage.

Overall, I like to think that SOS 2010 was a successful workshop. However, I would like to see this workshop series be more visible and receive more submissions. I hope that future chairs will be more successful than I have been in achieving these goals.

A Selection of Papers from CONCUR 2010

As I have already mentioned in earlier posts, I enjoyed a lot of talks in the programme for CONCUR 2010. Here are just a few highlights, with apologies to all the speakers whose talks/papers I do not mention in this post. Overall, the conference programme was of very high quality. This bodes well for the future of CONCUR.

• Lutz Schröder and Yde Venema. Flat Coalgebraic Fixed Point Logic. Lutz presented the paper and gave a very clear introduction to the coalgebraic approach to the study of modal logics. Technically, this paper presents a unified co-algebraic treatment  of flat fixed-point logics. (Fixed-point logics, such as the mu-calculus, are widely used in computer science, in particular in artificial intelligence and concurrency.) The main results in the paper are the completeness of the Kozen-Park axiomatization and a general  EXPTIME upper bound for flat fixed-point logics.
• Fides Aarts and Frits Vaandrager. Learning I/O Automata. The talk was delivered by Frits, who addressed the general question of learning models of reactive systems automatically, e.g., for model-based testing or software engineering.In this work, Fides and Frits establish links between three widely used modelling frameworks for reactive systems: the ioco theory of Tretmans, the interface automata of De Alfaro and Henzinger, and Mealy machines. It is shown that, by exploiting these links, any tool for active learning of Mealy machines can be used for learning I/O automata that are deterministic and output determined. The approach presented in the paper has been implemented on top of the LearnLib tool and has been applied successfully to three case studies, including learning a model of Fides' biometric passport. 
• Pawel Sobocinski. Representations of Petri net interactions. . Pawel, who was my co-chair for SOS 2010, presented a novel compositional algebra of Petri nets. The algebra contains two binary operators (tensor product and sequential composition) and twelve constants! He also introduced a stateful extension of the calculus of connectors and showed that .these two formalisms have the same expressive power.
• Pavol Cerny, Thomas Henzinger and Arjun Radhakrishna. Simulation Distances.  The simulation preorder is often used to establish the correctness of an implementation I with respect to a specification S as follows: I correctly implements S if S can simulate the behaviour of I. In other words, this happens if everything the implementation I does is allowed by the specification S. The result of such a verification is boolean and cannot be used to assess how far I is from implementing the behaviour allowed by  S. This paper extends the simulation preorder to the quantitative setting by  defining three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. The paper develops a comprehensive theory for those notions of simulation distances. 

Reading the papers from CONCUR 2010 will keep me busy for some time. 

Milner Session at CONCUR 2010

During CONCUR 2010, the concurrency-theory community paid a small tribute to Robin Milner by dedicating a session of its flagship conference to him. The so-called Milner Session was held on Wednesday, 1 September, from 2pm till 4pm. It consisted of a talk by Jos Baeten and of three presentations of papers that were selected for the conference by the PC.

Jos kicked off the session with a talk devoted to Milner's contributions to concurrency theory. He focused on his seminal Calculus of Communicating Systems, providing an overview of its syntax, of some of the design decisions Milner made in that calculus and of its semantics. The presentation by Jos was followed by a short discussion, with remarks from Ugo Montanari, Kohei Honda and myself, amongst others.

My two readers might be interested in reading a short note  by Samson Ambramsky entitled Robin Milner's Work on Concurrency that was published yesterday in the Proceedings of MFPS 2010. According to Samson,

Robin’s ideas have become part of the air we breathe in our scientific community.....

CCS was not just a new calculus, but a new paradigm — that has played a central role in the subsequent development of our subject. It opened up the world of compositional behavioural modelling.

I have always found that one of the red threads in Milner's work was the, I believe novel, emphasis on behavioural semantics and on his standpoint that a process is an equivalence class of process descriptions (be they terms in a process algebra/calculus or states in a labelled transition system/automaton) modulo some notion of behavioural equivalence. Milner himself reiterated this point in several of his writings/talks, and I am glad to see this mentioned in Samson's piece.

We knew what functions were already! But what are processes? CCS established the fundamental methodological point of studying them through their observational behaviour (defined in terms of labelled transition systems via SOS).

This led inexorably in turn to notions of observational equivalence.

Thanks to Jos and Samson for their tributes to Milner's work.

Amongst the contributed talks in the Milner Session, let me mention the excellent talk by Edsko de Vries, who presented joint work with Vasileios Koutavas and Matthew Hennessy on Communicating Transactions. Communicating transactions are obtained by dropping the isolation requirement from standard transactions and can be used to model automatic error recovery in distributed systems. Edsko presented a behavioural theory for a version of CCS with communicating transactions that  is sound and complete with respect to the may-testing preorder. The technical work looked really impressive.

I really enjoyed Silvia Crafa's talk entitled A Logic for True Concurrency, which presented joint work with Paolo Baldan. Perhaps, I was biased since Silvia's talk brought me back in time some twenty years, when a different version of myself was working on topics related to true concurrency. However, I was not the only one to be impressed by that paper, which proposes a logic for true concurrency whose formulae describe events in computations and their causal dependencies. The induced logical equivalence is hereditary history preserving bisimilarity. The authors also identify fragments of the logic that capture other truly concurrent behavioural equivalences in the literature: step, pomset and history preserving bisimilarity. After Silvia's talk, I felt that her paper with Paolo should have been written long ago. 

A Thought Experiment

Suppose that a top-class conference to which you usually submit your papers decide to publish its proceedings in an electronic open-access outlet instead of using a commercial publisher, like STACS and FST-TCS have done over the last few years. Would that decision have any effect on whether you submit your papers to that conference? Would you encourage your students to submit to that conference in order to further their future career? Do you think that a prestigious conference has anything to lose in publishing its proceedings in an electronic open-access outlet?

CONCUR 2010

From August 30 till the very early hours of September 3, I was in Paris to co-chair SOS 2010 and attend CONCUR 2010. It is always a pleasure to have the chance to attend CONCUR, which is the flagship conference for the concurrency-theory community, and the lure of Paris made this conference even more attractive than usual.

CONCUR 2010 was perfectly organized by Paul Gastin (LSV, ENS Cachan, France), François Laroussinie (LIAFA, Université Denis Diderot - Paris 7, France) and their support team (see the bottom of this page for the details), and was held at Université Denis Diderot - Paris 7.

According to the program chairs, there were 160 people registered for the main conference and 215 people were registered for the conference or one of the eight affiliated events. I am not a CONCUR historian, but I believe that this makes this edition of CONCUR one of the best attended on record, together with the one held in Bologna last year. I do not find this level of attendance particularly surprising----after all, Paris is an attractive city and it is one of the hotbeds of research in concurrency theory. However, it is a great credit to the organizational effort that everything went smoothly and that the atmosphere at the conference was relaxed and conducive to both scientific and social exchanges.

On behalf of the CONCUR community, I'd like to say thanks to François, Paul and their support team for organizing a great conference. We had many excellent talks on a variety of exciting topics, a session devoted to Robin Milner (chaired by Matthew Hennessy and featuring a talk by Jos Baeten), varied and tasty lunches served next to the conference room, and yet another edition of the CONCUR football match (which saw about 20 participants kick a ball around for about one hour before the conference dinner).

I hope to devote another post to the main conference and to SOS 2010. Here I will just limit myself to a few brief remarks on the invited talks that I could attend. (Unfortunately, I had to leave at an ungodly early hour on Friday, 3 September, and therefore I missed  Holger Hermann's invited presentation and the last day of the conference. Knowing Holger's communication skills, I am sure that I missed a great talk. I hope that Holger will make a recording of his talk available from his web page.)

The conference was given the best possible start by Vladimiro Sassone, who delivered a very clear talk entitled Trust in Anonymity Networks.  In his presentation, after having introduced the basic setting of anonymity protocols, Vladimiro presented an analysis of the privacy guarantees of the Crowds anonymity protocol, with and without onion forwarding, for standard and adaptive attacks against the trust level of honest users.

I had the great honour of chairing the session featuring the second invited talks, which was delivered by Maurice Herlihy. After-lunch sessions are always challenging, especially when the conference is held in France, but Maurice's talk, entitled Applications of Shellable Complexes to Distributed Computing, was the perfect digestive after an excellent lunch. In his talk, Maurice reviewed some of the ideas behind his award-winning application of tools from algebraic topology to distributed computing and then discussed some very recent results that will be presented at DISC 2010 in the paper Concurrent Computing and Shellable Complexes co-authored with Sergio Rajsbaum.

In her talk Taming Distributed Asynchronous Systems, Anca Muscholl delivered a good overview of many results and open problems related to  analysis techniques for distributed, asynchronous systems with two kinds of synchronization, namely shared variables and fifo channels. Anca has just received the prestigious CNRS silver medal for 2010 for computer science. Congrats to her!


The last invited talk I was able to attend was delivered by Frank S. de Boer, who gave a presentation entitled Dating Concurrent Objects: Real-Time Modeling and Schedulability Analysis. After giving the audience an overview of the CREDO project, Frank introduced a real-time extension of the concurrent object-oriented language Creol, and showed us how to analyze schedulability of an abstraction of real-time concurrent objects in terms of timed automata. He concluded the talk by telling the audience about techniques for testing the conformance between these behavioral abstractions and the executable semantics of Real-Time Creol in Real-Time Maude. I enjoyed the talk, and I think that Frank was successful in keeping his audience away from their laptops and in making the attendees resist the temptation of checking their email during his talk, which was one of his stated aims!

Addendum.  Holger Hermann's invited presentation is now available (in flash) from here. Enjoy!