Published: 19th September 2013
DOI: 10.4204/EPTCS.129
ISSN: 2075-2180

EPTCS 129


Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday
Manhattan, Kansas, USA, 19-20th September 2013

Edited by: Anindya Banerjee, Olivier Danvy, Kyung-Goo Doh and John Hatcliff

Dave Schmidt: a Lifetime of Scholarship
Anindya Banerjee, Olivier Danvy, Kyung-Goo Doh and John Hatcliff
A Swiss Pocket Knife for Computability
Neil D. Jones
1
A Proof System with Names for Modal Mu-calculus
Colin Stirling
18
A Comparison of Well-Quasi Orders on Trees
Torben Æ. Mogensen
30
Abstract interpretation-based approaches to Security - A Survey on Abstract Non-Interference and its Challenging Applications
Isabella Mastroeni
41
Personal Memories
Torben Amtoft
66
Notions of Monad Strength
Philip Mulry
67
Abstract Interpretation as a Programming Language
Mads Rosendahl
84
Formal Contexts, Formal Concept Analysis, and Galois Connections
Jeffrey T. Denniston, Austin Melton and Stephen E. Rodabaugh
105
Coroutining Folds with Hyperfunctions
J. Launchbury, S. Krstic and T. E. Sauerwein
121
Online partial evaluation of sheet-defined functions
Peter Sestoft
136
Modular Construction of Shape-Numeric Analyzers
Bor-Yuh Evan Chang and Xavier Rival
161
Verification of Imperative Programs by Constraint Logic Program Transformation
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti
186
Abstraction and Learning for Infinite-State Compositional Verification
Dimitra Giannakopoulou and Corina S. Păsăreanu
211
Denotational Semantics of A User-Oriented, Domain-Specific Language
Julien Mercadal, Zoé Drey and Charles Consel
229
Simulation of Two-Way Pushdown Automata Revisited
Robert Glück
250
Higher-Order Process Modeling: Product-Lining, Variability Modeling and Beyond
Johannes Neubauer, Bernhard Steffen and Tiziana Margaria
259
A Simple Semantics and Static Analysis for Stack Inspection
Anindya Banerjee and David A. Naumann
284
The Immune System: the ultimate fractionated cyber-physical system
Carolyn Talcott
309
A Survey on Product Operators in Abstract Interpretation
Agostino Cortesi, Giulia Costantini and Pietro Ferrara
325
A short note on Simulation and Abstraction
Chris Hankin
337
Automatic Repair of Overflowing Expressions with Abstract Interpretation
Francesco Logozzo and Matthieu Martel
341
David Schmidt: personal reflection
Michael Huth
358
Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version)
Martin Bodin, Thomas Jensen and Alan Schmitt
360
Iterable Forward Reachability Analysis of Monitor-DPNs
Benedikt Nordhoff, Markus Müller-Olm and Peter Lammich
384
Model Checking in Bits and Pieces
Kedar S. Namjoshi
404
A Tribute To Dave
Charles Consel
417
A Case for Dynamic Reverse-code Generation to Debug Non-deterministic Programs
Jooyong Yi
419

Dave Schmidt: a Lifetime of Scholarship

During his formative years, Dave brushed against Neil Jones's sleeve and that sent him all over the world: in Denmark first, in Edinburgh next, then forth to Iowa, and then back to Kansas State University, where his career has unfolded and flourished. There has been no year without Dave travelling abroad, for a conference or a visit, where in turn all of us have been fortunate to brush against his sleeve: we each have been better for it.

In thankful return, we are happy to organize this Festschrift and to offer him this Liber Amicorum: a collection of essays ranging from personal memories to technical contributions, because the show keeps going on.

We are grateful to EPTCS to provide a home for this collection of essays, and to Rob van Glabbeek for his helpful availability throughout. Each essay has been read and commented by at least two reviewers, to whom we also extend our thanks: Torben Amtoft, Robert Atkey, Thomas Austin, Ahmed Bouajjani, Luca Cardelli, Bor-Yuh Evan Chang, Andrey Chudnov, John Clements, Dennis Dams, Jérôme Feret, Andrzej Filinski, Pierre Ganty, Kent Grigo, Claudio Hermida, Hans Hüttel, Radu Iosif, Franjo Ivančić, Joxan Jaffar, Patricia Johann, Neil Jones, Se-Won Kim, Morten Krogh-Jespersen, Julia Lawall, Gurvan Le Guernic, Isabella Mastroeni, Laurent Mauborgne, Jan Midtgaard, Matthew Might, Antoine Miné, Neil Mitchell, Torben Mogensen, José F. Morales, Philip Mulry, Andrzej Murawski, Corina Pasareanu, David Pichardie, Corneliu Popeea, Pavithra Prabhakar, Jakob Rehof, César Sánchez, Ulrik Pagh Schultz, Helmut Seidl, Ilya Sergey, Peter Sestoft, Christian Skalka, Lau Skorstengaard, Gordon Stewart, Colin Stirling, Richard Trefler, Philip Wadler, Westley Weimer, and Thomas Wies.

