February 2008 Issue of the BEATCS

Volume 94 of the Bulletin of the EATCS is now available on line, freely and to everybody as it should be.

Of course, you should read the two pieces that make up the concurrency column :-) In addition, apart from the contributions to the other columns in the Bulletin, I encourage you to have a look at A "big-ideas" approach to teaching Computation Theory , a contribution to the educational column by Arnold L. Rosenberg. I have not had time to mull over his proposal yet, but it is certainly worth thinking about it and contributing our two-cent worth to what is an interesting opinion on how to teach one of our flagship courses.

Let me encourage you to support the EATCS by becoming a member of that association. For a mere 25 € 30 € per year (25€ if you are also a SIGACT member), you will make sure that the EATCS can continue supporting TCS research as a whole.

What is the Shortest PhD Thesis in TCS?

Gmail's webclips feature alerted me to the availability of Edmund Landau's PhD thesis in English translation. The thesis is 13 pages, which is substantially shorter than any PhD thesis in CS I am aware of.

I suspect that PhD theses in mathematics are, by and large, shorter than those in TCS. What is the shortest PhD thesis in either subject you are aware of? (In the case of mathematics, let's restrict ourselves to modern times, but if anyone knows of a thesis that is shorter than Landau's I'd be interested in knowing the details.)

Here is my own contribution. Off the top of my head, I recall that Jay Loren Gischer's PhD thesis from Stanford (year: 1984; topic: the theory of pomsets; supervisor: Vaughan Pratt, see also here) was between 45- and 50-page long.

Abel Prize 2008

The Norwegian Academy of Science and Letters has decided to award the Abel Prize for 2008 to John Griggs Thompson, University of Florida and Jacques Tits, Collège de France. Thompson and Tits receives the Abel Prize “for their profound achievements in algebra and in particular for shaping modern group theory”.

The committee's citation can be read here. Thompson and Walter Feit are the authors of the famous Odd Order Paper, filling a whole issue of the Pacific Journal of Mathematics. Georges Gonthier is leading an effort that aims to produce a computer-checked proof of this famous result in group theory.

The Usefulness of Bisimilarity Checking in Practice

I am collecting information as well as opinions on the practical usefulness of bisimulation checking. I feel that there are disparate views out there and they may be worth recounting. I plan to solicit opinions from experts in the verification community, but I am also interested in the thoughts on this topic of the readers of this blog. Feel free to email me your opinions or to post a comment. I would also appreciate receiving bibliographic references where the usefulness of bisimulation checking and bisimulation minimization are discussed.

Thanks in advance!

Accepted Papers for LICS 2008

The list of accepted papers for LICS 2008 is now available here. Some of the accepted papers that, judging by their titles, ought to be of interest for a concurrency theorist are the following ones.

- Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye and Marcus Groesser. Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata

- Taolue Chen and Wan Fokkink. On the Axiomatizability of Impossible Futures: Preorder versus Equivalence

- Ivan Lanese, Jorge A. Perez, Davide Sangiorgi and Alan Schmitt. On the Expressiveness and Decidability of Higher-Order Process Calculi

- Emmanuel Beffara. An Algebraic Process Calculus

- Tomas Brazdil, Jan Kretinsky, Antonin Kucera and Vojtech Forejt. The Satisfiability Problem for Probabilistic CTL

- Sam Staton. General Structural Operational Semantics through Categorical Logic

I'll try to find some time to write a few lines on at least some of them when they are available on line.

Axiomatizing Restriction and Relabelling

Time flies somehow. At some point in late February I posted the following paper:

Luca Aceto, Anna Ingolfsdottir, Bas Luttik and Paul van Tilburg. Finite Equational Bases for Fragments of CCS with Restriction and Relabelling. Technical Report CSR-08-08, TU/Eindhoven, February 2008.

I meant to write a blog entry on the paper then, but that intention has not materialized until now.

So what is the above study about? We investigate the equational theory of several fragments of Milner's CCS modulo (strong) bisimilarity with special attention to restriction and relabelling. The largest fragment we consider includes action prefixing, choice, parallel composition without communication, restriction and relabelling. We present a finite equational base (i.e., a finite ground-complete and omega-complete axiomatisation) for it, including the left merge from ACP as auxiliary operation to facilitate the axiomatisation of parallel composition.

Perhaps surprisingly, no complete axiomatisations of bisimilarity over languages including restriction and relabelling have been given to date. In a classic paper, Milner studied an algebra of flowgraphs with operations of (parallel) composition, restriction and relabelling, and provided a complete axiomatisation for it. In that reference, however, the notion of equivalence between expressions is purely “structural”, since two expressions are equated when they denote the same flowgraph up to isomorphism.

I hope that some of you will find the paper worth looking at. I enjoyed working on it a lot, thanks to my co-authors.

Four IFIP Scholarships for ICALP 2008

IFIP TC1 has kindly provided sponsorship for four 500-euro scholarships. The four scholarships will be used to support participation in ICALP 2008 by young researchers from countries where access to funds is limited by covering registration and some of the local expenses. Preference will be given to PhD students presenting papers at the conference.

To apply for one of the IFIP scholarships, please send an email to the address icalp08 AT ru DOT is. The application should be sent by Wednesday, 30 April 2008, at 12:00 GMT, and should contain a motivation for the sponsorship request together with an indication of whether the applicant is a co-author of one of the papers selected for the conference.

Proving Non-finite Axiomatizability Results Via Reductions

I recently completed the writing of two papers before the final rush towards ICALP 2008. The first of these papers, in chronological order, is

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir and MohammadReza Mousavi. Lifting Non-Finite Axiomatizability Results to Extensions of Process Algebras. Technical Report CSR-08-05, TU/Eindhoven, February 2008.

The general setting for the work reported in this paper is that of process algebras, which are prototype languages for the description of reactive systems. Since these languages may be used for describing specifications of process behaviour as well as their implementations, an important ingredient in their theory is a notion of equivalence or approximation between process descriptions. The equivalence between two terms in a process algebra indicates that, although possibly syntactically different, these terms describe essentially the same behaviour. Behavioural equivalences are therefore typically used in the theory of process algebras as the formal yardstick by means of which one can establish the correctness of an implementation with respect to a given specification.

In the light of the algebraic nature of process algebras, a natural question is whether the chosen notion of behavioural equivalence or approximation can be axiomatized by means of a finite collection of equations. The first negative results concerning finite axiomatizability of process algebras go back to the Ph.D. thesis of Faron Moller. Since then, several other non-finite axiomatizability results have been obtained for a wide collection of very basic process algebras; see here for a survey of such results dated mid-2005.

In general, results concerning (non-)finite axiomatizability are very vulnerable to small changes in, and extensions of, the formalism under study. Furthermore, proofs of non-finite axiomatizability results in the concurrency-theory literature are extremely delicate, rather long and error-prone. Hence, it would be useful to find some general techniques that can be used to prove non-finite axiomatizability results. Such a general theory would allow one to relate non-finite axiomatizability theorems for different formalisms, and spare researchers (some of) the delicate technical analysis needed to adapt the proofs of such results. The search for such general results is what inspired our research leading to this paper.

In the aforementioned paper, we present a theorem offering a general technique that can be used to prove non-finite axiomatizability results, and present some of its applications within concurrency theory. In this theorem, we give sufficient criteria to obtain new non-finite axiomatizability results from known ones.

The technique we propose is based on a variation on the classic idea of reduction mappings, which underlies the proofs of many classic undecidability results in computability theory and of lower bounds in complexity theory. In this setting, reductions are translations between languages that preserve sound (in)equations and (in)equational proofs over the source language, and reflect families of (in)equations responsible for the non-finite axiomatizability of the target language. In other words, the existence of a reduction shows that

• "nasty" families of (in)equations over the target language are also present in the source language, and
  
• if they were provable by means of a finite collection of valid (in)equations in the source language, they would also be "finitely provable" in the target language.
  

We show the applicability of our reduction-based technique by obtaining seven, to our knowledge novel, non-finite axiomatizability results for timed and stochastic process algebras. We also investigate some limitations of our approach. In particular, we show that prebisimilarity is not finitely based over CCS with the divergent process Omega, but that this result cannot be proved by a reduction to the non-finite axiomatizability of CCS modulo bisimilarity.

There are a few promising areas of further research in this area, and we are currently exploring some of them (ICALP organization and other tasks permitting).

I'll write a few lines on the second paper soon, but those of you who are interested in looking at it may find it here.

CS/Math Blogging and Social Skills

A very recent post by David Eppstein discusses the risks untenured academics may run into when blogging. David mentions the following typical quote: “pretenured professors should be aware of the risks of blogging and develop strategies to avoid or mitigate the pitfalls of blogging without a tenure net.”

I have the feeling, however, that at times what is needed is not the development of strategies for "safe blogging", but rather an appreciation of the fact that academics live in a society of peers, and that social skills and tact are needed for most of us to thrive in the scientific community. When supervising budding academics, we focus a lot on their scientific development, and rightly so. I am starting to believe, however, that at the same time we should pay more attention to the development of their "social skills". Being able to maintain a good working relationship with one's colleagues is a definite plus at work. Being perceived as an arrogant oddball typically isn't. Spurting gratuitous vitriolic remarks may be even funny in the very short term, but I believe that it soon becomes tiring.

We are part of a community, and a certain amount of respect for the work of our peers is healthy, if not altogether necessary, for the proper working of our society. I do not think that it is a proper thing to do to refer to one's colleagues as "losers" or to conferences as "worthless". We are all in this business to try and offer our modest contributions to (theoretical) computer science. Some of us are definitely more successful than others, but we (and most of our scientific conferences and journals) all have a role, no matter how tiny, to play. When a conference or workshop is not playing a useful role for the community it addresses, either it stops running or it redefines its scope.

Sheer arrogance serves neither the community as a whole nor the individuals who exhibit it. It will lead us nowhere. We should teach our students to exercise their freedom in judging their future colleagues with care, and make them aware of the dangers of considering themselves geniuses who are not bound by the minimal social conventions that apply to most common mortals. In fact, reading the blogs of, or talking to, scientists whose work I admire, I have always been struck by their courtesy and professionalism. We should all learn from their good example.

As an aside, Timothy Gowers, in his lovely little book "Mathematics: A Very Short Introduction", writes:

It is my impression, and I am not alone in thinking this, that, among those [the mathematicians] who do survive the various culls, there is usually a smaller proportion of oddballs than in the initial student population.

While the negative portrayal of mathematicians may be damaging, ...., the damage done by the word 'genius' is more insidious and possibly greater.....

The last quality [exceptional strategic ability] is, ultimately, more important than freakish mental speed: the most profound contributions to mathematics are often made by tortoises rather than hares.

I strongly recommend the book. It is really well written.

ACM SIGPLAN Third Workshop on Programming Languages and Analysis for Security (PLAS 2008)

Úlfar Erlingsson has asked me to advertise this event. So, here is the CFP. Do submit! Submission Deadline: March 24, 2008.



ACM SIGPLAN Third Workshop on
Programming Languages and Analysis for Security (PLAS 2008)

Tucson, Arizona, June 8, 2008

Sponsored by ACM SIGPLAN
Co-located with PLDI '08
Supported by IBM Research and Microsoft Research

http://research.ihost.com/plas2008/

Submission Deadline: March 24, 2008

Second Call for Papers

PLAS aims to provide a forum for exploring and evaluating ideas on the
use of programming language and program analysis techniques to improve
the security of software systems. Strongly encouraged are proposals of
new, speculative ideas; evaluations of new or known techniques in
practical settings; and discussions of emerging threats and important
problems.

The scope of PLAS includes, but is not limited to:

* Language-based techniques for security
* Verification of security properties in software
* Automated introduction and/or verification of security enforcement
mechanisms
* Program analysis techniques for discovering security vulnerabilities
* Compiler-based security mechanisms, such as host-based intrusion
detection and in-line reference monitors
* Specifying and enforcing security policies for information flow
and access control
* Model-driven approaches to security
* Applications, examples, and implementations of these techniques


Important Dates and Submission Guidelines

* March 24, 2008: Submission due date
* April 21, 2008: Author notification
* May 12, 2008: Revised papers due
* May 30, 2008: Student travel grant applications due
* June 8, 2008: PLAS 2008 workshop

We invite papers of two kinds: (1) Technical papers about relatively
mature work, for "long" presentations during the workshop, and (2)
papers for "short" presentations about more preliminary work, position
statements, or work that is more exploratory in nature. Short papers
marked as "Informal Presentation" will only have their abstract
printed in the proceedings. All other papers will be included in the
formal proceedings and must describe original work in compliance with
the SIGPLAN republication policy. Page limits are 12 pages for long
papers and 6 pages for short papers.

Student Travel Grants

Student attendees of PLAS can apply for a travel grant (in addition to
any PLDI grants), thanks to the generous support of IBM Research and
Microsoft Research. The application forms are on the workshop Web site.


Program Organization
* Úlfar Erlingsson, Reykjavík University, Iceland, Program Co-Chair
* Marco Pistoia, IBM T. J. Watson Research Center, Program Co-Chair

Program Committee
* Gilles Barthe, INRIA Sophia-Antipolis, France
* Bruno Blanchet, École Normale Supérieure, France
* Andy Chou, Coverity, USA
* Mads Dam, Royal Institute of Technology, Sweden
* Úlfar Erlingsson, Reykjavík University, Iceland
* Heiko Mantel, Technische Universität Darmstadt, Germany
* Isabella Mastroeni, Università di Verona, Italy
* Greg Morrisett, Harvard University, USA
* Andrew Myers, Cornell University, USA
* David Naumann, Stevens Institute of Technology, USA
* Marco Pistoia, IBM T. J. Watson Research Center, USA
* Eijiro Sumii, Tohoku University, Japan
* Dan Wallach, Rice University, USA

The Importance of Being Mobile

A comment on this post reads:

....the musical chairs that us academics play in our careers serves to disseminate our knowledge.

I agree that mobility is important in the career of most academics. Indeed, most of us have studied and worked at several institutions.

I was reminded of this comment yesterday, when I was asked to fill in a EU questionnaire on the mobility of researchers. One of the multiple-choice questions on the form read: "How often should a researcher move at different stages in her/his career?" (I was asked to answer this question since I claimed that mobility is important in the career of a researcher.) For instance, how often should one move over a four-year period at the early stages of one's career? I assumed that this question was referring to the first four years after one's PhD, and my answer off the top of my head was 1-2 times. (What I really meant was twice, but I thought 3-5 times was too much; the rationale being that one should be mobile at that crucial time in one's career, but that being overly mobile might cause too much overhead---especially if this involves changing countries. Later I looked back at my movements in the period 1991-1994 and realized that I actually moved 5 times myself.)

What is your opinion? Is mobility important at all stages of one's career? And how often should a researcher be mobile during the first four years of one's career?

Sussex[[Matthew Hennessy = goto Trinity.Continue]]

I apologize for the nerdy title for this post. I just thought that the most appropriate way to summarize the message of the post was to use a "Dpi process". Why? Because Matthew Hennessy, my former PhD supervisor and mentor, and the prime mover behind the development of Dpi has recently left my British alma mater, the University of Sussex, and joined the Department of Computer Science at Trinity College Dublin.

The news was unexpected for many of us, even though Matthew had been contemplating a move for a while. A look at the list of academic staff members of the School of Informatics at Sussex tells me that the diaspora of the group of TCS people I shared my Sussex days with, and that Matthew was instrumental in building, is now complete.

I wish Matthew the best of luck for his life and work at Trinity. As for Informatics at Sussex, I am not so sure that they are looking forward to the results of the RAE 2008. I wish them luck too, but they have lost so many truly excellent researchers over the last few years that I feel they may need more than luck, even though they seem to have hired rather well. Time will tell.

EATCS Award 2008 to Leslie Valiant

The EATCS Award 2008 will go to Leslie Valiant. You can read the motivation prepared by the Award Committee.

The award will be assigned during a ceremony that will take place in Reykjavik (Iceland) during ICALP (July 6-13, 2008). Leslie Valiant will contribute an invited talk to the event. This is yet another reason for not missing the conference!

BTW, the deadline for submitting to ICALP is approaching. Make sure you have your submissions in by Sunday, 10 February at 23:59 GMT.

I look forward to meeting you in Reykjavík, and to enjoying a scientific feast with the conference participants. Well, probably we organizers won't have that much time to enjoy the event, but we'll try :-)

Addendum (16 February 2008): See also this post by Bill Gasarch on the Complexity Blog. (Make sure you read the beautiful comment by Janos Simon.) You might also want to read the post on bit-player, which links to a very interesting piece on Leslie Valiant's work on holographic algorithms, which was the subject of a column in American Scientist.

ACM Turing Award 2007 to Clarke, Emerson and Sifakis

Via the Geomblog, I have just learned that ACM has named Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis the winners of the 2007 A.M. Turing Award for their original and continuing research on model checking. You can read the ACM press release here. This is, of course, outstanding news for the concurrency-theory and the computer-aided-verification communities, and I am looking forward to inform my students about the motivations for this award next time I preach on the importance of temporal logics as specification formalisms in computer science and on model checking and implementation verification.

Normally, I feel that I would have to write a few more lines on model checking in a post like this, but, with a couple of upcoming deadlines, I am very glad to see that Ganesh Gopalakrishnan has done all the work for me on Suresh's blog :-) (Thanks to both of them!) Let me just add that the basic idea underlying model checking can be concisely and memorably summarized by means of an equation that I first saw stated in a set of slides for a talk delivered by Moshe Vardi:

model checking = graphs + logic + algorithms.

Indeed, in model checking we use automata of some kind---that is, (labelled) graphs---to represent (an abstraction of) the actual behaviour of computing systems, (temporal) logics to describe what properties we expect systems to afford, and we employ algorithms to check whether the automaton representing the behaviour of the system has the desired properties at the press of a button. (Alternatively, one can say that we check whether the automaton is a model of the formula describing the specification; hence the name model checking for this verification and validation technique.) As remarked by Ganesh in his perspective on model checking, model checking tools and techniques and now being increasingly used in many other areas apart from system verification and validation. Decision processes, reliability models, planning in AI, optimal scheduling, (on-line) model-based testing and analysis of GUIs are just a few areas of application of model checking. I expect that more will emerge in the near future.

I am particularly happy about this award because, as I hope I have convinced you with the short and oversimplified account above, model checking is an area of TCS where both volume A and volume B TCS play a fundamental role. Moreover, teams working on model checking have produced software tools that can be used to sneak in TCS ideas in first-year courses for CS and engineering students, thus awakening the students' interest in our beautiful area of scientific endeavour. What more can we ask for?

Congrats to Ed, Allen and Joseph!

Addendum (6 February 2008): Make sure you read Rance Cleaveland's guest post on the Complexity Weblog, and that you do not miss Paul Beame's very informative comment.

DBLP Complete Search

I often look at DBLP to find bibtex entries for papers and links to their electronic editions. Now that Holger Bast has produced CompleteSearch, one can use DBLP also as an after-lunch amenity to find more publication data for computer scientists and conferences/journals in the field.

Do you want to know who has published the most in, say, Theoretical Computer Science? Look here, and you'll find that Grzegorz Rozenberg has published a whopping 62 (!) papers in that journal. What about Information and Computation? A look at this page yields that Sanjay Jain is the top scorer with 19 papers. (That researcher also has 20 TCS papers.) Top scorer for JACM is Seymour Ginsburg with 23 papers, with Christos Papadimitriou second with 21 entries. A look at the page for LICS reveals that Moshe Vardi has published 22 papers in that conference, and he is way ahead of the rest of the pack.

I'll stop here, since I do not want to spoil the fun you might have playing with this new feature. Well done, Holger!

Advice for (Prospective) Graduate Students

A topic that is being increasingly covered in TCS blogs is that of giving advice to (prospective) graduate students and beginning researchers. (See, for instance, here, here or here.) This is a welcome development, and a very good way of using the medium for the benefit of an important component of our research community. (After all, young researchers are the future of research, aren't they?) In fact, I have no problem in admitting that I enjoy reading those blog posts or anything similar myself. I feel that I am still learning on the job every day, and that those pieces of advice remind me of things that I should keep in mind, but that I tend (consciously or unconsciously) to "forget". After all,

Advice is what we ask for when we already know the answer but wish we didn’t. (Erica Jong)

The latest few words of advice on research for graduate students I read have been penned down by Fan Chung. She addresses mostly combinatorialists, but what she says applies equally well to theoretical computer scientists at large. I like the fact that she stresses the collaborative nature of the research enterprise, and that she embraces one of my favourite hobby horses, viz. the Hardy-Littlewood rule: authors are alphabetically ordered and everyone gets an equal share of credit. She adds:

The one who has worked the most has learned the most and is therefore in the best position to write more papers on the topic.

(I had never thought in these terms myself, but yes that's true.) She also writes:

If you have any bad feeling about sharing the work or the credit, don't collaborate. In mathematics, it is quite okay to do your research independently. (Unlike other areas, you are not obliged to include the person who fund your research.) If the collaboration already has started, the Hardy-Littlewood rule says that it stays a joint work even if the contribution is not of the same proportion. You have a choice of not to collaborate the next time. (If you have many ideas, one paper doesn't matter. If you don't have many ideas, then it really doesn't matter.) You might miss the opportunity for collaboration which can enhance your research and enrich your life. Such opportunity is actually not so easy to cultivate but worth all the efforts involved.

I could not agree more. I will add Fan Chung's advice to the list of links I suggest to all my students and colleagues. Maybe you'd like to do so too.

Wolf Foundation Prizes for 2008

The Wolf Foundation has released the list of awardees of the Wolf Prizes 2008. Pierre Deligne and Phillip Griffiths, both of the Institute for Advanced Study, and David Mumford of Brown University, will share the 2008 Wolf Foundation Prize in Mathematics. (I note that the third of these mathematicians seem to be doing research with a high computational content these days!)

Claudio Abbado is one of the two recipients of an award in the arts. I did a quick-and-dirty Google search and it seems that none of the main Italian newspapers has devoted an article to this prize. Sadly, I am not surprised.

Concurrency Column for the February Issue of the BEATCS

I have just posted the concurrency column that will appear in the February 2008 issue of the Bulletin of the EATCS. This installment of the concurrency column is devoted to a double bill, as it offers the following two contributions:

• Part 1: Dynamic Spatial Logics: A Tutorial Survey by Luis Caires. [PDF]
• Part 2: Applying Concurrency Research in Industry: Report on a Strategic Workshop by Luca Aceto, Jos Baeten, Wan Fokkink, Anna Ingolfsdottir and Uwe Nestmann. [PDF]
  

The first piece is a survey devoted to spatial logics contributed by Luis Caires, one of the prime movers behind the development of this exciting kind of specification logics. Since the original work of Pnueli, (temporal) logics have been a prime formalism for the description of the behaviour of concurrent systems. Spatial logics are specification logics for describing the behaviour as well as the spatial structure of concurrent systems. Despite being only a fairly recent addition to the family of specification formalisms for concurrent computation, spatial logics are already the subject of a large literature reporting on a substantial body of non-trivial results. Luis Caires’s survey gives us a highly readable and welcome bird’s-eye view of this fast-moving subject.

The second contribution is a strategic report on applying concurrency research in industry. This non-technical article is one of the outcomes of the Workshop on Applying Concurrency Research in Industry, colocated with CONCUR 2007 in Lisbon, which I co-organized on behalf of IFIP WG1.8 “Concurrency Theory”. The essay tries to distil the contents of the presentations delivered at the workshop, and of the ensuing discussion, for the benefit of the concurrency community as a whole. I thank all the participants in the workshop for their contribution to the event. Special thanks go to the invited speakers (Vincent Danos, Hubert Garavel, Jan Friso Groote and Kim G. Larsen) for making the trip to Lisbon to share their considerable experience on this topic with us, and to Rance Cleaveland, Joost-Pieter Katoen, Moshe Vardi and Frits Vaandrager for providing their answers to the questions that the audience asked the invited speakers at the workshop.

I hope that you will enjoy these contributions, and that you will feel enticed to contribute to the ongoing discussion within the concurrency theory community.

Last, but not least, do contact me if you'd like to contribute a piece to the column!

Using Model Checkers in "Intro to OS" Courses

The advent of mature model-checking tools has made algorithmic model-based verification much more accessible to the average computer scientist/engineer. So much so that we can now teach first-year students to use model-checking tools by sweeping essentially all of the theory behind them under the carpet. See, for example, the very recent experience report:

Roelof Hamberg and Frits Vaandrager. Using Model Checkers in an Introductory Course on Operating Systems. Technical Report ICIS-R07031,
ICIS, Radboud University Nijmegen, December 2007.

I strongly recommend reading this report to anybody with even a passing interest in formal methods. It is well written, content rich, and presents material that can inspire many of us in the lecture room. I myself wish that the paper had been posted last August, when I was planning (at the last minute) a second-year course on Operating Systems. I would have used the authors' tips and teaching material then. Not to mention great quotes like:

“Programs are not released without being tested; why should algorithms be published without being model checked?” (Leslie Lamport)

Last November, on the spur of a sudden moment of inspiration, I did use the Uppaal model checker in a one-week intensive course on operating systems for engineering students, and the results were very encouraging.

Frits and his coauthor have done all of us a great service by making their material available on the web, and by sharing their experience with the rest of us. Let's expose our students to easy-to-use model checkers like Uppaal from the first year of the studies in CS and Engineering. This will also a increase the impact of research in formal methods. Several of the students taking my one-week course wrote in their course evaluation that they were glad to have been exposed to Uppaal, and that they think they will use the tool again in their future studies on, e.g., control systems. This indicates that, once students have seen how useful model checkers are, they will be enticed to use them later on when facing similar problems. Last, but not least, the mathematically inclined students may be motivated to carry out independent studies and (under)graduate research in formal methods and other areas of theoretical computer science.

Quoting from the concluding section of the paper:

“Why should algorithms be explained without the use of a model checker?”

Indeed, why not? It will be a good day for the construction of reliable software systems when our students will routinely simulate and analyze concurrent algorithms using model checkers. For the moment, let's share our teaching experiences following the example set by Frits and his coworker, and let's make model checking and logic permeate our undergraduate education as much as possible.

Author Contributions, Redux

Some time ago, I pointed out an article with a very detailed account of the authors' contributions. Here is another similar case I have just seen, via Galileo. (Look at the acknowledgements.) This makes me wonder whether it is standard practice in the medical literature to list what each of the authors contributed to a paper. Is it?

Knuth and Me (Guest Post by Sergey Kitaev)

Guest post by Sergey Kitaev, a very good colleague of mine from the combinatorics group at Reykjavík University.

To show the significance of Donald Knuth in my life, it would probably be enough to indicate that he introduced in 1969 the area of “permutation patterns” which is the field of my main research interest in combinatorics that I’m dealing with almost every day. However, while thinking on the subject, it comes to mind the personal communications with Knuth at Mittag-Leffler Institute at the beginning of 2005. In particular, after attending my talk on partially ordered generalized patterns, Knuth decided to include a result of mine in volume 4 of “Art of computer programming.” It is remarkable that Knuth was collecting information for this volume for over 40 years! However, this was not the thing I was offered Knuth’s famous $1.28 reward for. Unlike most other rewards, this one was not directly related to mathematics – I let Knuth know the middle name of Alexandr Kostochka that he recorded in his name database both in English and Russian (Knuth is able of writing things in Russian which he learned in college, and I find this to be impressive). In any case, stupidly enough, I refused taking the check from Knuth, which would be a nice souvenir as I realized later on; I simply told Knuth that it was a great pleasure for me to be helpful for him …

Addendum. A (permutation) pattern is a permutation of a totally ordered set. An occurrence of a pattern P in a permutation p is a subsequence of letters of p whose relative order is the same as that of the letters in P. As an example, the permutation 461352 has three occurrences of the pattern 321, namely the subsequences 432, 632 and 652.

The initial motivation for studying pattern avoiding permutations came from its connections with container data types in computer science. In 1969 Don Knuth pioneered this work by showing that the stack sortable permutations are exactly the 231-avoiding permutations.

A Free Journal-Ranking Tool

The latest issue of Nature feutures a news item reporting on a freely-available tool that can be used to generate citation statistics for papers, journals and countries. The SCImago Journal & Country Rank is a portal that includes the journals and country scientific indicators developed from the information contained in the Scopus® database. This platform takes its name from the SCImago Journal Rank (SJR) indicator, developed by SCImago, a Spanish data-mining and visualization group. This indicator is based on Google PageRank. This tool is a competitor to Thomson's Web of Science, and covers more journals (15,000 in lieu of 9,000) and 20-45% more records than the Web of Science.

The availability of this tool, as well as of Google Scholar of course, puts Thomson under some pressure. I think that this is welcome pressure. To see why, you might wish to read this editorial. Basically, the "impact factor" is one of the Gods of modern-day academia, together with "leadership" and a few other criteria not necessarily related to scholarship. It has "a strong influence on the scientific community, affecting decisions on where to publish, whom to promote or hire, the success of grant applications, and salary bonuses. " However, as claimed in the editorial, "members of the community seem to have little understanding of how impact factors are determined, and, to our knowledge, no one has independently audited the underlying data to validate their reliability." This is obviously undesirable.

I think that, for good or for worse, impact-factor-based evaluation of our research output is here to stay. However, when making decisions based on impact factor, citations and what not, I hope that deans, employers, funding agencies and rectors will consult several different sources and compare the results that they get. Moreover, I do hope that good, old-fashioned evaluation of the quality of one's work will not disappear altogether to be replaced by purely quantitative indicators.

For the moment, let's play with our new toy. In case you are interested here are the rankings of countries in computer science: all subjects, computational theory and mathematics, TCS (but as a subcategory of mathematics), logic (as a subcategory of mathematics) and mathematics as a whole.
Draw your own conclusions.

The Theoretic Centre of Computer Science

The latest issue of SIGACT News features a very entertaining piece entitled The Theoretic Center of Computer Science by Michael Kuhn and Roger Wattenhofer. This article is a "printed version of a frivolous PODC 2007 business meeting talk, held by the second author". It speculates on the central conferences and researchers in computer science, with emphasis on theory, and makes for excellent after-lunch reading. I recommend it to the readers of this blog.

In this post, I'd like to offer a couple of comments on the list of most central authors in computer science. First of all, how do Michael Kuhn and Roger Wattenhofer determine how central an author is? Here is the relevant excerpt from the paper.

Analogously to the construction of the Erdos number, we base our method on the co-author-graph. We then create the induced subgraph for each region of interest (PODC, STOC/FOCS/SODA, and computer science). For PODC, for example, this graph would only contain authors that have at least one PODC paper, and so on.

Other than in the construction of the Erdos number, we do not rely on shortest paths, but rather on the PageRank idea: We start several short random walks at different nodes of the graph, and count how often each author gets visited. This idea is then extended to time dependent centrality, by starting the random walks only at authors that have published in the last five years.

What are the results of this approach? Table 1 on page 62 of the paper gives the most central authors for computer science as a whole. Alberto Sangiovanni-Vincentelli (another Italian expat) tops the all-time list, and Noga Alon is the runner-up. Without doubt, the list contains only major players, and concurrency theorists will be happy to see Moshe Vardi at #7 on the list of most "central" authors in computer science. Some analysis of this table is provided in the paper. Here are a couple of quick thoughts and questions from yours truly.

• Computer scientists working in the area of databases feature prominently in the all-time most central authors in CS. Indeed, a look at the list of researchers with the largest number of entries in DBLP, the data set used by the authors, shows that some of the most prolific authors in CS work in that area. Could it be that people publish more and have more coauthors in the field of databases, broadly construed, than in other areas of CS?
  
• The list of most central authors does not include any Turing award winner, as far as I can tell at first sight. Does this mean that Turing award winners are not central? Of course not! To my mind, this just means that an analysis of the collaboration graph favours prolific authors with lots of coauthors. Consider, by way of example, two giants of CS research like Tony Hoare and Robin Milner, who are not even in the list of top 1000 CS authors. (Neither are Stephen Cook, Don Knuth, Gordon Plotkin or Leslie Valiant to name but a few giants, by the way :-)) By modern standards, their "number of papers" is not outstanding. However, their ideas and writings have had, and still have, enormous impact on computer science research. All of what I have done myself, for instance, is built on their original work, which has kept many computer scientists busy for about thirty years. (Of course, Robin and Tony are not responsible for the noise I have generated myself :-)) These tables are a fun read, and they do tell us something worthwhile about the players in our subject. However, as the authors point out themselves, "Without doubt the future will teach our evaluations a lesson, ultimately revealing in which direction computer science evolves, and maybe even discover the most influential computer scientist. After all, research is not about how many papers we write, or how many citations they get, but rather, what the best contributions are."
• I think that the right-hand side of Table 1 is strongly influenced by the phenomenon of name ambiguity. Consider, for instance, Wei Wang, who is ranked as #2. When I saw that Wei Wang has 86 DBLP entries for 2006, I asked myself the question: "Who is Wei Wang"? This Google search return over 1.8 million entries! It seems to me that Wei Wang is a (very large) disciple of Bourbaki or Lothaire :-)
  
