CS@Aalborg University: Research evaluation 2011-2015

Every five years, the Department of Computer Science at Aalborg University undergoes a research evaluation. The purpose of this exercise is to provide the department with qualified and independent opinions on its "actual research topics, results, and performance, but also on strategic issues like funding, internal organization and synergies, possible new directions, collaboration with industry, internationalization, positioning IT as a key enabler in society, etc." So the overall aim is to improve the quality and impact of the research carried out within the department.

The evaluation committee for the period 2011-2015 consisted of Peter Apers (University of Twente, the Netherlands), Jan Gulliksen (KTH Royal Institute of Technology, Stockholm, Sweden), Chris Hankin (Institute for Security Science and Technology and Imperial College, UK), Heikki Mannila (Aalto University, President of the Academy of Finland, Finland) and Torben Bach Pedersen (Aalborg University, Denmark), who was the internal member and chair of the committee.

The report resulting from the latest such evaluation has recently been released and can be found here. The editors of the report were Manfred Jaeger, Jesper Kjeldskov, Hua Lu and Brian Nielsen. As a former editor of such a report in days long gone, I know that their job required a considerable use of time and effort.

So, what did the evaluation committee have to say? Quoting from its evaluation of the department as a whole,

"The Computer Science Department has two world-class groups and excellent staff in all groups. The Danish IT benchmarking exercise of 2014 shows that the Department is the best department in Denmark for number of refereed publications and BFI points per full-time faculty member. The Department is also top in a number of other metrics. During the review it was also reported that Aalborg Computer Science graduates are highly prized by industry. The Department thus deserves to be ranked even higher in the QS World University Rankings by Subject or the Academic Ranking of World University (ARWU \Shanghai") Subject ranking. The current rankings are to a large degree caused by the poor coverage of computer science publications in the commercial bibliometric indices used in these rankings (WoS, Scopus). Here, Google Scholar provides a much better coverage. However, the Department clearly has the potential to rise considerably in these rankings but will require support from the Faculty and University to achieve this."

The two world-class groups mentioned in the above quotation are the Database and Programming Technologies and the Distributed and Embedded Systems units. (The latter is now called Distributed, Embedded and Intelligent Systems unit as it now also includes researcers from what used to be the Machine Intelligence group.) Those two groups are led by the Danish computer scientists with the highest h-index, and have a truly impressive publication and grant-winning record.

You can find the committee's evaluations for each of the research groups in the report. Here I'll limit myself to mentioning an excerpt of what the committee wrote about the Distributed and Embedded Systems unit, where I had the pleasure to work for ten years.

"The Distributed and Embedded Systems group is a world-class group. It is involved in a broad range of activities from semantic foundations through tool development for verification and validation to real-world applications. The group is making excellent contributions across the whole spectrum of activity; this is internationally recognized by prestigious awards such as:

• The ERC Advanced Grant LASSO
• The 2013 CAV Award for Uppaal - the first time that this award has been granted to a non-US team
• The ranking of  "Uppaal in a Nutshell" as the 9th most influential paper in Software Engineering since 1972
• Best paper awards, medals and other awards to Associate Professors

The h-index of Kim Guldstrand Larsen is outstanding and places him among the top echelon of researchers in this area; his h-index is higher than some Turing Award winners in cognate areas. It is also pleasing to note that some of the Associate Professors also have high h-indices for their career point. .....

The group has published well during the review period with 175 conference papers - 75% of which are in A and B venues - and 63 journals - 92% of which are in A and B venues. .....

The group has secured 37 new grants to a total value of DKK103.8M. ....

The major strength of the group is the people; not only the group leader but the strong group of more junior academic staff and an excellent group of support staff. The broad span from foundational work to applications is also unusual in such groups in other universities and is a considerable strength of DES. The profile and reach of the group is enhanced by its dissemination activities but also the engagement of senior staff in policy-related activities at national and European levels."

Of course there is still a lot of room for improvement, but this will require support from the university as a whole, high-profile new hires in the future and the development of the talent the department already boasts. However, the opinion of the evaluation committee clearly highlights the current strength of a CS department that, in my admittedly biased opinion, deserves to be better known worldwide.

Zoltán Ésik (1951-2016): In Memoriam

The following obituary for Zoltán Ésik will appear in the October issue of the Bulletin of the EATCS and on the web page of Academia Europaea.

Zoltán Ésik (1951-2016)

In Memoriam 

Luca Aceto and Anna Ingólfsdóttir

ICE-TCS, School of Computer Science, Reykjavik University

Our friend and colleague Zoltán Ésik passed away in Reykjavik, Iceland, on Wednesday, 25 May 2016. He was visiting us as he did with some  regularity, compatibly with his many engagements throughout the world. 

The day before his untimely death, Zoltán had delivered an ICE-TCS seminar entitled Equational Logic of Fixed Point Operations at Reykjavik University. At the start of his talk, he looked somewhat tired and out of breath. However, the more he was presenting a research topic that he loved and that has kept him busy for most of his research career, the more he seemed to be feeling at ease. After the talk, we spent some time making plans for mutual visits in the autumn of 2016 and we discussed some EATCS-related matters. His wife Zsuzsa and he were due to spend a few days travelling in the north of Iceland before their return to Szeged, but life had other ideas. 

Zoltán was a scientist of the highest calibre and has left behind a large body of deep and seminal work that will keep researchers in theoretical computer science busy for a long time to come. The list of refereed publications available from his web site at 
http://www.inf.u-szeged.hu/~ze/classified.pdf 
includes two books, 32 edited volumes, 135 journal papers, four book chapters, 86 conference papers and seven papers in other edited volumes. However, impressive as they undoubtedly are, these numbers give only a very partial picture of Zoltán's scientific stature. Together with the late Stephen Bloom, Zoltán was the prime mover in the monumental development of Iteration Theories. As Stephen and Zoltán wrote in the preface of their massive book on the topic, which was published in 1993 by Springer:

Iteration plays a fundamental role in the theory of computation: for
example, in the theory of automata, in formal language theory, in the
study of formal power series, in the semantics of flowchart algorithms
and programming languages, and in circular data type definitions.  It
is shown that in all structures that have been used as semantical
models, the equational properties of the fixed point operation are
captured by the axioms describing iteration theories. These structures
include ordered algebras, partial functions, relations, finitary and
infinitary regular languages, trees, synchronization trees, 2-categories,
and others.

It is truly remarkable that the equational laws satisfied by fixed point operations are essentially the same in a large number of structures used in computer science. Isolating those laws, and showing their applicability, has been one of the goals of Zoltán's scientific life and we trust that the members of our community will keep reading his work on iteration theories, which continued and went from strength to strength after Stephen and he published their 600-page research monograph in 1993. During his last talk in Reykjavik, we asked Zoltán whether he was planning to write a new edition of that book, and half-jokingly told him that it would probably be about 1,200 pages.

Zoltán's research output includes contributions to automata theory, category theory, concurrency theory, formal languages, fuzzy sets and fuzzy logic, graph theory, logic in computer science, logic programming, order theory, semiring theory and universal algebra, amongst others. The breadth of research areas to which he has contributed bears witness to his amazing mathematical powers and to his curiosity. Wherever he went and no matter how long he had travelled to get there, Zoltán's brain was always open. 

Zoltán also contributed to the research community with his service work and received several awards. Here we will limit ourselves to mentioning that he was elected member of the Academy of Europe in 2010, was named Fellow of the EATCS in 2016, was a member of the council of the EATCS from 2003 to 2015, and of the Presburger Award Committee in 2015--2016. He represented the Hungarian theoretical computer science community in the International Federation for Information Processing (IFIP) as member of TC1 since 2000 and was one of the prime mover in the establishment of the IFIP WG 1.8, Working Group on Concurrency. He also received the Gy. Farkas Research Award and the K. Rényi Research Award of the János Bolyai Mathematical Society.