Thanks are also due to the Department of Computing and Information Sciences at Kansas State University for hosting the Symposium during which we will offer Dave this Liber Amicorum. (In the etymological sense of the term, a Symposium is a gathering where people drink together, but we mean it in the modern sense: a meeting of scientists.)

But most of all, thanks to you, Dave, for your knowledge and for your generosity, for your teaching and for your mentoring, for your encouragements and for your modesty, for your service to the community, and throughout for your scholarship.


Personal Memories

Torben Amtoft (Kansas State University)

In 1989, at a party at the Copenhagen home of my Master advisor Neil Jones, I got to chat with a cheerful guy. Between jokes, he told me that he was from a place called Manhattan, Kansas. He had a hard time convincing me that he was not kidding.

This was my first encounter with Dave Schmidt. In the following decade, we frequently ran into each other at various places around the world. I much appreciated how Dave always greeted me with kindness and interest in my life and work.

In 2001, I finally witnessed first-hand the existence of Manhattan, Kansas. Dave had asked me to come for an interview, and as all hotels were booked, he opened up his home for me. Much later, he mailed me that he thought there were good chances I would be offered the position. After mentioning that to my office mate, a former student of Dave, I was assured that this was a very good sign: he knew Dave to be very honest with his words and never promise more than he can deliver.

In September of 2002, I arrived to start my new job, and Dave came the long way to Kansas City to pick me up at the airport. I was amazed that he could find the time for that, given that the next week he was going to be married to his Linda.

For 10 years now, I have had the pleasure of being a colleague of Dave. I keep being impressed by his vast knowledge of current and previous work in our field, and his ability to explain complex matters in the simplest possible way. We are many who hope he will not retire anytime soon!


David Schmidt: personal reflection

Michael Huth (Imperial College London)

On the occasion of David Schmidt’s Sixtieth Birthday, I would like to share some personal reflections of the man. Since he has been one of the most important shapers of my own professional career, it is perhaps inevitable and hopefully apt to see him through the prism of my own professional development. These reflections are meant both as an expression of deep gratitude and as an inspiration for others to follow his shining example as a scholar, teacher, and mentor.

I first met David Schmidt at the Seventh International Conference on Mathematical Foundations of Programming Semantics, in Pittsburgh, Pennsylvania, in March 1991. I had just finished my PhD studies at Tulane University and arrived at the welcome reception of what was then my second scientific conference. In the centre of the room sat David (henceforth referred to as “Dave”) surrounded by his students. He was easy to notice, with his beard, his bottle of beer, and the almost Italian use of gestures whilst passionately discussing semantic issues with those around him. Later in the evening, I learned that Dave had driven his own car all the way from Kansas to Pittsburgh just so that his students could also attend the meeting. And only a few days later he offered me a 1-year postdoc at Kansas State University saying that one of my duties would be to help with the supervision of a particular PhD student. He also apologized for the offer, saying that the money left in the grant did not amount to much.

I think that these first impressions painted a man who is passionate about both his work and the people that participate in it. It also suggested a man who possesses a great wealth of knowledge but who displays genuine modesty, and who is most respectful and helpful in his dealings with others. At that time, I had not yet been in the Midwestern United States and was therefore not very familiar with its people, their history, and values. But I think now that Dave and his student group were great ambassadors of that part of the world, and that the impression they left on me definitely influenced my decision to accept his gracious offer and move to Kansas. (Being lazy at the time, I also saw no reason to look for another job!)

Those who know Dave will not be surprised to learn that he was not only a great teacher, adviser, and mentor to me during this first postdoc: I honestly cannot remember how often he drove me around town in the first couple of weeks in order to get me set up with essentials (drivers license, rental, etc.). In the years to come, I learned that this dedicated care of those who passed through Kansas – be it for short, medium or long-term visits – was invariably his (gold) standard treatment!

Dave also understands that work is not everything. Not only did he allow me to join the university big band, which entailed four rehearsals a week and trips to concerts in Kansas and beyond. He also jokingly would tell others at social gatherings that he hired me to support my career as a jazz musician.

And back in those days, there were only few web pages around and research was still disseminated mostly through personal talks, printed publications, and tech reports that one might receive through surface mail. Dave always understood the importance of securing access to ongoing research and he was incredibly effective in getting leading people from the US, Europe, and beyond pass through Kansas for seminar talks and research visits. Quite a few famous people in programming languages I first met in Nichols Hall! I think this exposure to excellent research ideas and results played a big role in my decision to pursue a long-term career in academia.

That decision brought me back to Europe, where I was lucky enough to secure a few postdocs. In 1995, it was time to apply for my first permanent job. One application went to Kansas State University, to join the growing departmental presence of programming languages, software engineering, and verification. I was not too hopeful to make the shortlist. But I do remember getting a call from Dave one day, asking whether I would seriously consider this job. And I certainly did and, in the end, did get an offer which I gratefully accepted. So in August 1996 I packed my bags and moved back to Kansas.

I had five wonderful years there as Assistant Professor in the Department of Computing and Information Sciences. As you may suspect, Dave played a big part in making these years fruitful, enjoyable, and important for me and my professional development. Let me just mention some random evidence for this claim.