• Table 2 on page 62 is a veritable who's who in the FOCS/STOC/SODA branch of TCS. It has a truly amazing number of Israeli computer scientists (six out of ten on the "all-time" list, and four out of ten on the "last-five-years" list, I believe).

Enjoy!

AMS Prizes 2008

Via the Geomblog, I see that the list of AMS prizes for 2008 is out.

First of all, let me join the chorus of congratulations for Shlomo Hoory, Nati Linial and Avi Wigderson, who have been awarded the Levi L. Conant Prize for the best expository article in the Notices or the Bulletin of the AMS in the last 5 years. They received this prize, which is a great recognition for TCS research within the mathematical community, for their article Expander graphs and their applications in the Bulletin of the AMS.

As Nati Linial says in his response for the prize

I believe that the full potential impact of combinatorics on the rest of mathematics is only starting to reveal itself and the study of expander graphs can give us some idea of the true power of these connections.

Combinatorial research is also honoured with the Leroy Steele Prize for seminal contribution to research going to Endre Szemeredi for the paper On sets of integers containing no k elements in arithmetic progression, Acta Arithmetica XXVII (1975), 199–245. I love these words in Szemeredi's response:

This award could not have occurred were it not for the fundamental work of
other mathematicians who developed the field of additive combinatorics and
established its relations with many other areas. Without them my theorem is only
a fairly strong result, but no “seminal contribution to research”.