Zoltán's appetite for work was phenomenal, but he also liked to have fun, to spend time with friends eating good food and drinking excellent wine, and to travel. Indeed, Zoltán's lust for travel was amazing. We lost track of his visits to myriads of research institutions and universities all over the world. He attended conferences in the most remote locations and always made sure that he would reserve some time for enjoying the most beautiful and known sites. At times, we had the feeling that he had been everywhere in the world.  

Despite being often on the move, Zoltán was very much a family man. He was very proud of his wife Zsuzsanna, their daughter Eszter and their son Robert. He always told us about the latest developments in their lives and was happy about his four grandchildren. We had the pleasure of enjoying Zsuzsanna and Zoltán's exquisite hospitality both in Szeged and in their summer home on Lake Balaton.

Zoltán was very loyal to his friends and would make trips to see them wherever they were living. We were lucky to be amongst them and had the pleasure of hosting him in Aalborg, Florence and Reykjavik, where he visited us a few times and where the thread of his life was cut. We will miss the time we spent doing research or relaxing together, his sense of humour, his conviviality and his hospitality. 

LICS 2017: Call for Workshop Proposals

                                        Call for Workshop Proposals
                                                  LICS 2017
                                32nd Annual ACM/IEEE Symposium
                                    on Logic in Computer Science

                                     http://lics.rwth-aachen.de/lics17/


The thirty-second Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'17) will be held in Reykjavik, Iceland on June 20–23, 2017. The workshops will take place on June 18–19, 2017. June 18 will only be used by two-days workshops (if any), or in case the number of workshops is really large. This year, workshop fees should be around 65 euros for a one-day workshop (including lunch and two coffee breaks).

Researchers and practitioners are invited to submit proposals for workshops on topics relating logic – broadly construed – to computer science or related fields. Typically, LICS workshops feature a number of invited speakers and a number of contributed presentations. LICS workshops do not usually produce formal proceedings. However, in the past there have been special issues of journals based in part on certain LICS workshops.

Proposals should include:

        • -  A short scientific summary and justification of the proposed topic.
             This should include a discussion of the particular benefits of the topic to the LICS community.
        • -  A discussion of the proposed format and agenda.
        • -  The proposed duration, which is typically one day (two-day workshops can be accommodated too).
        • -  Procedures for selecting participants and papers.
        • -  Expected number of participants. This is important for the room!
        • -  Potential invited speakers.
        • -  Plans for dissemination (for example, special issues of journals).

Proposals should be sent to Patricia Bouyer: bouyer@lsv.fr

** Important Dates **

        Submission deadline:    November 1, 2016
        Notification:                   November 15, 2016
        Program of the workshops ready: May 19, 2017
        Workshops:                      June 18–19, 2017
        LICS conference:                June 20–23, 2017

The workshops selection committee consists of the LICS General Chair, LICS Workshops Chair, LICS 2017 PC Chair and LICS 2017 Conference Chair.

An interview with Paul Spirakis, the new EATCS president

During its annual meeting at ICALP 2016 in Rome, the Council of the EATCS elected Paul Spirakis (University of Liverpool, UK, and University of Patras, Greece) as its new president. Paul is a well-known figure in the theoretical'computer-science community and truly needs no introduction. However, I felt that it might be a good idea to interview him briefly in order to give him the opportunity to present himself to the community and to discuss some of his plans for his mandate as president of the EATCS.

I interviewed Paul Spirakis via email and present his answers to my questions in this interview that will appear in the October issue of the Bulletin of the EATCS. In order to preserve the style of Paul’s answers, I did not edit them. I hope that the readers of this blog and of the Bulletin of the EATCS will enjoy reading the text of the interview and will find it as interesting as I did.

Proceedings of ICALP 2016

The proceedings of ICALP 2016 are now available from the LIPIcs web site. Many thanks to all the colleagues who have worked so hard to make this possible.

I hope that many of you will read the papers in the proceedings, which were selected by Davide, Michael, Yuval and  their PCs, and build on their research contributions.

CAV Award 2016

The CAV Award 2016 was presented today to Josh Berdine, Cristiano Calcagno, Dino Distefano, Samin Ishtiaq, Peter O'Hearn, John Reynolds, and Hongseok Yang for "the development of Separation Logic and for demonstrating its applicability in the automated verification of programs that mutate data structures." This is the second major award that is given for work on Separation Logic in the space of roughly a week. Indeed, Steve Brookes and Peter O'Hearn received the 2016 Gödel Prize last week at ICALP 2016 for their invention of Concurrent Separation Logic. (The retrospective article describing Concurrent Separation Logic starts on page 47.)

The award recipients are honoured for the development of the theory of Separation Logic, which includes the key notion of separating conjunction, the work showing its applicability in the analysis of non-trivial programs, and the tool development that culminated in Facebook Infer.

Congratulations to the award recipients!

Those interested in learning about Separation Logic can consult, for instance, the following resources by Peter O'Hearn:

• A Primer on Separation Logic (and Automatic Program Verification and Analysis).
• Tutorial on Separation Logic. (slides)

Enjoy!

Report on the EATCS General Assembly at ICALP 2016

The annual general assembly of the EATCS was held at ICALP 2016 on Thursday, 14 July, from 16:30 till 18:15. The slides I used for the meeting are here, for those who are interested.

I started the general assembly by apologizing to the audience for the problems we had in making the official LIPIcs proceedings available by the conference date. (A preliminary version of the proceedings was available in the form of three large files, one per track, but those were very large and hard to download at the conference hotel. The EATCS Secretary prepared a dedicated web page from which the files of the individual papers could be accessed,  but this page was available too late.) This ICALP was the first edition of the conference with LIPIcs proceedings and there were some associated teething problems. (ICALP is the largest conference ever to publish its proceedings with LIPIcs, as far as I know.) I am responsible for this problem and promised that it won't happen again.

During the ensuing discussion, Thore Husfeldt mentioned that, based on his experience as editor of a recent LIPIcs proceedings, he realized that we (theoretical computer scientists) are not good at following the given typesetting guidelines and that this makes the work of the proceedings editors and of the LIPIcs staff harder than it needs to be. (In passing, in a comment to this post, Marc Herbstritt from LIPIcs pointed out that some ICALP papers contains flaws that LIPIcs is still trying to resolve as part of publishing a high-quality proceedings volume. He also noted that most of the authors did not comply with the  typesetting instructions they were given, which results in a huge amount of additional work for LIPIcs, and asked: "How come?")

I thanked Thore and asked the audience to help the proceedings chair and the LIPIcs staff by sticking to the typesetting instructions they are given. With electronic proceedings, one or two pages more don't matter and there is no point in trying to gain them by hacking the style files or using fonts that are forbidden by the publisher.

As a counterpoint, Mikkel Thorup and Yuval Rabani stated that they felt authors should not be bothered by strict typesetting guidelines, and that they should spend their time doing good science rather than having to worry about typesetting guidelines from the publishers. Mikkel stated that "if it typesets, it should be good enough". He also suggested that a nice web interface to which authors could upload their papers for checking whether they meet the guidelines of the publisher would be very helpful.

I thanked all the contributors to the discussion. The EATCS will take all the suggestions into account and discuss them with LIPIcs. ICALP will also try to cooperate with other conferences and LIPIcs in order to develop some automated support that can help in preparing the proceedings efficiently and professionally.

I then remembered four colleagues who have left us too early: Hartmuth Ehrig, Zoltán Ésik, David Johnson and Helmut Veith. Obituaries for all these colleagues, apart from Zoltán Ésik, may be found in the June issue of the Bulletin of the EATCS. I trust that contributions honouring the memory of Zoltán Ésik will appear in the October issue of the Bulletin. The EATCS Council decided to offer a small donation to the award in memory of Helmut Veith, established by the University of Vienna to support promising students. As usual, I invite the members of the TCS community to honour the memory of the aforementioned colleagues by building on their work and disseminating it amongst our students.