Dave’s influence on my teaching runs very deep. I carefully studied his books on denotational semantics and programming language design, like so many others did. These studies revealed to me that one can distill – through hard work – the essence of teaching material so that very technical issues can be conveyed via carefully chosen examples and presentational approaches. And that this not only makes these subjects accessible to a broader audience. But that such material is also truly appreciated by researchers themselves (although not all would be willing to admit this in public!).

The collaborations on research papers that I was blessed to have with Dave also showed me how he would incessantly think about how best to develop and present novel research so that the finished product would withstand the test of time. To this day, I try to live up to his standard, noting that my most cited papers are from the distant past and co-authored whilst in Kansas.

Dave’s influence on me as a manager has also been profound. I won’t attempt to provide any evidence for this. But I can only hope that my past, present, and future PhD students and Research Associates will recognize in my interaction with them at least the shadow of Dave’s compassion and dedication.

Any generation of researchers should consider itself to be lucky to have people like Dave, who will not find it beneath himself to give an invited talk at a workshop or conference in which he would portray seemingly basic and well known facts. But where the presentation would always connect dots and make points that would be genuinely valuable and would often provoke new research questions. I can only hope that Dave will continue to be such a skilled and competent raconteur, a passionate teacher, and first-rate researcher, and a dedicated mentor in many years to come!


A Tribute To Dave

Charles Consel (University of Bordeaux / Inria)

Like many other computer scientists, I first met David Schmidt through his book on Denotational Semantics. I knew a professor in Mathematics at the University of Paris VI who was interested in approaching Programming Languages from a formal angle. Thus, we set out to study this book by ourselves. During every session, this mathematician kept on praising the elegance and clarity with which the mathematical elements of Denotational Semantics were introduced. With my programming-language implementation background, I was equally impressed by the conciseness and clarity with which the very essence of programming language concepts was captured.

The first time I met David Schmidt in person was during the 1987 workshop on Partial Evaluation and Mixed Computation. A last-minute session for work-in-progress was organized and Olivier Danvy offered me to present early results of my PhD work. After long hours of hard work, here I was about to deliver my first talk in English in front of an audience including such giants as David Schmidt and Neil Jones. Well, I guess that was just too much for me to cope with: words couldn’t come out of my mouth! At least, not in a form that humans could understand. David Schmidt and others showed infinite patience, asking simple questions, guiding me in my answers. Despite this rather miserable first meeting with David Schmidt, he eventually invited me to visit him at Kansas State University a few months later, and made me the honor of serving as an examiner for my PhD defense, together with Neil Jones. David Schmidt has been a continuing source of inspiration in my career for his work and for his kindness and support towards accomplished computer scientists as well as students. His way of sharing his knowledge is an invitation to his audience to engage in investigating further a given topic.

Over the course of my career, I have studied many areas beyond programming languages, including Network [4], Telecommunications [1], Operating Systems [3], and Software Engineering [2]. In doing so, one recurring observation I have made to myself is how much Programming Language concepts are fundamental to all these other areas, and how much could be gained by promoting further David Schmidt’s concepts. Indeed, this programming language-driven approach can, for example, support (1) the design of declarations for a distributed system using the principles of abstraction, correspondence and qualification, (2) the separation between their static and dynamic semantics as a basis to examine verification and compilation issues, and (3) the definition of a combinator-based semantics to abstract over underlying intricacies and achieve portability. Besides providing solid, formal foundations, these Programming Language concepts can spread the design taste and principles that have been praised in landmark programming languages, such as Algol.

At this point Dave, I guess I don’t need to emphasize further how much you influenced my approach to research in Computer Science; I am deeply thankful for that. I wish you the best for your future projects, and please do continue to enlighten us with your profound understanding of our research field.

References

[1]   Laurent Burgy, Charles Consel, Fabien Latry, Julia Lawall, Nicolas Palix & Laurent Réveillère (2006): Language technology for Internet-telephony service creation. In: Communications, 2006. ICC’06. IEEE International Conference on, 4, IEEE, pp. 1795–1800, doi:10.1109/ICC.2006.254980.

[2]   Damien Cassou, Julien Bruneau, Charles Consel & Emilie Balland (2012): Toward a Tool-Based Development Methodology for Pervasive Computing Applications. IEEE Trans. Software Eng. 38(6), pp. 1445–1463, doi:10.1109/TSE.2011.107.

[3]   Fabrice Mérillon, Laurent Réveillère, Charles Consel, Renaud Marlet & Gilles Muller (2000): Devil: An IDL for Hardware Programming. In: 4th Symposium on Operating Systems Design and Implementation (OSDI 2000), San Diego, California, pp. 17–30, doi:10.1.1.178.5596.

[4]   Scott Thibault, Charles Consel & Gilles Muller (1998): Safe and Efficient Active Network Programming. In: 17th IEEE Symposium on Reliable Distributed Systems, West Lafayette, IN, pp. 135–143, doi:10.1109/ RELDIS.1998.740484.