Calling his theorem a "fairly strong result" is really faint praise, but I like the fact that Szemeredi points out that a result becomes a seminal contribution to research when it used by other researchers to obtain fruits that were considered beforehand too high on the tree of knowledge to be picked.

The prize booklet makes for some interesting reading. Wearing my Italian expatriate's glasses, I note in particular the two awards to Italian mathematicians (Alberto Bressan and Enrico Bombieri) , both of whom work in the US.

I look forward to seeing who will be the recipient of the EATCS award for 2008.

The Dangers of Blogging

In this entertaining TED talk, Yossi Vardi issues a word of warning for the male bloggers out there, and addresses the "local warming" problem.

I know that this post is somewhat different in nature from my typical ones, but it's the first day of term and a little after-lunch entertainment was called for :-)

Enjoy!

Science Magazine's Breakthroughs of the Year 2007

Anders Claesson just alerted me to the fact that Solving Checkers has been listed by Science magazine in tenth position in the list of breakthroughs of the year 2007. See here.

My colleague Yngvi Björnsson from the School of Computer Science at Reykjavík University was a member of the team behind this breakthrough. Congratulations to Yngvi and his colleagues at Alberta.

A Good Example from Canada

I recently became aware of the Canada Research Chairs programme. That programme has been running since the year 2000, and aims at establishing 2000 research professorships—the so-called Canada Research Chairs—in universities across Canada by 2008. The Canada Research Chairs programme invests $300 million a year to attract and retain some of the world's most accomplished and promising minds.