Tiziana Calamoneri delivered the report from the conference organizers. (Tiziana's slides are here.) ICALP 2016 had 239 registered participants, 205 of whom registered by the early registration deadline. In her presentation, Tiziana also analyzed some of the reasons for the lack of workshops at this year's edition of ICALP.

Yuval Rabani, who chaired the PC for Track A of ICALP,  delivered the report on the PC chairs. (The slides are here.) Yuval said that chairing the PC of Track A was an unexpectedly pleasant experience and thanked his PC for the splendid work it had done. Apart from reporting on the figures related to accepted  and submitted papers, Yuval described the selection process for Track A, building on his blog posts available here. Quoting from Yuval's blog,

The committee identified around 50 borderline papers, and we had to choose among them 5 or 6 papers. (For those familiar with EasyChair - most papers with scores 2, 1, 1 were rejected.) Choosing those 5-6 papers out of 50 or 51 papers took up about half of the discussion time, because it was indeed a difficult choice. We felt that almost all of the borderline papers could have ended up in the program. The final choice was made, in part, by assessing the “added value” to already chosen papers. For 2 of the 6 slots we ended up voting between 2-3 alternatives for each slot (papers in the same area that were thought to be of about the same quality). Aside from these few last papers, we devoted almost no attention to balancing subareas of theory. Papers were accepted based on pure merit, as judged by experts. Despite the indifference to areas, I think the program came out rather balanced between algorithms and complexity theory, with a nice presence in specialized niche areas. This is a natural outcome of a diverse committee.

Immediately after Yuval's presentation, I handed out the awards for the best papers and the best student papers at ICALP 2016.  The best paper awards went to the following papers:

• Andreas Galanis, Andreas Göbel, Leslie Ann Goldberg, John
  Lapinskas and David Richerby. Amplifiers for the Moran Process.  (Track A)
• Neeraj Kayal, Chandan Saha and Sébastien Tavenas. An almost Cubic Lower Bound for Depth Three Arithmetic Circuits. (Track A)
• Olivier Bournez, Daniel Graça and Amaury Pouly. Polynomial Time corresponds to Solutions of Polynomial Ordinary Differential Equations of Polynomial Length.   (Track B)

The following papers received the best student paper awards:

• Samuel Hetterich. Analysing Survey Propagation Guided Decimation on Random Formulas.  (Track A)
• Keerti Choudhary. An Optimal Dual Fault Tolerant Reachability Oracle. (Track C)

Congratulations to the authors of the award-receiving papers!

Mikolaj Bojanczyk gave a short report on the organization of ICALP 2017 on behalf the organizing committee. ICALP 2017 will be held in Warsaw, Poland, in the period 10-14 July 2017. The PC chairs will be Piotr Indyk (MIT, USA) for Track A, Anca Muscholl (LaBRI, France) for Track B and Fabian Kuhn (Freiburg,
Germany) for Track C. Three invited speakers have already been confirmed: Mikolaj Bojanczyk (Warsaw, Poland), Monika Henzinger (Vienna, Austria) and Mikkel Thorup (DIKU, Denmark). A fourth invited speaker will be announced soon.

Mikolaj mentioned that four workshops have already agreed to co-locate with ICALP 2017. If you are interested in organizing a workshop at ICALP 2017, please contact the local organizers.

Jiří Sgall presented a bid to host ICALP 2018, the 45th ICALP,  in Prague in the period July 9-13, 2018. The slides for Jiři's presentation are here. The bid from Prague was accepted by the General Assembly. Thanks to Jiří and his colleagues for their kind offer to host ICALP in the beautiful city of Prague! ICALP 2017 and 2018 will also allow us to celebrate the excellent contributions of the Polish and Czech research communities to TCS and discrete mathematics.

After the ICALP-related presentations, I asked the audience the following questions:

• Does ICALP cover TCS sufficiently broadly?
• What do you think of the current acceptance rates at ICALP?
• What would you like to see at ICALP that we don’t do?
• Any criticisms/kudos/suggestions?

There were interesting suggestions from several colleagues. In particular, there was a lively discussion related to the role of the current incarnation of Track C. Despite the best efforts of the PC chairs of the last few years to "brand" this track as a "theory of networking" track, it is fair to say that, despite the high quality of the contributed papers, Track C is still being seen by many as a less competitive version of Track A. This opinion was, for instance, aired by Mikkel Thorup. In particular, Mikkel asked: "What is the role of the current Track C rather than allowing PC members for Track A to submit to the conference?" I reminded the audience that Track C was meant to cover "emerging areas" and that its scope should therefore be regularly considered. During the ensuing discussion, Paul Spirakis suggested that perhaps Track C could be solely devoted to Algorithmic Game Theory. Summing up, the EATCS Council will examine the future of Track C of ICALP in its coming meetings.

Mikkel Thorup also suggested that the submitted versions of the accepted ICALP papers should be posted on the conference web page as soon as they are accepted. This suggestion led to further interesting discussions. IMHO, it would certainly be beneficial to post the final versions of the accepted papers on the conference web site as soon as they arrive.

Thore Husfeldt suggested that the EATCS establish an SC for the conference, possibly independent of the council, and that the EATCS consider establishing a "fast track" for the publication of journal versions of the best ICALP papers. Regarding the first point, I informed the audience that the EATCS already has an ICALP Liaison Committee, but that it would be a good idea to give more power and responsibilities to it. That committee should also revise the current version of the guidelines for ICALP organizers, which are definitely out of date in the light of the new publication outlet for the proceedings and the new awards sponsored by the EATCS. I also informed the audience that the EATCS Council has been discussing the possible establishment of an open-access ournal of the association for some time.

Regarding awards, the audience suggested that the EATCS consider establishing an ICALP Test-of-Time Award. A young researcher even suggested that ICALP should have a best reviewer award.

I thank the attendees for their many suggestions and invite any reader of this post to send theirs to the president of the EATCS or as comments to this post. You are the life and blood of the association. Your input is always most welcome and the EATCS listens to you. We are here to serve.

Next the secretary and the treasurer of the EATCS delivered their annual reports. (The financial report is here and the report from the secretary is here.) We also thanked Dirk Janssens who left his post as treasurer of the EATCS after 27 years of sterling service to the association. We welcomed Jean-Francois Raskin as the new treasurer of the EATCS.

The rest of the general assembly was devoted to a report from the outgoing president (viz. me). I refer you to the slides for my presentation and to the EATCS Annual Report for the details. Here I will limit myself to saying that at the general assembly I announced the new leadership of our association for the coming two-year term. The new president of the EATCS will be Paul Spirakis (University of Liverpool and U. Patras). He will be supported by Leslie Ann Goldberg (University of Oxford), Antonin Kucera (Masaryk University) and Giuseppe Persiano (University of Salerno) as vice-presidents.

During the general assembly, Paul gave a short speech describing some if his objectives as president of the EATCS for the coming two years. The EATCS is in very good hands and I look forward to seeing its influence grow under its new leadership.

Let me close this report by asking my readers and the members of the TCS community at large the questions I posed to the colleagues who attended the general assembly:

• What should the EATCS do for the TCS community?
• What activities should the EATCS support (financially or otherwise)?
• How can we make EATCS membership more attractive (especially among the younger generations)?

Any input you might have will be useful for the new leadership of the EATCS. Make your voice heard, so that the EATCS can serve the TCS community even better than it is already doing.

I thank all of you for the support I have received over the last four years in my role of president of the EATCS. It was a lot of work (to achieve probably very little), but I learned much from many of you. Thank you! You are the life and blood of the EATCS.

A peek at ICALP 2016 in Rome

ICALP 2016 took place last week in Rome from the 12th till the 15th of July. The conference, which brought ICALP to Italy for the fifth time, was well organized by Tiziana Calamoneri, Irene Finocchi, Nicola Galesi and Daniele Gorla, whom I thank for the effort they put into making ICALP 2016 a memorable event.

According to the data presented by Tiziana on behalf of the local organizers during the General Assembly of the EATCS held on Thursday, 14 July, ICALP 2016 had 239 registered participants, 74 of which were students. The USA was the country contributing the largest share of attendees (50), followed by France, the UK, Germany and Italy. Let me note, in passing, that I would have expected a larger number of participants from Italy, given the size of the Italian TCS community, the number of TCS researchers based in Rome and in neighbouring cities, and the ease with which Rome can be reached from most of the country. (Italy contributed 21 participants to the conference.)

ICALP 2016 featured four invited talks, which were delivered by Devavrat Shah (MIT, USA), Xavier Leroy (INRIA, France), Seffi Naor (Technion, Israel) and Marta Z. Kwiatkowska (Oxford, UK), as well presentations by the recipients of the Presburger Award, the Gödel Prize and the EATCS Award.

Devavrat Shah kicked off the conference on Monday, 12 July, by delivering a talk entitled Computing Choice. In his talk, Devavrat discussed algorithmic results relating to ranking, rank aggregation and personalized rankings associating intensity to rankings based on partial information resulting from a sparse set of comparisons. The talk, which was excellently paced and interesting, presented many results and I invite you to check Dev's work for the details.This work addresses computational challenges for decision making without a choice model, and offered a glimpse of the exciting possibilities for inter-disciplinary work across disciplines such as CS, EE, OR and Economics.

Xavier Leroy delivered the second invited talk, entitled Formally verifying a compiler: What does it mean exactly?, on Wednesday, 13 July. In his talk, Xavier discussed the context for, and the results of, the CompCert project, which investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. In this project, Coq is used both as a proof assistant and as a programming language.

In his talk, Xavier said that "Pure functional programming is the shortest path to writing and verifying software." He also asked and addressed two fundamental questions arising from this work and related ones:

• Did we prove it (the compiler) right?
• Did we prove the right thing? 

In particular, Xavier discussed the latter question in detail and argued that the social consensus underlying the acceptance of proofs in mathematics also plays a role in accepting proofs of software correctness. He also mentioned the "unreasonable effectiveness of labelled transition systems" in semantics and in supporting such correctness proofs.

Seffi Naor's talk took place on Thursday, 14 July, and was entitled Maximatization of submodular functions: Recent progress. Seffi stepped in at the last moment for Subhash Khot, who was unable to make the trip to Rome. On behalf of the EATCS and of the TCS community as a whole, I thank him for delivering an excellent talk at such a short notice.

Research on the topic of Seffi's talk started in  the 1950s-1960s and is now thriving. It has applications in the study of social welfare, economics/game theory, combinatorial optimization, machine learning and information theory. In his talk, Seffi first surveyed results on unconstrained maximization of non-monotone functions, with focus on approximation algorithms, and then presented results for the constrained maximization problem. I refer the readers to Seffi's papers and to this Wikipedia page for more information.

The last invited talk at ICALP 2016 was delivered by Marta Z. Kwiatkowska on Friday, 15 July. Marta's talk was entitled Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice and is accompanied by a paper that is available here. Marta stated right at the start that, despite the success that model checking and synthesis techniques have had and are having, we have not found yet the right modelling abstractions for autonomous mobile agents such as robots and autonomous vehicles. Software for these vehicles is expected to behave reliably under uncertainty, and its analysis and synthesis require quantitative approaches to specification and verification. As Marta argued cogently in her talk, a game-theoretic point of view is fruitful in the study of such systems. Indeed, games of various kinds have played a fundamental role in the study of the synthesis of correct programs from specifications from the very beginning, and papers on game-theoretic models abound in Volume B conferences. (See the slides for this talk by Moshe Vardi for historical remarks and an overview of the game-theoretic approach to synthesis.) Rather than attempting to summarize Marta's talk, I strongly encourage you to read her accompanying paper, which beautifully summarizes her work on this topic and contains pointers to related literature.

The core of the scientific programme consisted of the papers that were selected for presentation by the PC chairs (Michael Mitzenmacher, Yuval Rabani and Davide Sangiorgi) and their PCs. Because of EATCS commitments, I could not attend as many talks as I would have liked, but all those I did manage to listen to were excellent both scientifically and from the point of view of the quality of the presentation. (For one of the talks, I even had to wear 3D glasses :-)) Thanks to the PC chairs and their PCs for doing a truly great job!