I encourage the readers of this blog to have a look at the web site for the programme. There is a lot of interesting material there, and I cannot help but think that many countries would be well served by setting up a similar programme to attract the best possible scientists in all disciplines. Now, this is something well worth lobbying for in the coming year, isn't it?

If you do not have time to look at the web site I linked to above, here is my executive summary of the programme.

• Each eligible degree-granting institution in Canada receives an allocation of Chairs. For each Chair, a university nominates a researcher whose work complements its strategic research plan and who meets the program's high standards.

  Three members of a college of reviewers, composed of experts from around the world, assess each nomination and recommend whether to support it.

• Universities are allocated Chairs in proportion to the amount of research grant funding they have received from the three federal granting agencies: NSERC, CIHR, and SSHRC in the three years prior to the year of the allocation.

• There are two types of Canada Research Chair:

  Tier 1 Chairs, tenable for seven years and renewable, are for outstanding researchers acknowledged by their peers as world leaders in their fields. For each Tier 1 Chair, the university receives $200,000 annually for seven years.

  Tier 2 Chairs, tenable for five years and renewable once, are for exceptional emerging researchers, acknowledged by their peers as having the potential to lead in their field. For each Tier 2 Chair, the university receives $100,000 annually for five years.
  

As you can see, there is a strong financial incentive to attract people to these endowed chairs!


• Chairholders are also eligible for infrastructure support from the Canada Foundation for Innovation (CFI) to help acquire state-of-the-art equipment essential to their work.

• If an institution's performance decreases relative to other institutions to the extent that the next recalculation of Chair allocations results in that institution's allocation being reduced, the Chairs Secretariat will reclaim, as appropriate, one or more of its unoccupied Chairs. Should all of the institution's Chairs be occupied, the secretariat will negotiate with the university on how best to reclaim the lost Chair(s).

Of course, the success of a programme like this one should be measured by the quality of the people who take up the chairs. (Italy has a similar programme already in place. You can read about it in a short article in Nature, with commentaries in the blog posts "The Runaway Brains" and "Brain Drain and Brain Gain".) You can look up the chairholders in all disciplines here. A quick browse through the names of the Canada Research chairholders in Information Technology and Mathematics makes me pretty sure that you'll find outstanding people in your area of interest.

Wouldn't it be great if we could convince our own ministries for education, university and research to set up a Research Chairs programme along the Canadian lines? Let's see what the new year will bring, but I do not hold my breath. I am already doing so waiting for the result of the pending research grant applications .

I wish a happy and productive 2008 to all readers of this blog.

Workshop on Women in TCS

The department of CS at Princeton University is hosting a "Women in Theory" student workshop in Princeton on June 14-18, 2008. See http://www.cs.princeton.edu/theory/index.php/Main/WIT08 for more details and list of confirmed speakers. (Via in theory.)