The award ceremony was held on Wednesday, 13 July, and saw the presentation of the EATCS Distinguished Dissertation Awards, of the Presburger Award to Young Scientists, of the Gödel Prize and of the EATCS Award. The event was a festive occasion and celebrated some of the outstanding members of the TCS community.

The EATCS Distinguished Dissertation Award Committee, consisting of Javier Esparza, Michal Feldman, Fedor Fomin,  Luke Ong and Giuseppe Persiano (chair), has selected the following three theses for the EATCS Distinguished Dissertation Award for 2015:

• Radu Curticapean, The Simple, Little and Slow Things Count: On Parameterized Counting Complexity. Thesis work carried out at the Department of Computer Science at Saarland University, Saarbrücken, Germany. Supervisor: Markus Bläser.
• Heng Guo. Complexity Classification of Exact and Approximate Counting Problems. Thesis work carried out at the Department: of Computer Sciences in the University of Wisconsin-Madison. Advisor: Jin-Yi Cai,
• Georg Zetzsche. Monoids as storage mechanisms. Thesis work carried out at the Department: of Computer Science at University of Kaiserslautern. Supervisor:  Roland Meyer. 

The award committee received an impressive set of submissions in terms of quality. The three selected theses are outstanding.

The Presburger Award was presented to  Mark Braverman (Princeton University, USA). The Gödel Prize went to Stephen Brookes and Peter O'Hearn for their invention of concurrent separation logic, and the EATCS Award was given to Dexter Kozen. The presentation of each of these three awards was accompanied by an excellent talk by the award recipient(s). As I mentioned during the award ceremony, this might very well be the first time that the Gödel Prize is mentioned in a piece in the New Yorker.

The award session was extremely well attended and preceded a short bus tour in Rome and a social dinner in a popular restaurant in Trastevere.

The annual General Assembly of the EATCS took place on Thursday, 14 July. I'll report on it elsewhere. Here I will limit myself to saying that, at the General Assembly, I formally stepped down as president of the EATCS after two terms of service (four years). The new president of the EATCS will be Paul Spirakis (University of Liverpool and U. Patras). He will be supported by Leslie Ann Goldberg (University of Oxford), Antonin Kucera (Masaryk University) and Giuseppe Persiano (University of Salerno) as vice-presidents. At ICALP 2016 in Rome, Dirk Janssens also left his post as treasurer of the EATCS after 27 years of sterling service. Jean-Francois Raskin kindly accepted to serve as the new treasurer of our association. The association is very grateful to the above-mentioned colleagues for their willingness to serve and to Dirk for his outstanding service over such a long time. I know that the EATCS community will support the members of the new leadership  in their work, just like they helped me during the last four years.

If you were at ICALP in Rome and you have any comment, suggestion or criticism, please post them as comments. I'll make sure that they reach the leadership of the EATCS. We are always working on improving an already very successful conference that does its best to provide a bird's eye view of TCS as a whole.

Call for guest bloggers at ICALP 2016

I would like to have some blog coverage for ICALP 2016. If you are attending the conference in Rome and you are interested in guest blogging, drop me a line. Ideally, I would like to have a guest blogger for each of the tracks in the conference. You are, of course, also most welcome to blog about the five invited talks, the award ceremony, the general assembly and any other aspect of the conference.

I'll try to write something myself, but the more the merrier!

EATCS Bulletin Issue 119 is available online

The June 2016 issue of the Bulletin of the EATCS is now available on line. If you prefer, you can download a pdf with the printed version of the Bulletin. As usual, thanks to the support of the members of the EATCS, the Bulletin is open access.

This issue of the Bulletin  features the following columns:

• "Survey of Distributed Decision", by Laurent Feuilloley and Pierre Fraigniaud; 
• "Learn to Program? Program to Learn!", by Matthias Hauswirth; and
• "Fundamentals of p-values: Introduction", by Yuri Gurevich and Vladimir Vovk. 