I am happy to see an initiative like this. In fact, I believe that we should have more events that highlight the achievements of women in TCS and that offer prospective students role models that they can look up to.

During my student days in Pisa, I thought that it was very natural for CS classes to be attended by roughly an equal number of men and women. I also followed a good number of classes where lecturers or TAs were female members of staff. Back then, I never thought that computer science was a male-dominated subject, and I had no reason to think so. Only much later, did I realize that what I thought was the norm was, in fact, an exception and, by the time I taught a class in Aalborg that was being attended by only one female student out of about 50 registered students, the lack of women in CS was not a surprise to me any more.

It is still my impression that Italy has a fairly substantial number of female (theoretical) computer scientists---at least compared to countries in Northern Europe. People often ask me for the reasons behind this phenomenon, and I am always at a loss to try and explain it.

Do any of you have a good explanation why countries like France and Italy seem to suffer less than others from the lack of women in subjects like CS? Could it be that things are getting worse there too?

Computer Scientist: 21st Century Renaissance Man

The period from January till May each year is when faculty at the School of Computer Science at Reykjavík University try to make a determined effort to entice students to study our lovely discipline. (I know, we should do so all the year round, but somehow our good intentions do not become good deeds on a regular basis by themselves :-()

As part of our 2008 campaign, I have coauthored a short essay entitled Computer Scientist: 21st Century Renaissance Man. There is nothing particularly new in it, but I hope that it is readable and that it carries the message that CS is much more than most laypeople believe it is. Maybe some of you will find it useful for your own PR campaigns. Feel free to use it, if you think it may help.

You can draw some more inspiration from the items in our suggested-reading list. More essays of general interest may be found here. See also the excellent survey collection at Theory Matters.

Positions in Computer Science and Applied Maths at Reykjavík University

Some readers of this blog might be interested in the following job announcement. We are particularly interested in applicants in Computer Security, System Dependability, and related areas within the field of computer science. Moreover, Software Engineering is intended in a broad sense and we welcome applications from people working in, e.g., formal development techniques, model-based software development, and testing and verification.

In order to implement its ambitious strategy in research and teaching, the School of Computer Science at Reykjavik University seeks to hire faculty members for new academic positions. The following links point to pages with more detailed information about the vacant positions.

Applied Mathematics: http://hr.is/?PageID=6595
Computer Science: http://hr.is/?PageID=6596
Software Engineering: http://hr.is/?PageID=6608

In all cases, position levels can range from assistant professor to full professor, depending on the qualifications of the applicant. Salary level is negotiable and relocation assistance is offered. The position is available immediately, but later starting dates can be negotiated.

Informal communication and discussions are encouraged, and interested candidates are welcome to contact the Dean of the School of Computer Science, Dr. Ari K. Jónsson (ari@ru.is), for further information.

Registration for ICALP 2008 is Open

The registration page for ICALP 2008 and affiliated events went live yesterday evening at http://www.ru.is/icalp08/registration.html.

We have done our best to keep the registration fees as competitive as we possibly could. The prices on the registration form are in ISK, but, by way of example, the regular early fee for a non-ICALP participant to a one-day workshop is around 77 euros, which become roughly 56 euros for somebody who registers also for ICALP. The early registration fee for ICALP is a little below 380 euros (including the excursion).

If you know that you will attend ICALP 2008, as you should :-), I strongly encourage you to book your flights and accommodation early. July is prime holiday time in Iceland, and you are more likely to get a good deal on your flights if you book as early as you possibly can.

Let me end, in the style of Numb3rs, by noting that ICALP 2008 is

13 workshops
8 days
5 invited speakers
3 tracks
2 prize awards
1 conference.

Thanks to my co-organizer Magnús M. Halldórsson for pointing out this "ICALP for fun" countdown and that this is going to be a Fibonacci-like ICALP!

Ranking of Excellent European Graduate Programmes in Natural Sciences

This report of the Centre for Higher Education Development (CHE), which was released about a week ago, may be of interest to readers of this blog. The CHE is a think tank for higher education. Based on international comparisons, they develop models for the modernization of higher education systems and institutions.

Their report develops a Ranking of Excellent European Graduate Programmes in Natural Sciences (viz. biology, chemistry, mathematics and physics), which is intended as an orientation guide for undergraduates, helping them find their way around European Higher Education while at the same time helping them to choose a suitable university for their graduate studies: Master’s and PhD.

At first sight, the report looks very well done, and for an Italian expatriate like me it is good to see that Italian institutions are doing rather well. I'd like to see a similar analysis carried out for programmes in computer science.

Let me try and provide a few remarks on the CHE report. In passing, I'll also offer some personal conclusions related to what the findings of this report may mean for a country like Iceland, which has great ambitions despite its tiny population.

Let me start by focusing on one message from the report that I find most important here (quoted from page 14 of the report). While reading the following text, bear in mind that "subject areas" refers to biology, chemistry, mathematics and physics, and not to a huge array of different disciplines.

"Another interesting finding is the fact that most institutions (33) are selected in only one subject area, 15 in two subject areas, 4 in three and also only 4 in all subject areas. If, even in the relatively closely connected academic fields of the natural sciences and mathematics, only 14% of the very top institutions in one geographic region are featuring three or all four subject areas, this can indeed be taken as an argument against institutionwide rankings."

Even though I enjoy reading the results of university-wide rankings, I believe that what should concern students choosing where to pursue their studies and funding agencies determining where to invest their research funds in specific disciplines is not the overall ranking of a university, but rather its excellence in the specific topic of interest. For this reason, I agree with the finding that subject-specific rankings are much more informative than institution-wide ones.

Of course, in general, a university that scores highly institution-wide won't have any very weak department. However, there may be, and indeed there are, universities that have peaks of true excellence in specific areas, even though they may not be world-beaters in many areas. If I were a prospective PhD student, I would prefer going to study in a department which is known to be top-class in the specific area of my interest rather than going to university X just because it has a globally good reputation. Quoting from the report:

"Prospective doctoral students are possibly less interested in the general performance of a faculty or department than in a specific research group. They usually have very clear ideas about the specialised topic on which they are focusing. Thus, it might be of some value for a student searching for a biology doctoral programme specialising in insects to know that the faculty at University A is excellent in its research output in this domain. However, it might be much more interesting for this individual to
learn that he could delve into honeybee studies in Würzburg's bee group. Or, a student in astrophysics might be attracted less by the overall performance of the Physics Department at the University of Copenhagen than by its research group focusing on dark matter and cosmology."

So my first conclusion is:

Conclusion 1. Our business as academic institutions is reputation. It is better to be known in a few selected areas than to be unknown in many. Icelandic universities should prioritize and place more resources in those areas where they can maintain or build a strong reputation internationally. The competition is growing stronger by the day; nobody stands still and we will need many more resources in the future just to maintain our present standing where we have one.

The second point that I'd like to pick out from the report is the minimum entry requirement for even entering the evaluation. The 3000 ISI publications from a institution over the evaluation period are indeed a very tall order for any Icelandic institution at this moment in time. Sometimes we pat ourselves on the shoulders and tell each other how well we are doing, and for very good reasons. However, we should never lose sight of the "big picture". A very good practice for any scientist is to remain humble, to know that there is a lot one does not know, and to keep in mind that there are very many strong scientists and departments out there.

As Socrates famously put it, "A wise man is one who knows he does not know." In this setting, I would translate this statement into something like this:

Conclusion 2. A wise rector/dean/head of department is one who knows that her university/faculty/department will need to improve its research quality and output considerably just to maintain its present status, no matter what its present strength is. The only way to do so is to hire the best possible researchers, to give them the best possible working environment and the freedom to follow their research interests. Research output will need to be considered when distributing research money to ensure that the most funding goes where the highest "interests" (read "quality publications in internationally recognized outlets") will be generated.

Two of the indicators considered by the CHE Ranking are

• the percentage of international and female staff within the group of staff with a doctorate and
• the percentage of female and international doctoral and master's students.

I am afraid that, despite our snow queens, we score badly on both of these fronts. Ranking measurements aside, it is of paramount importance for science in Iceland to nurture female talent and to seek actively to hire the best available female applicants. Mind you, I am against hiring female applicants just because of their gender. What I am saying is that our departments should have search committees who actively nurture connections with the best possible female applicants for positions and that outstanding female applicants should be given precedence when they are at least as good as the competition. Here the ministry could also chip in with some financial incentives to universities to hire outstanding female applicants. (I won't turn this into a conclusion though )

One may wonder whether some research groups from Icelandic universities can make it into the big league. The answer to this natural question that emerges from the CHE report is, I believe, positive. Look at the bottom of page 12 in the report. There you will read:

"Looking at table 2, the United Kingdom not only attains the largest number of gold medals but also the largest number of medals in total within the excellence group. Switzerland, with only three universities in this group, is in third place concerning gold medals and holds the largest relative percentage of gold medals: 16 out of 22 medals in the whole."

This is an outstanding, and not unexpected, performance of Swiss institutions. In fact, ETH Zurich is one of only four universities with gold medals in all of the subjects in the excellence group (the others being Imperial College, the University of Cambridge and the University of Utrecht)! How can Switzerland achieve this outstanding level of academic achievement? Rather than trying to answer this question myself, I will rely on higher authority and freely quote a few excerpts from an interview to the Italian mathematician Alfio Quarteroni (professor at the Ecole Federale Polytechnique de Lausanne and at the Politecnico di Milano) published in this book.

• Switzerland has only two federal universities (ETH and EFPL).
• These are two truly international institutions. To wit, about 70% of their professors are foreigners, and so are about 65% of the PhD students and about 33% of their undergraduates.
• Each of the few and carefully chosen full professors in those institutions has the financial resources to build her own research team. For instance, Quarteroni's team has about 20 members. (As a curiousity, they helped build Alinghi, the boat that has won the last two installments of the America's cup.)
• Quarteroni roughly says: "EFPL offers outstanding environmental and quality conditions that I have not found elsewhere. I have worked at the University of Minnesota, at Paris VI and, for shorter periods, in about 50 universities and research centres throughout the world, including NASA at Langley; well, on the basis of my personal experience, Lausanne is the place where I have been able to realize my goals in the simplest, fastest and most efficient way."

Conclusion 3. I let you draw your own conclusions as to what we need to do here in Iceland in order to approach the lofty heights that those Swiss institutions as well as several universities in Finland, The Netherlands, and Sweden have managed to attain. The above opinions of Quarteroni's raise many questions which I hope Icelandic university administrators will be willing to answer.

RU in the Guardian Education

Colin Stirling pointed out this article in the Guardian Education to me yesterday. This article is going to generate a little publicity for my current institution (Reykjavík University) and we can certainly do with that! It is also certainly true that Icelandic (academic) institutions feature more women in leading positions than elsewhere, and that their wages are comparable to those of equally qualified male colleagues. However, I am not so sure that Iceland is a particularly good example of a country that attracts good numbers of female students and members of staff in science and technology. We still have far too few women enrolling in computer science degrees, for instance, and my department employs one female professor and two female assistant professors. (Yes, we now have English web pages!) We will need to work very hard to try and change this situation, and this is one of our tasks for the future as far as recruiting is concerned both at student and staff level.

But enough grumping, let's enjoy our five minutes of fame in the British media, even though, as my rector Svafa Groenfeldt wrote to me,

"The interview was ok but as always the journalists take a bit of an artistic license when they quote what we said :-)"

A Cancellation Theorem for BCCSP

Wan Fokkink, Anna Ingolfsdottir and I have recently completed the paper A Cancellation Theorem for BCCSP, which is now available from the web page where Anna and I collect our papers.

The aim of this paper is to prove a cancellation result for the language BCCSP modulo all the classic semantics in van Glabbeek's linear time-branching time spectrum. The statement of this result is as follows.

Theorem. Let t and u be BCCSP terms that do not contain the variable x as a summand. Let <= be a preorder in van Glabbeek's spectrum. If t+x <= u+x then t <= u.

Apart from having some intrinsic interest, this cancellation result plays a crucial role in the study of the cover equations, in the sense of Fokkink and Nain, that characterize the studied semantics.

Fokkink and Nain proved the instance of the above theorem for failures semantics, with the aim to obtain an ω-completeness result for this semantics; their proof is rather delicate. To the best of our knowledge, failures semantics has so far been the only semantics in the spectrum for which the above result has been published. In our paper, we provide a proof of the above-mentioned property for all of the other semantics in the linear time-branching time spectrum. Despite the naturalness of the statement, which appears obvious, these proofs are far from trivial (at least for yours truly), and quite technical. I myself was really surprised by the amount of work we needed to do to prove such an "obvious" statement. (In case you wonder, the "obvious" statement is false in general. Consider, for instance, an algebra with carrier {0,1} and where the sum of any two elements is 1. Then the inequation y+x <= z+x holds, but y <= z obviously does not.)