Some of you might also be interested in advice to young researchers from Michael Fellows and other Fellows of the EATCS, and in interviews with the recipients of the Gödel Prize 2016 and of the first Alonzo Church Award.

Thanks to Kazuo Iwama, the editor in chief of the Bulletin, and the EATCS Secretary Office for their work on another excellent issue of the Bulletin.

One PhD or post-doctoral position at the School of Computer Science, Reykjavik University

Theoretical Foundations for Monitorability

School of Computer Science, Reykjavik University
One PhD or Postdoctoral Position

Applications are invited for one PhD or postdoctoral position at the School of Computer Science, Reykjavik University.  The position is part of a research project funded by the Icelandic Research Fund, under the direction of Luca Aceto (Reykjavik University), Adrian Francalanza (University of Malta) and Anna Ingolfsdottir (Reykjavik University). The general aim of the project is to develop further the theoretical foundations of monitorability for fragments of variants of Hennessy-Milner logic with recursion/modal mu-calculus.

The project work will build on the RV 2015 paper by the co-proposers (http://dx.doi.org/10.1007/978-3-319-23820-3_5), and on the experience developed during their previous work on runtime verification and on the tool detectEr (http://www.cs.um.edu.mt/svrg/Tools/detectEr/). The goals of the project will be:

• to explore more stringent conditions for detection than the ones considered in the RV 2015 paper and study whether this has any effect on the monitorable subset of the logic;
• to investigate the monitorability of the logic with respect
  to instrumentation set-ups other than the one used in the RV 2015 paper;
• to extend our results from the RV 2015 paper to the setting of real-time systems, modelled as timed automata, and to a real-time variant of Hennessy-Milner Logic with recursion;
• to understand how existing notions of monitorability relate to the one formulated in the RV 2015 paper, thereby consolidating disparate concepts of monitorability;
• to investigate extensions to monitorability that incorporate notions
  of enforceability; and
• to apply the results of the theoretical work in the construction of a prototype software tool for the runtime analysis of systems.

The successful candidates will benefit from, and contribute to, the research environment at the Icelandic Centre of Excellence in Theoretical Computer Science (ICE-TCS). For information about ICE-TCS and its activities, see

http://www.icetcs.ru.is/.

Moreover, she/he will visit Adrian Francalanza's group at the University of Malta during the project work and will benefit from the research experience on runtime verification within that group.

Qualification requirements

Applicants for the PhD fellowship should have an MSc degree in Computer Science, or closely related fields. Some background in concurrency theory and mathematical competence are desirable.

Applicants for the postdoctoral position should have, or be about to hold, a PhD degree in Computer Science or closely related fields. Previous knowledge of at least one of concurrency theory, process calculi, (structural) operational semantics and logic in computer science is highly desirable.

Remuneration
The PhD position provides a stipend of 290,000 ISK (roughly 2080 € at the current exchange rate) per month before taxes, for three years, starting as early as possible.

The wage for the postdoctoral position is 400,000 ISK (roughly 2870  € at the present exchange rate) per month before taxes. The position is for one year, starting on September 1, 2016 (later starting dates are possible), and is renewable for another year, based on good performance and mutual satisfaction.

Application details

Interested applicants should send their CV, including a list of publications, in PDF to all addresses below, together with a statement outlining their suitability for the project and the names of at least two referees.

Luca Aceto
email: luca@ru.is

Adrian Francalanza
email: adrian.francalanza@um.edu.mt

Anna Ingolfsdottir
email: annai@ru.is
We will start reviewing applications as soon as they arrive, and will continue to accept applications until the position is filled. However, we strongly encourage interested applicants to send in their applications as soon as possible.

10 funded positions for PhD studies in Computer Science at GSSI in L'Aquila

I have been asked to distribute this advertisement of ten fully-funded PhD positions at the Gran Sasso Science Institute, an international PhD school that is close to my heart and that is located in Abruzzo, my home region in Italy. I'd be grateful if you could distribute this announcement to potentially interested students. There are excellent opportunities for students interested in TCS.

The Gran Sasso Science Institute (GSSI - http://www.gssi.infn.it/ ), a recently established international PhD school and a Center for advanced studies in L'Aquila (ITALY), offers 10 PhD positions in Computer Science (CS).

The PhD program in CS is mainly concerned with heterogeneous distributed systems and their interactions. Different perspectives are offered to provide students with the necessary tools for the design, the implementation, the management and the use of distributed systems. The main research areas of interest are:
- Efficient algorithms for communication networks and social networks;
- Formal methods for systems correctness and analysis;
- Software engineering for efficient and resilient applications.

Apart from pursuing their own research studies, the successful candidates will have the opportunity to cooperate with members of the research group and of the Scientific Board, as well as with the frequent guests of the Institute. Detailed information about the CS research group and about the activities for the Phd program in CS can be found at http://cs.gssi.infn.it/

The fellowships are awarded for three years and their yearly amount is € 16.159,91 gross. Moreover all PhD students:
 - will have free accommodation at the GSSI facilities and use of the canteen;
-  will have tuition fees waived;
-  will be covered by insurance against accident and/or injury.

The application must be submitted through the online form available at http://www.gssi.it/phd/ and have to be accompanied by the curriculum vitae and by a statement letter describing:
 - a brief research project outlining the research challenges to consider for the PhD thesis;
 - the reasons for choosing GSSI for the PhD studies.

The deadline for application is: 1st September 2016 at 18.00 (Italian time zone).

For information see http://www.gssi.infn.it/phd/ or write an email to info@gssi.infn.it or call +39 0862 428026.

"Views on work in theoretical computer science" by Wolfgang Thomas

 
In the fifth installment of the series in which Fellows of the EATCS provide their advice to the budding TCS researcher, I am posting the contribution by Wolfgang Thomas. Happy reading!

As one of the EATCS fellows I have been asked to contribute some personal words of advice for younger people and on my research interests. Well, I try my best.

Regarding advice to a student and young researcher interested in TCS, I start with two short sentences:

• Read the great masters (even when their h-index is low).
• Don’t try to write ten times as many papers as a great master did.

And then I add some words on what influenced me when I started research - you may judge whether my own experiences that go back to „historical“ times would still help you.

By the way, advice from historical times, where blackboards and no projectors were used, posed in an entertaining but clearly wise way, is Gian-Carlo Rota’s paper „Ten Lessons I Wish I Had Been Taught“ (http://www.ams.org/notices/199701/comm-rota.pdf). This is a view of a mathematician but still worth reading and delightful for EATCS members. People like me (68 years old) are also addressed - in the last lesson „Be Prepared for Old Age“…

Back in the 1970’s when I started I wanted to do something relevant. For me this meant that there should be some deeper problems involved, and that the subject of study is of long-term interest. I was attracted by the works of Büchi and Rabin just because of this: That was demanding, and it treated structures that will be important also in hundred years: the natural numbers with successor, and the tree of all words (over some alphabet) with successor functions that represent the attachment of letters.

The next point is a variation of this. It is a motto I learnt from Büchi, and it is a warning not to join too small communities where the members just cite each other. In 1977, when he had seen my dissertation work, Büchi encouraged me to continue but also said: Beware of becoming member of an MAS, and he explained that this means „mutual admiration society“. I think that his advice was good.

I am also asked to say something about principles for the postdoctoral phase. It takes determination and devotion to enter it. I can say just two things, from my own experience as a young person and from later times. First, as it happens with many postdocs, in my case it was unclear up to the very last moment whether I would get a permanent position. In the end I was lucky. But it was a strain. I already prepared for a gymnasium teacher’s career. And when on a scientific party I spoke to Saharon Shelah (one of the giants of model theory) about my worries, he said „well, there is competition“. How true. So here I just say: Don’t give away your hopes - and good luck. - The other point is an observation from my time as a faculty member, and it means that good luck may be actively supported. When a position is open the people in the respective department do not just want a brilliant researcher and teacher but also a colleague. So it is an important advantage when one can prove that one has more than just one field where one can actively participate, that one can enter new topics (which anyway is necessary in a job which lasts for decades), and that one can cooperate (beyond an MAS). So for the postdoc phase this means to look for a balance between work on your own and work together with others, and if possible in different teams of cooperation.

Finally, a comment on a research topic that excites me at this moment. I find it interesting to extend more chapters of finite automata theory to the infinite. This has been done intensively in two ways already - we know automata with infinite „state space“ (e.g., pushdown automata where „states“ are combined from control states and stack contents), and we know automata over infinite words (infinite sequences of symbols from a finite alphabet). Presently I am interested in words (or trees or other objects) where the alphabet is infinite, for example where a letter is a natural number, and in general where the alphabet is given by an infinite model-theoretic structure. Infinite words over the alphabet N are well known in mathematics since hundred years (they are called points of the Baire space there). In computer science, one is interested in algorithmic results which have not been the focus in classical set theory and mathematics, so much is to be done here.

Scott Smolka's advice to the young theoretical computer scientist

As the fourth installment of the series in which Fellows of the EATCS provide their advice to the budding TCS researcher, I am posting the advice from Scott Smolka. Enjoy!

Advice I would give to a student interested in TCS Not surprising, it all starts with the basics: automata theory, formal languages, algorithms, complexity theory, programming languages and semantics.

Advice I would give a young researcher in TCS Go to conferences and establish connections with more established TCS researchers. Seek to work with them and see if you can arrange visits at their home institutions for a few months.

A short description of a research topic that excites me at this moment in time (and possibly why) Bird flocking and V-formation are topics I find very exciting. Previous approaches to this problem focused on models of dynamic behavior based on simple rules such as: Separation (avoid crowding neighbors), Alignment (steer towards average heading of neighbors), and Cohesion (steer towards average position of neighbors). My collaborators and I are instead treating this as a problem of Optimal Control, where the fitness function takes into account Velocity Matching (alignment), Upwash Benefit (birds in a flock moving into the upwash region of the bird(s) in front of them), and Clear View (birds in the flock having unobstructed views). What’s interesting about this problem is that it is inherently distributed in nature (a bird can only communicate with its nearest neighbors), and one can argue that our approach more closely mimics the neurological process birds use to achieve these formations.

Sad news: Zoltán Ésik passed away yesterday

Our good colleague and friend Zoltán Ésik passed away suddenly yesterday afternoon in the hotel room where he was staying with his wife during a visit to our group at Reykjavik University. He had delivered a survey talk at Reykjavik University on the Equational Logic of Fixed Point Operations on Tuesday and we were making plans for the coming days.


Zoltán was a scientist of the highest calibre; he was one of the prime movers in the monumental development of Iteration Theories, amongst many other achievements. He had served the EATCS as a member of its Council for many years, had recently been named as one of the 2016 EATCS Fellows and he had been a member of the Presburger Award Committee for the last two years.

There is much more to be said about his scientific achievements and warm personality, but this will have to wait for better times.

R.I.P. Zoltán. 

Giuseppe Italiano's advice to young researchers in TCS

As the third installment of the series in which Fellows of the EATCS provide their advice to the budding TCS researcher, I am posting the advice from Giuseppe Italiano. Happy reading!

The advice I would give to a student interested in TCS There’s a great quote by Thomas Huxley: “Try to learn something about everything and everything about something.” When working through your PhD, you might end up focusing on a narrow topic so that you will fully understand it. That’s really great! But one of the wonderful things about Theoretical Computer Science is that you will still have the opportunity to learn the big picture!

The advice I would give a young researcher in TCS Keep working on the problems you love, but don’t be afraid to learn things outside of your own area. One good way to learn things outside your area is to attend talks (and even conferences) outside your research interests. You should always do that!

A short description of a research topic that excites me at this moment in time (and possibly why) I am really excited by recent results on conditional lower bounds, sparkled by the work of Virginia Vassilevska Williams et al. It is fascinating to see how a computational complexity conjecture such as SETH (Strong Exponential Time Hypothesis) had such an impact on the hardness results for many well-known basic problems. (Editor's notes: You might be interested in the slides for the presentations given at this workshop that was co-located with STOC 2015.)

David Harel's advice to the young theoretical computer scientist

As second installment of the series in which Fellows of the EATCS provide their advice to the budding TCS researcher, I am posting the advice from David Harel. Enjoy!

Advice I would give to a student interested in TCS:

If you are already enrolled in a computer science program, then unless you feel you are of absolutely stellar theoretical quality and the real world and its problems do not attract you at all, I’d recommend that you spend at least 2/3 of your course efforts on a variety of topics related to TCS but not “theory for the sake of theory”. Take lots of courses on languages, verification AI, databases, systems, hardware, etc. But clearly don’t shy away from pure mathematics. Being well-versed in a variety of topics in mathematics can only do you good in the future. If you are still able to choose a study program, go for a combination: TCS combined with software and systems engineering, for example, or bioinformatics/systems biology. I feel that computer science (not just programing, but the deep underlying ideas of CS and systems) will play a role in the science of the 21^st century (which will be the century of the life sciences) similar to that played by mathematics in the science of the 20^th century (which was the century of the physical sciences).

Advice I would give a young researcher in TCS:

Much of the above is relevant to young researchers too. Here I would add the following two things. First, if you are doing pure theory, then spend at least 1/3 of your time on problems that are simpler than the real hard one you are trying to solve. You might indeed succeed in settling the P=NP? problem, or the question of whether PTIME on general finite structures is r.e., but you might not. Nevertheless, in the latter case you’ll at least have all kinds of excellent, if less spectacular, results under your belt. Second, if you are doing research that is expected to be of some practical value, go talk to the actual people “out there”: engineers, programmers, system designers, etc. Consult for them, or just sit with them and see their problems first-hand. There is nothing better for good theoretical or conceptual research that may have practical value than dirtying your hands in the trenches.

A short description of a research topic that excites me at this moment in time (and possibly why):

I haven’t done any pure TCS for 25 years, although in work my group and I do on languages and software engineering there is quite a bit of theory too, as is the case in our work on biological modeling. However, for many years, I’ve had a small but nagging itch for trying to make progress on the problem of artificial olfaction ̶ the ability to record and remotely produce faithful renditions of arbitrary odors. This is still a far-from-solved issue, and is the holy grail of the world of olfaction. Addressing it involves chemistry, biology, psychophysics, engineering, mathematics and algorithmics (and is a great topic for young TCS researchers!). More recently, I’ve been thinking about the question of how to test the validity of a candidate olfactory reproduction system, so that we have an agreed-upon criterion of success for when such systems are developed. It is a kind of common-sense question, but one that appears to be very interesting, and not unlike Turing’s 1950 quest for testing AI, even though such systems were nowhere in sight at the time. In the present case, trying to compare testing artificial olfaction to testing the viability of sight and sound reproduction will not work, for many reasons. After struggling with this for quite a while, I now have a proposal for such a test, which is under review.

ICALP 2016 early registration deadline approaching

The organizers of ICALP 2016  have asked me to distribute the message below. I encourage you to attend the conference, which is going to be a veritable celebration of TCS research. 

The EARLY REGISTRATION period for ICALP 2016 ends on May 31, 2016.

The 43rd International Colloquium on Automata, Languages and Programming

(ICALP 2016) will be held in Rome (Italy) from July 12-th  to 15-th 2016 (http://www.easyconferences.eu/icalp2016/index.html).

The list of ACCEPTED PAPERS  is here (http://www.easyconferences.eu/icalp2016/accepted.html)

Conference's  INVITED SPEAKERS  are: 

- Subhash Khot (New York University, USA)

- Marta Z. Kwiatkowska (Oxford University, UK)

- Xavier Leroy (INRIA, Paris, France)

- Devavrat Shah (MIT, USA)

The following 2016 AWARDS will give a talk during the conference

-  Steve Brookes (Carnegie Mellon, USA) and Peter O'Hearn (UCL, UK)  -- Gödel Prize

-  Dexter Kozen (Cornell - USA) -- EATCS award

-  Mark Braverman (Princeton, USA) -- Presburger award

The PROGRAM of the conference is available here (http://www.easyconferences.eu/icalp2016/index.html). 

Info about ACCOMMODATION here (http://www.easyconferences.eu/icalp2016/accommodation.html)

Yuri Gurevich's advice to the young theoretical computer scientist

I have always enjoyed reading articles, interviews, blog posts and books in which top-class scientists share their experience with, and provide advice to, young researchers. In fact, despite not being young any more, alas, I feel that I invariably learn something new by reading those pieces, which, at the very least, remind me of the things that I should be doing, and that perhaps I am not doing, to uphold high standards in my job.

Based on my partiality for scientific advice and stories, it is not overly surprising that I was struck by the thought that it would be interesting to ask the EATCS Fellows for

• the advice they would give to a student interested in TCS,
• the advice they would give to a young researcher in TCS and
• a short description of a research topic that excites them at this moment in time (and possibly why).

The EATCS Fellows are model citizens of the TCS community, have varied work experiences and backgrounds, and span a wide spectrum of research areas. One can learn much about our field of science and about academic life in general by reading their thoughts.

I am collecting the answers to the above-listed questions I have received from some of the current EATCS Fellows in a contribution that will appear in the June issue of the Bulletin of the EATCS. Over the next few days, as a sneak preview for that article, I'll post the advice from some of the fellows on this blog. Enjoy it!

Advice from Yuri Gurevich (Microsoft Research)

Advice I would give to a student interested in TCS Attending math seminars (mostly in my past), I noticed a discord. Experts in areas like complex analysis or PDEs (partial differential equations) typically presume that everybody knows Fourier transforms, differential forms, etc., while logicians tend to remind the audience of basic definitions (like what’s first-order logic) and theorems (e.g. the compactness theorem). Many talented mathematicians didn’t take logic in their college years, and they need those reminders. How come? Why don’t they effortlessly internalize those definitions and theorems once and for all? This is not because those definitions and theorems are particularly hard (they are not) but because they are radically different from what they know. It is easier to learn radically different things — whether it is logic or PDEs or AI — in your student years. Open your mind and use this opportunity!


Advice I would give a young researcher in TCS As the development of physics caused a parallel development of physics-applied mathematics, so the development of computer science and engineering causes a parallel development of theoretical computer science. TCS is an applied science. Applications justify it and give it value. I would counsel to take applications seriously and honestly. Not only immediate applications, but also applications down the line. Of course, like in mathematics, there are TCS issues of intrinsic value. And there were cases when the purest mathematics eventually was proven valuable and applied. But in most cases, potential applications not only justify research but also provide guidance of sorts. Almost any subject can be developed in innumerable ways. But which of those ways are valuable? The application guidance is indispensable.

I mentioned computer engineering above for a reason. Computer science is different from natural science like physics, chemistry, biology. Computers are artifacts, not “naturefacts.” Hence the importance of computer science and engineering as a natural area whose integral part is computer science.

A short description of a research topic that excites me at this moment in time (and possibly why) Right now, the topics that excite me most are quantum mechanics and quantum computing. I wish I could say that this is the result of a natural development of my research. But this isn’t so. During my long career, I moved several times from one area to another. Typically it was natural; e.g. the theory of abstract state machines developed in academia brought me to industry. But the move to quanta was spontaneous. There was an opportunity (they started a new quantum group at the Microsoft Redmond campus a couple of years ago), and I jumped upon it. I always wanted to understand quantum theory but occasional reading would not help as my physics had been poor to none and I haven’t been exposed much to the mathematics of quantum theory. In a sense I am back to being a student and discovering a new world of immense beauty and mystery, except that I do not have the luxury of having time to study things systematically. But that is fine. Life is full of challenges. That makes it interesting.

Interview with Rajeev Alur and David Dill, recipients of the 2016 Alonzo Church Award

As announced earlier today, Rajeev Alur (University of Pennsylvania USA) and David L. Dill (Stanford University, USA) are the recipients of the 2016 Alonzo Church Award for Outstanding Contributions to Logic and Computation for their work on timed automata, a decidable model of real-time systems that combines beautiful, new and deep theory with widespread practical impact.

In order to celebrate the award of the Alonzo Church Award to this hugely
influential work and to give the theoretical computer science community at large a glimpse of the history of the ideas that led to it, I interviewed Rajeev Alur
(abbreviated to RA in what follows) and David Dill (referred to as DD in the text
below) via email. The interview will also appear in the June issue of the Bulletin of the EATCS.

LA: You are receiving the 2016 Alonzo Church Award for Outstanding Contributions to Logic and Computation for your invention of timed automata, which, as far as I know, was the first decidable formalism for reasoning about the ubiquitous class of real-time systems.  Could you briefly describe the history of the ideas that led to the development of the formalism of timed automata, what were the main inspirations and motivations for its invention and how timed automata advanced the state of the art?

DD: The interesting part of the story for me is the inspiration that led to the question in the first place and the initial results.  Things worked out so magically that I'm still amazed, so I hope that the story will be interesting to others.  I also learned a lot of lessons about research, which I hope I can convey here.

I am not a logician and don't consider myself a theorist.  I generally want to do research that has practical impact, but I like being able to apply theory to help with that.  And, in this case, I ended up creating some theory as part of that process.

My PhD research under Ed Clarke at CMU was on using finite automata for formal verification of speed independent circuits.  I started working on them using CTL model checking, and then decided during my thesis work to abandon model checking and used finite automata (I am grateful that Ed accepted this change in direction, since his primary research agenda was CTL model checking).  Speed-independent circuits are digital circuits with no clocks, which are supposed to meet their specifications for all possible gate delays.  Ed had recently co-invented CTL model checking and was exploring speed-independent circuits as an application, because speed-independent circuits are among the simplest concurrent systems with bugs.  But speed independence is a very conservative model, because engineers often know some constraints on delays, even if they can't specify exact values for the delays.  A circuit designer (Prof. Chuck Seitz of CalTech) had some ways of designing speed-independent circuits that relied on timing constraints without precisely specified delays, and asked me whether I could prove such circuits correct.

I looked at the literature, and there were a number of people who had used finite automata with a special alphabet symbol representing clock ticks, and they would simply count the clock ticks using the states of the automaton (what was later called a discrete time model).  But I wasn't comfortable with that, because asynchronous circuits don't have clocks!  I felt that events in circuits happened in continuous time, which might be different from discrete time -- but I didn't know.

While I was working on my PhD, I sat down to try to work out a method to verify timed asynchronous circuits.  The research was painless compared to a lot of my other PhD work.  I imagined that each gate had a timer that was set to a real value between constant delay bounds, and that these timers decreased continually with time until the reached 0, at which point the gate output would change. Very quickly, I came up with an algorithm that kept track of the set of all possible timer values for various discrete states, and, magically, the analysis of the regions could be easily solved using the all-pairs shortest paths problem.  I think I just got lucky and happened to think about it the right way, so it was easy to do. (Later, I learned that Vaughan Pratt had observed that certain systems of linear inequalities could be solved using shortest paths, and that a similar algorithm was used in a kind of timed Petri nets -- but I didn't know that at the time).

I left this method out of my PhD thesis, because my thesis seemed coherent and the timed model didn't seem to mesh with the other material. Then, in my first few years at Stanford, I pulled it out again and tried to prove that it was actually sound.  Getting the details right was harder than working out the original idea.  It took several weeks. The paper eventually appeared in CAV '89.

Verification with linear time (as opposed to branching time) models seemed beautiful to me because all the problems reduced to standard closure properties and decision properties that had been solved for finite automata:  Closure under intersection, complementation, and projection, and the decidability of language emptiness.  Implicit in my CAV paper were were closure under intersection, projection, and the decidability of emptiness for timed regular languages, but I couldn't prove closure under complementation.  I felt very strongly that timed regular languages were closed under complementation and would work the same way as conventional finite automata.

Then Rajeev Alur walked into my office.  He was a second year student who was ready to do some research, and his research advisor, Zohar Manna, was out of the country for a while.  I explained timed automata to Rajeev and asked whether he could resolve the question of whether they were closed under complementation.  Rajeev very quickly came up with a nicer definition of timed automata, with clocks that counted up and predicates, and an "untiming" construction for deciding language emptiness that had lower complexity than mine.   I remember it took him several months to prove that, in fact, timed automata were not closed under complementation and that, surprisingly, the universality problem was undecidable.  He proved several other amazing results, and then we wrote the "Timed Automata" paper.   The paper was rejected twice from conferences with pretty harsh reviews (I think FOCS was one conference -- I don't remember the other one) and was eventually accepted at ICALP.

I'm not sure why it was so poorly received.  I don't remember changing it much when we resubmitted it.  I think there is a problem when you formulate a new problem and solve it, but reviewers don't understand why the problem is important.  If the solution is a bit difficult, they look for reasons to reject the paper.  If you attack a well-known problem so everyone knows why you want to solve it, it's sometimes easier to sell the paper (but maybe it won't have as much impact). Or maybe we just had some bad luck -- everyone gets bad reviews, and I've unfortunately written some bad reviews myself.

RA: I joined Stanford University in 1987 as a graduate student primarily interested in logic and theory of computation. Topics such as model checking, temporal logics, and automata over infinite strings were hot topics then, and extending these formalisms to reasoning about real-time systems was a natural research direction.

For me, the key starting point was Dave's wonderful paper titled "Timing assumptions and verification of finite-state concurrent systems" that appeared in CAV 1989. Dave has already explained how he arrived at the idea of difference bounds matrices that appeared originally in his paper, and I will explain two new ideas in our follow-up work aimed at generalizing the results. Dave's original paper modeled timing constraints by introducing timers each of which could be set to a value chosen nondeterministically from a bounded interval, decreased with time, and triggered an event upon hitting 0. We changed the model by introducing clock variables each of which could be reset to 0, increased with time, and could be tested on guards of transitions. In retrospect, this led to a simpler model, and more importantly, led naturally to many generalizations such as hybrid automata. The second idea was the definition of region equivalence that defines a finite quotient over the infinite set of clock values. This proved to be a versatile tool and forms the basis of many decidability results, and in particular, algorithms for model checking of branching-time temporal logics.

LA: According to Google Scholar,  the journal paper for which you receive the Alonzo Church Award, which was published in 1994, has so far received over 6,500 citations, whereas the ICALP 1990 on which it was based has been cited over 1,250 times. A Google Scholar query also reveals that at least 135 publications citing your landmark TCS paper have more than 135 citations themselves. Moreover, the most successful and widely used tools for modelling and verification of real-time systems are based on timed automata. When did it dawn on you that you had succeeded in finding a very good model for real-time systems and one that would have a lot of impact? Did you imagine that your model would generate such a large amount of follow-up work?

DD: It will be really interesting to hear what Rajeev says about this.

At the time, I just felt happy that we had a nice theory.  I was looking around for other uses besides asynchronous circuits to which timed automata would be applicable, and, based on the name, "real-time systems" seemed like a good candidate.  But I didn't know much about the practical side of that area, and timed automata didn't seem to be directly applicable to many of the problems they worried about (there were a *lot* of papers on scheduling!).

It took a very long time before I was confident that timed automata were useful for anything, including real-time systems. So, for me, it was based on feedback from other people.  I got some grant money to work on the problem, which was a good sign.  People from control theory and real-time systems invited me to come and talk to them about it. It may be that timed model checking (which is very closely related) has had more practical impact than timed automata themselves. Other people built tools that were better than anything I created.

After a few years, the area got too hard for me. Others, especially Rajeev, were doing such a good job that I didn't feel that my efforts were needed.  So, I moved on to new topics in formal verification and asynchronous circuit design. Now I only have a fuzzy idea about the impact of timed automata, embarrassingly.

RA: The initial reception to our work was not enthusiastic. In fact, the
paper was rejected twice, once from FOCS and once from STACS, before it
was accepted in ICALP 1990. There was also a vigorous argument
advocated by a number of prominent researchers that modeling time
as a discrete and bounded counter was sufficient. By mid 1990s though
the model started gaining acceptance: in theory conferences such as
CONCUR, ICALP,and LICS a steady stream of papers studying complexity
of various decision problems on timed automata and extensions started,
and a number of implementations such as KRONOS and UPPAAL were
developed. However, I could have never imagined so much follow-up work,
and I feel very grateful to all the researchers who have contributed to
this effort.

LA: What is the result of yours on timed automata you are most proud of? And what are your favourite results amongst those achieved by others on timed automata?

DD: I'm most proud of coming up with the question and the initial (not so hard) results. To me, the question seemed so completely obvious that I couldn't believe it hadn't been answered.  I contributed to some of the later results, but Rajeev took off like a rocket and I couldn't keep up with him.  At some point, there was so much work in the area that I didn't feel I had much to add.  I know there are a lot of amazing results that I haven't studied.

I like the fact that timed automata formed a paradigm that others followed with hybrid automata and so on.  The idea of extending finite automata with other gadgets, like clocks, and analyzing the resulting state space seems to have influenced people as much as the results on timed automata.

RA: There are lots of strong and unexpected results that I like and it is hard to choose. But since you asked, let me point out two which are closely related to our original paper. The paper by Henzinger et al titled "Symbolic model checking of real-time systems" (LICS 1992) introduced the idea of associating invariants with states. I think this is a much cleaner way of expressing upper bounds on delays, and in fact, is now part of the standard definition of timed automata. In our original paper, we had proved undecidability of timed language equivalence. Cerans showed in 1992 decidability of timed bisimulation which I did not expect and involves a clever use of region equivalence on product of two timed automata.

LA: Twenty five years have passed since the invention of timed automata and the literature on variations on timed automata as well as logics and analysis techniques for them is huge. Do you expect any further development related to theory and application of time automata in the coming years? What advice would you give to a PhD student who is interested in working on topics related to timed automata today?

DD: I'm sorry, but I haven't actively pursued the area and I just don't know.  If I were giving advice to a younger version of me, knowing my strengths and weaknesses, I would actually advise that person to go and find a new problem that hasn't been worked on much.  Maybe you'll start a new field, and you'll get to solve the first problems in the area before it gets too hard.  What has worked for me was looking at an application problem, trying to find a clean way to formalize it, and then looking at the problems stemming from that formalization. It's an amazing fact that there are fundamental questions that haven't been addressed at all. Starting with a practical problem and then thinking about what theory would be helpful to solve it is a good way to come up with those questions.  Also, watch for cases where existing theory doesn't exactly fit.  Instead of trying to pound nails with a wrench, imagine a more appropriate, but simple, theory and invent that.

RA: I feel that theoretical problems as well as verification tools have been extensively investigated. Given that, my advice would be to first focus on an application. When one tries to apply an existing technique/tool to a real-world problem, there is invariably a mismatch and that insight can suggest a research idea. The emerging area of cyber-physical systems is a rich source of applications. For instance, formal modeling and analysis of medical devices can be a fruitful direction.

LA: You have both been involved in inter-disciplinary research with colleagues from biology and control theory. What general lessons have you learned from those experiences? What advice would you give a young researcher who'd like to pursue that kind of research?

DD: On reflection, my research in formal verification was not as collaborative as it could have been.  But in computational biology, if you don't have a wet lab, you really have to collaborate with other people!  Collaboration can be rewarding but also frustrating. My advice would be: learn as much about the other area as you can, so you can at least talk the same language as your collaborators. And prepare to invest lots of time communicating and understanding what motivates them -- and make sure they're willing to do the same, otherwise, it's a collaboration that is not going to work out.  What keeps you working together is mutual benefit.

Most collaborations don't work out.  If you have a good collaborator, be grateful.  And, sometimes, you may want to choose among research directions based on which ones have the best collaborators.

LA: David, Rajeev, many thanks for taking the time to share your views with the members of the TCS community and congratulations for receiving the first Alonzo Church Award!