I hope that some of the readers of this blog will find the paper worth reading. The techniques used in the proof of the cancellation theorem may also have some independent interest.

Accepted Papers at FOSSACS 2008

The list of accepted papers for FOSSACS 2008 is out. I was in the PC for the conference, and I have to say that this year the number of very good submissions was substantially higher than the number of slots. (And this without counting the papers with which I had to declare a conflict of interests.)

Looking at the accepted papers, it is striking how many of them have French authors. In fact, France was the country with the largest number of authors of submitted papers this year (67 to be precise) , and the acceptance ratio for papers co-authored by French authors was high. By way of comparison, the country that had the second largest number of authors was the US with 29. Germany, Italy and the UK were roughly on a par with the US.

French TCS is hot, judging by these figures. LSV alone contributes at least five papers to FOSSACS 2008. This is quite a way of celebrating their tenth anniversary.

ACM Fellows - 2007

I just had a look at the list of ACM Fellows for 2007. It has been a good year for TCS, and even concurrency theory and computer-aided verification are well represented in the list. Congratulations to Rajeev Alur, Lance Fortnow, Georg Gottlob, Rajeev Motwani, Amir Pnueli and all the other the new fellows.

On the subject of awards, I yesterday saw the call for nominations for the first CAV award. I have at least one person that I'd really like to nominate, but since I would prefer that person to be in cool Reykjavík for ICALP 2008 instead of sultry Princeton for CAV 2008, I guess I'll have to wait for one year before sending in my nomination :-) Who would you nominate for such an award? Note that

The cited contribution(s) must have been made not more recently than five years ago and not over twenty years ago. In addition, the contribution(s) should not yet have received recognition via a major award, such as the ACM Turing or Kanellakis Awards.

Unfortunately, the CAV organizers decided to fix the dates for their conference so that they coincide with the dates for ICALP 2008, which were known long before theirs. Time will tell whether this was an inspired decision on their part.

ICALP 2008: Second Call for Papers

The second call for papers for ICALP 2008 has just been posted to several mailing lists. The chances are that your mailboxes will be flooded by a good number of copies of the call for papers, but, in case this does not happen, you have been notified via this post :-) (In fact, I was quite amazed to discover that this modest blog is featured in the Theory of Computing Blog Aggregator, and so the odd post of mine might even be read by a CS theorist or two.)

In fact, submissions to ICALP 2008 are already open! To submit, please follow this link. Registration for the conference and affiliated workshops will be open very soon, allowing prospective participants to book flights and accommodation at a decent price. Iceland is a hot tourist destination in July.

ICALP 2008: Co-located Events

The list of events that will be co-located with ICALP 2008 (6-13 July, Reykjavík, Iceland) is now available. We received a record number of workshop proposals, and the number of affiliated events witnesses the interest in visiting the land that hosts me right now.

A second call for paper for ICALP 2008 will be posted very soon. Sharpen your pencils, and submit your best paper to the conference!

10 Years of Verification in Cachan: Part I

On November 26 and 27, Anna and I were in Paris for 10 Years of Verification in Cachan, a two-day workshop organized by the Laboratoire Spécification & Vérification (LSV) of the ENS Cachan to celebrate its 10th anniversary. The workshop was centered around two special award ceremonies honouring two very good colleagues and friends of ours: Patricia Bouyer received CNRS's 2007 Bronze Medal for Computer Science (Monday 26th November), and Kim G. Larsen became Doctor Honoris Causa at ENS Cachan (Tuesday 27th November).

Despite being very busy and getting nowhere fast, we felt that we really ought to make the trip to Paris for this event, to which the organizers had kindly invited us to contribute talks. We were visiting professors at LSV in May 1998, when that laboratory was in its infancy, and we have very fond memories, both scientifically and socially, from that stay. In fact, our connection with LSV started informally long before that time when François Laroussinie and I shared an office in Aalborg for about a year starting from the autumn 1994 (when BRICS started its activities).

Today, there is little doubt that LSV is one of the hotbeds of TCS research in the Paris area, where there is really no shortage of talent and of extremely strong CS departments covering the whole gamut of TCS research. According to Philippe Schnoebelen, the present director of LSV, the centre now has about 40 members, and since its inception it had graduated 33 PhD students, seven of whom have been hired by CNRS. This is just one of the many indications of the success achieved by LSV over the first ten years of its existence. To my mind, another definite sign of impact is the number of former members of the laboratory who have taken up high-profile academic positions elsewhere. Here is what I could find on the LSV web site.

• François Laroussinie has become a full professor at University Paris-Diderot (Paris 7).
• Ralf Treinen is a full professor at University Paris-Diderot (Paris 7).
• Hubert Comon-Lundh is on sabbatical leave at RCIS (AIST, Tokyo).
• Michel Bidoit is the Director of INRIA Futurs.
• Antoine Petit is the director of INRIA Paris-Rocquencourt.
• Béatrice Bérard is a full professor at University Paris-Dauphine.

The workshop was a really enjoyable event. We had a great time, listened to some excellent talks, met a lot of colleagues and friends, and tasted some very good food. The organization was simply superb, thanks to the sterling efforts of Philippe Schnoebelen, Thomas Chatain, and Stéphanie Delaune.

Apart from my presentation, which ended the event, the two-day workshop featured talks by André Arnold, Pierre Wolper, Kim G. Larsen, Claude Kirchner, Marta Kwiatkowska, Michel Bidoit, Patricia Bouyer, Anna Ingólfsdóttir, Wolfgang Thomas, and Colin Stirling. This was really an embarrassment of riches, and I learned a lot from all of the talks---even from the two delivered in French :-) The quality of the presentations by these colleagues was invariably high, and the talks offered very accessible introductions to several areas of research covered by the members of LSV.

It would take way too long to report on all of the presentations. In this post and in subsequent ones, I'll therefore limit myself to recalling a few opinions and trivia that I heard at the workshop.

In his talk 25 years of automata and verification, Pierre Wolper went on record as saying that "Complexity, as traditionally measured, is not very relevant in verification." To wit, in his talk he pointed out that verification algorithms with high worst-case complexity turn out to perform well in practice and are widely used. Prime examples are automata-theoretic algorithms for LTL model checking as well as those implemented in the tool MONA, which implements decision procedures for the Weak Second-order Theory of One or Two successors (aka WS1S/WS2S)---a theory that is not elementary-recursive, as shown by Albert Meyer in this seminal paper. On the other hand, he presented an example from his own work yielding efficient automata-theoretic algorithms for CTL model checking, which are not used in practice. His conclusion was that one cannot trust complexity results. (I myself have mixed feelings about this opinion of Wolper's. Maybe I'll devote a post to this topic when life is less hectic. In the meantime, I'd love to hear your opinion.)

Pierre Wolper also said that his LICS 1986 paper An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report) with Moshe Vardi, which eventually won the LICS Test-of-Time Award and formed the basis for their paper that won the Gödel prize in 2000, had been rejected by two or three conferences before being accepted at LICS 1986! He also recalled the following sequence of reactions by Gerald Holzmann to their automata-theoretic algorithms for LTL model checking:

1. "It must be wrong!"
2. "It is impractical!"
3. "It does not fit into SPIN!"

Eventually, the algorithm was implemented in SPIN, showing the power of elegant ideas in practice.

At the end of his talk, Pierre called for renewed efforts in implementing automata. I keep telling my students that automata are the most basic computational model in computer science, and I cannot help but share Pierre's call to arms.

I hope to report on a few other talks from the workshop when I have managed to catch up with a few of the items on my to-do list.