There is also a list by kind of publication (book, journal article, conference paper, book chapter...).
Last updated on 25 September 2023.
For online versions of publications (all recent ones, and many older ones), follow the right-margin links.
Almost every entry carries a note about the content and sometimes the circumstances of publication.
(See here for a raw list with neither notes nor links nor separation by years.)
Mostly devoted to software enginering, but with forays into other areas — hence “technology+”. About 200 articles so far. Some are short entries, but many are essays or even short technical papers that it is just as simple to publish in this format. Some of the more significant articles are listed in this bibliography.
I post every once in a while to the Communications of the ACM blog, complementing my own blog . Some of the more significant articles are listed in this bibliography.
Coming out of our teaching of concurrency at ETH and the work of SCOOP, a textbook showing that it is possible to make concurrent programming both simple and reliable. Likely release: early 2024.
 (Ongoing) Standard Eiffel (revised edition of ), in progress.
All our teaching material is open-source and can be used freely. We appreciate attribution. Usually both PDF and PowerPoint versions are available on the course pages.
Partial list of courses: Software Construction, Architecture and Engineering (at Constructor, since 2019), Introduction to Programming (English and German versions), Software Architecture, Software Engineering, Concepts of Concurrent Computation, Software Verification (ex-Trusted Components), Object-Oriented Software Construction (ex-Advanced Topics in Object Technology), Distributed Software Engineering Laboratory (ex-Distributed and Outsourced Software Engineering, ex-Software Engineering for Offshore Development), Concurrent Object-Oriented Programming, Programming in the Large, Java and C# in Depth.
Part of a series of articles on the combination of tests and proofs. Existing work on program repair typically needs to execute proposed fixes to see if they pass previous tests -- a slow and uncertain approach. Here we use a prover instead.
 With Manuel Oriol and Huang Li Seeding Contradiction: a fast method for generating full-coverage test suitesa, in ICTSS 2023, proceedings of 35th IFIP International Conference on Testing Software and Systems, Bergamo (Italy), 18-21 September 2023.
A new method for achieving full test coverage, very fast, without execution. Detailed description will be added soon.
For the general spirit of the work leading to this patent see .
For many years I have been fascinated by the complementarity between proofs and tests. That was the original impetus for the creation of the Tests And Proofs (TAP) conference with Yuri Gurevich and the combined development of the AutoProof      and AutoTest              verification tools. One important idea that we are exploring now is how to take advantage of a prover to generate high-quality tests. The inability to prove a program correct, a common occurrence in attempts at program verification, can be frustrating, but it also enables the prover to produce a counter example, which we can use both to understand the reason for the proof's failure (usually due to a bug in the program) and to generate a useful test for the program's regression test suite.
 With Maria Naumcheva, Sophie Ebersold, Alexandr Naumchev, Jean-Michel Bruel, and Florian Galinier: Object-Oriented Requirements: a Unified Framework for Specifications, Scenarios and Tests, in JOT (Journal of Object Technology), vol. 22, no. 1, 2023, pages 1-19.
An article explaining how object-oriented requirements subsume use cases and other scenario techniques. Partly based on ideas from my requirements book  (see also the shorter and more informal treatment of the topic in a blog article ) but including a significant case study developed by Maria Naumcheva: Roborace software for Formula-1 cars.
(Revised version of  — which is from 2016, so one can see it took over 6 years to complete. Note the addition of coauthors.
In fact  was itself based on  from 2005, and the roots of the work go back to the description of class invariant semantics in Object-Oriented Software Construction in 1997  and 1988 . See also the “flexible invariants”  work from 2014.
The following summary is the abstract from the paper itself.)
There is no “French School of Programming” in the strict sense but a group of brilliant researchers who share a passion for simplicity and elegance. This book collects a number of specially written articles by some of the topmost members of that group, including Patrick Cousot, Gérard Berry, Joëlle Coutaz, Marie-Claude Gaudel, Michel Raynal, Jean-Marc Jézéquel, Jean-Pierre Jouannaud, Jean-Pierre Briot, Giuseppe Castagna and their colleagues. The preface is by Jim Woodcock.
 Right and Wrong: Ten Choices in Language Design, to appear in The French School of Programming, ed. Bertrand Meyer, Springer, 2023 ().
Object-oriented programming has achieved wide success but often in a corrupted form. This article goes back to the principles, explains how many OO languages violate some of them, and gives in some depth the rationale behind the design of Eiffel, meant to ensure the production of high-quality software.
 Online version of Object Success , released March 2023.
This is not a new book but an online, fully hyperlinked version of  from 1995, with a few minor updates.
My latest published book, a general survey and textbook of requirements analysis. Introduces a comprehensive view of requirements among 4 dimension or PEGS: Project, Environment, Goals and System. Covers how to write good requirements, how to conduct an effective requirements process, the place of requirements in the project lifecycle (whether traditional or agile), object-oriented requirements, the role and limitations of use cases, formal approaches...
A note discussing the inadequacy of the word “statement” to mean “instruction”.
 What Do ChatGPT and AI-based Automatic Program Generation Mean for the Future of Software (blog article), in Communications of the ACM blog , 23 December 2022.
An examination of the shock provoked by ChatGPT, confirmation that it is a game-changer, and analysis of what it means for the profession.
Use cases, user stories and other scenario-based techniques are the preferred mode of requirements specification in much of the industry. They rely on prescribing the order of operations early ̀ too early. This article, drawn in part from material in my requirements book , argues that using logical constraints, in the form of contracts in an object-oriented specification, leads to more general and useful requirements.
 How To Teach (blog article), in Communications of the ACM blog , 21 December 2022.
A presentation of a teaching technique adapted to the modern era, taking advantage of electronic resources, particularly MOOCs, and using a “Socratic” technique to foster interaction and in-depth learning.
Part of a series of articles on the combination of tests and proofs; see . Explain how one can start from a counter-example generated by a program prover after a failed verification attempt, and optimize it so that it yields a test case easily understandable by a programmer.
A supplement to my article on Barry Boehm's life and work , recalling a tongue-in-cheek exercise in his book.
 Online version of Object-Oriented Software Construction, second edition , released September 2022.
This is not a new book but an online, fully hyperlinked version of  from 1997, with a few small updates reflecting changes in syntax.
For the general spirit of the work leading to this patent see e.g. .
Barry W. Boehm was a pioneer of software engineering, introducing rigor into studies of software projects and devising the widely used COCOMO cost estimation model. His 1981 book “Software Engineering Economics” founded the field. I was privileged to know him from early on and wrote this article to summarize some of his accomplishments. See also .
 With Alfredo Capozucca, Jean-Michel Bruel and Manuel Mazzara (editors): Special Issue on New Paradigms of Software Production and Deployment>, in Springer Nature Computer Science, vol. 3, no. 2, 2022.
A collection of articles coming out from the DEVOPS 2019 workshop at Villebrumier (proceedings were published as ) on innovative approaches to software project organization.
 With Jean-Michel Bruel, Sophie Ebersold, Florian Galinier, Manuel Mazzara and Alexandr Naumchev: The Role of Formalism in System Requirements, in ACM Computing Surveys, vol. 54, no. 5, pages 1-36, June 2022.
A general survey on formal (mathematical) approaches to specification, covering a wide variety of approaches. Techniques covered go from natural-language (Requirements Grammar, Relax, NL to OWL...) to the semi-formal (Reqtify, KAOS, SysML, URML...) to automata-based (Statecharts, Problem Frames, Petri Nets) to fully formal (Event-B, Alloy, VDM...) and seamless (multirequirements). A significant example, a Landing Gear System, is used throughout to illustrate and contrast the approaches.
An attempt to summarize some of my scientific contributions, acknowledged or not, over the years.
The Personal Software Process, devised by Watts Humphrey (see ), is largely forgotten but can provide useful guidance, suitable for the age of modern agile development.
For the 60-th anniversary of IFIP, the International Federation for Information Processing, Leon Strous, the president, asked me to write a survey of the history and challenges of the software engineering field, as part of a collection of such chapters about the future of computing.
 With Jean-Michel Bruel, Alfredo Capozucca, Manuel Mazzara, Alexandr Naumchev and Andrey Sadovykh: Frontiers in Software Engineering Education, Proceedings of First International Workshop, FISEE 2019, Villebrumier, France, November 11-13, 2019, Invited Papers, Springer Lecture Notes in Computer Science 12271, 2020.
The first of a series of worskhops on software engineering education held in the outstanding venue provided by the Château de Villebrumier. The second in the series, postponed (thanks, Covid), will take place in January 2023.
 With Jean-Michel Bruel and Manuel Mazzara: Software Engineering Aspects of Continuous Development and New Paradigms of Software Production and Deployment, Proceedings of Second International Workshop, DEVOPS 2019, Villebrumier, France, May 6-8, 2019, Revised Selected Papers. Springer Lecture Notes in Computer Science 12055, 2020.
It can be difficult to get a program right, even a seemingly simple program like binary search. This blog articles (previously published in nine successive post on the Communications of the ACM blog , each but the last asking the reader to criticize the current version before it is corrected in the next one) proposes successive versions of binary search, most beset by subtle but often fatal bugs.
A general approach to handling the issue of alias analysis in software verification.
A comprehensive survey of formal (mathematical) approaches to requirements and specifications. The version published two years later, , benefits from extensive revisions), but this one includes coverage of some approaches that we had to remove because of space constraints.
An examination of what it means for requirements to be “complete”, using in particular the notion of “ ” in abstract data types (Guttag-Horning). A chapter of the later “Requirements Handbook”  expands on these ideas and defines an even more “complete” version of requirements completeness.
A general reflection on the teaching and use of algorithms, prompted in part by demonstrations by students in the UK about admission procedures.
As Barry Boehm (see ) explained as early as 1981 and many later studies confirmed, every project has a “ ” cost and development time, and however hard you work and how much money you spend you cannot gain more than 25%. This result is one of the few certainties we have about software project management and can legitimately be called a theorem. This blog article explains it. Communications of the ACM republished it later as a regular article .
A commented list of my publications on computer science and software engineering education, up to that time.
 Editor, with Manuel Mazzara, Jean-Michel Bruel and Alexander K. Petrenko: TOOLS 51: Software Technology: Methods and Tools, Proceedings of 51st International Conference, Kazan, October 15-17, 2019, Springer Lecture Notes in Computer Science 11771, 2019.
After a temporary stop, TOOLS restarted in in 51st (!) iteration in Kazan, following the tradition of quality of previous conferences in the series.
Part of a systematic effort to define requirements concepts precisely. Much of the material found its way into my requirements textbook .
 With Alexandr Naumchev, Manuel Mazzara, Florian Galinier, Jean-Michel Bruel and Sophie Ebersold: AutoReq: Expressing and verifying requirements for control systems, in Journal of Computer Languages, vol. 51, pages 131-142, 2019.
Software requirements can be seamless    , expressed in a suitable programming language; they can also be verified thanks to the appearance of such tools as AutoProof . The approach can fruitfully be applied to embedded systems and, in the case study of this article, it uncovered an error in a previously published formal description.
What makes an analysis sound? What makes it complete? In their application to the correcness and verification of programs, the notions of soundness, completeness, precision and recall are widely misunderstood. The terms “false positives”' and “false negative”' are also fraught with potential confusion. This article attempts to clarify these important concepts.
 With Jean-Michel Bruel and Manuel Mazzara: Software Engineering Aspects of Continuous Development and New Paradigms of Software Production and Deployment, Proceedings of First International Workshop, DEVOPS 2018, Villebrumier, France, March 5-6, 2018, Revised Selected Papers, Springer Lecture Notes in Computer Science 11350, 2019.
The proceedings of the first in a series of Villebrumier workshops; see  for the second one.
What is the use of formal methods in requirements? A productive technique, for delicate parts of requirements, is to devise a mathematical specifcation, then come back to English, leading to a natural-language specification that is both precise and readable by ordinary stakeholders. There was already a hint of this “formal picnic ” approach in the early “Formalism in Specications” paper ; this 2018 blog article presents it in more generality. The approach is developed further and illustrated with a full example in the 2022 Handbook of Requirements and Business Analysis .
I find it increasingly hard to understand how people can program without the benefit of contracts and in particular class invariants. This article shows an example of detailed contracts serving to keep under control a sophisticated data structure which would otherwise be very hard to get right.
An invited paper assessing agile methods, based on my Agile! book . It discusses, beyond the hype, the benefits and dangers of agile principles and practices, focusing on concrete examples of what helps and what hurts.
In recent years software engineering research has increasingly turned to empirical techniques. This article, based on keynote talks at ESEM and ESEC-FSE, discusses the proper place of empirical research in the overall software engineering discipline.
A short essay on the role and future of software engineering as a discipline.
An early version, not published, of .
I was asked to give a keynote on computers and ethics. Looking at classical views of ethics from Aristotle and Kant onwards reveals theories that do not sustain a minute's examination by someone used to rational thinking as practiced in science and technology. I decided to forget about computers, except as a source of examples, and focus on defining ethics instead, developing a basis for sound and practical ethical principles.
A design pattern for conveniently using execution arguments in Eiffel.
The PAUSE symposium was held in the new conference and seminar center of Villebrumier near Toulouse to mark the closing of my group, the ETH Chair of Software Engineering, after 14 years. The participants were some of the top names from many areas of software engineering. This volume collects some of their contributions.
The Chair of Software Engineering existed at ETH Zurich from October 2001 to January 2016. Originally written as a chapter for the PAUSE symposium , but rejected, this history of the Chair covers both teaching and research.
Our work on requirements, in line with a general approach to object-oriented development emphasizing seamlessness (going back to Object-Oriented Software Construction ), promotes the use of the same concepts and a single notation for requirements as well as design and code. The multirequirements paper  laid out a basis for the desirable requirements process. Alexander Naumchev is taking the approach further; in this paper we continue to refine the requirements process and mmake it applicable to large projects. See also .
(Superseded by .)
Class invariants are a key concept of object-oriented programming and essential to the verification of OO programs, but raise theoretical issues that have only received unsatisfactory answers so far —-- unsatisfactory in that they impose on programmers an unacceptable extra annotation burden.
This article classifies the open problems under two headings, furtive access and reference leak, and proposes a comprehensive solution requiring no annotations and no new language constructs.
Part of ongoing work to define athe semantics of the SCOOP concurrent programming model and particularly to define no-deadlock conditions. Combines ideas from Rewriting Logic and Maude (as in Benjamin Morandi's work ) and alias analysis to define a new approach.
 With Alexander Naumchev: Complete Contracts Through Specification Drivers, in TASE 2016, 10th International Symposium on Theoretical Aspects of Software Engineering, Shanghai, 17-19 July 2016, IEEE Computer Society, 2016, pages 160-167,
The idea of specification drivers provides a new way to integrate precise, formal elements to requirements. It also introduces a new way to make object-oriented specifications complete, an interesting alternative or complement to the technique of model queries    ref which we previously introduced and used in the verification of EiffelBase2. A specification driver is a specification element that talks about some part of the software specification or implementation. Look in particular for the description of stacks, expressing the full power of a mathematical Abstract Data Type specification within the context of an imperative OO programming language.
In the SmartWalker project we developed a modern, computer-equipped version of the (hopelessly low-tech) walkers used by elderly people and others with limited mobility. The SmartWalker performs many tasks to help its users. Internally it rests on a sophisticated hardware and software architecture; the software relies on the SCOOP concurrency framework for Eiffel and specifically the Roboscoop robot programming system developed by Andrey Rusakov. We are actively looking for industrial collaboration to develop the prototype further.
 With Mischael Schill and Christopher M. Poskitt: An Interference-Free Programming Model for Network Objects, in COORDINATION 2016, Proc. 18th IFIP International Conference on Coordination Models and Languages, Heraklion, Greece, Lecture Notes in Computer Science 9686, Springer, pages 227-244.
Making SCOOP ready for distributed programming, with the concept of network objects.
 With Alexey Kolesnichenko, Christopher M. Poskitt and Sebastian Nanz: Contract-based general-purpose GPU programming, in GPSE 2015, Proceedings of 2015 ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, ACM SIGPLAN Notices, vol. 51, Issue 3, March 2016, pages 75-84.
GPU programming typically uses low-level primitives. This paper describes a simple approach to GPU programming based on the SCOOP model.
 Theory of Programs, in Proceedings of LASER summer school on Software 2013-2014 2007/2008, eds. Bertrand Meyer and Martin Nordio, Advanced Lectures on Software Engineering, Lecture Notes in Computer Science 8987, Springer, 2015 .
The basis of a general theory of programs, programming languages and programming, entirely relying on three operations from elementary set theory. Covers concurrency, refinement, axiomatic semantics and many other concepts heretofore considered advanced.
 (Editor, with Martin Nordio) Software Engineering; International Summer Schools, LASER 2013-2014, Elba Island, Italy, Revised Tutorial Lectures; Lecture Notes in Computer Science 8987, Springer, 2015.
 With Alexander Naumchev and Victor Rivera: Unifying Requirements and Code: an Example, in Perspective of System Informatics, Proceedings of fifth Andrei Ershov Memorial Conference, Kazan, 24-27 August 2015, eds. Manuel Mazzara and Andrei Voronkov,Lecture Notes in Computer Science 9609, Springer, 2015, pages 233-234.
 With Scott West and Sebastian Nanz: Efficient and Reasonable Object-oriented Concurrency , in ESEC/FSE 2015, Proceedings of 2015 European Software Engineering Conference and Foundations of Software Engineering Symposium, ACM Press, 2015, pages 734-744.
Recent work on SCOOP (by Scott West and others, building on earlier improvements by Benjamin Morandi and others), as part of the Concurrency Made Easy ERC project, has resulted in spectacular improvements of concurrent programming performance. This paper describes the techniques and the results.
 With Jiwon Shin, David Itten and Andrey Rusakov: Towards an Intelligent Robotic Walker for the Elderly, in 11th International Conference on Intelligent Environments (IE 11), Prague,17-19 July 2015, IEEE, August 2015 (best paper award).
 With Paolo Antonucci, Christian Estler, Durica Nikolic and Marco Piccioni: An Incremental Hint System For Automated Programming Assignments, in ITiCSE '15, Proceedings of 2015 ACM Conference on Innovation and Technology in Computer Science Education, 6-8 July 2015, Vilnius, ACM Press, pages 320-325.
In connection with the Codeboard automated program compilation and execution system, designed by Christian Estler and others and used extensively both in our courses and in our MOOCs, Paolo Antonucci in his master's thesis, supervised by Marco Piccioni, built a clever mechanism to help students answer exercises, through successive hints that the instructor can prepare for each question. A clueless students can get more and more help by pressing the Hint button repeatedly.
 With Jiwon Shin and Ivo Steinmann: Automatic Speed Control for SmartWalker, in PETRA 2015, Proceedings of 8th ACM International Conference on PErvasive Technologies Related to Assistive Environments, 21-23 June 2015, Rhodes, Greece, ACM Press, 2015.
Part of the work on the SmartWalker mobility-assistance robot, see . The speed-control mechanism of SmartWalker, as devised by Ivo Steinmann during his master's thesis supervised by Jiwon Shin.
 With Jiwon Shin and Andrey Rusakov: Concurrent Software Engineering and Robotics Education, in 37th International Conference on Software Engineering (ICSE 2015), Florence, May 2015, IEEE Press, pages 370-379.
The Roboscoop project applies concurrency and modern software engineering techniques to robot programming. Since 2013 we are holding at ETH a multi-disciplinary course, the “Robotics Programming Laboratory”, teaching robotics software to students from computer science as well as mechanical engineering and electrical engineering. This paper presents empirical results on the results of the course.
 With Yu Pei, Carlo A. Furia and Martin Nordio: Automated Program Repair in an Integrated Development Environment, in 37th International Conference on Software Engineering (ICSE 2015), Florence, May 2015, IEEE Press, pages 681-684.
Our AutoFix tool suite provides the ability to suggest high-quality fixes for bugs. Previous papers on AutoFix (see , , ) described the theory, applications and experimental results. In this one we discuss how automatic fixing fits in an integrated development environment, where AutoFix collaborates with other development and verification tools. One of the key aspects is timeliness: how can we ensure, in spite of the time AutoFix needs to produce good fix candidates, that it provides users with useful feedback fast enough? Only under that condition can AutoFix hold it promises for improving the development process.
 An automatic technique for static deadlock prevention, in PSI 2014 (Ershov Informatics Conference), eds. Irina Virbitskaite and Andrei Voronkov, Lecture Notes in Computer Science 8974, Springer, 2015, pages 45-58.
Deadlocks remain one of the biggest threats to concurrent programming. Usually, the best programmers can expect is dynamic deadlock detection, which is only a palliative. Object-oriented programs, with their rich reference structure and the resulting presence of aliasing, raise additional problems. The technique developed in this paper relies on the alias calculus to offer a completely static and completely automatic analysis of concurrent object-oriented programs. The discussion illustrates the technique by applying it to two versions of the dining philosophers program, of which it proves informally that the first is deadlock-free and the second deadlock-prone. The technique is still incomplete but, I think, promising. It is one more application of the alias calculus  .
 With Scott West and Sebastian Nanz: Efficient and Reasonable Object-oriented Concurrency , in PPoPP 2015, Proceedings of the 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, San Francisco, 7-11 February 2015, ACM SIGPLAN Notices, vol. 50, no. 8, August 2015, pages 273-274.
An earlier two-page summary of the work reported more completely later that year at ESEC .
 Framing the Frame Problem, in Dependable Software Systems, Proceedings of August 2014 Marktoberdorf summer school, eds. Alexander Pretschner, Manfred Broy and Maximilian Irlbeck, NATO Science for Peace and Security, Series D: Information and Communication Security, Springer, 2015, pages 174-185.
The “frame problem” is one of the critical open problems in software verification, particularly for object-oriented programs. It denotes the question of how to specify and verify what properties of a program do not change in the execution of a given operation. For example, a withdrawal operation on a bank account, which changes the balance, should not change the account number, the name of the account holder and many other properties. The frame problem is both a specification problem and a verification problem: how to specify what does not change, without listing most properties in most operations; and how to verify that operations indeed change only what they are permitted to change. The article proposes a “double frame inference” method which computes the frame (the set of unchanged properties) on both the specification and verification sides. For specification, it deduces the frame from the list of properties mentioned in the postcondition. For verification, it examines the code and applies the alias calculus developed in other papers (e.g. , as well as  which contains a first sketch of the techniques discussed here).
 With Alexander Kogtenkov and Sergey Velder: Alias Calculus, Change Calculus and Frame Inference, in Science of Computer Programming, 2015, pages 163-172, DOI 10.1016/j.scico.2013.11.006 (first published online 26 November 2013).
A new development of the work on alias analysis (see  and ). It describes an improvement of the alias calculus, with a corrected version of the assignment axiom, and an important application to the issue of frame inference. The prospect now exists of using alias analysis to infer frame conditions entirely automatically; in experiments using Alexander Kogtenkov's implementation, all the frame conditions of an example library were inferred, including some that had been missed in manually written “modifies” clauses, and with very few spuriously inferences. (A more recent description of the application to framing appears in .)
An analysis of agile approaches and assessment of their positive and less positive contributions. This book is the result of immersing myself into agile methods for some four years. I found that they are a mixture of the best and the worst; brilliant ideas coexist with damaging advice. The book sorts out the gems from the gravel. It serves as a tutorial, explaining the key agile concepts, as well as a reasoned critique, discussing agile methods in the broader context of software engineering knowledge and identifying the key ideas that truly help software projects.
 With Cristina Pereira, Hannes Werthner and Enrico Nardelli: Informatics Education in Europe: Institutions, Degrees, Students, Positions, Salaries — Key Data 2008-2013, Informatics Europe report, October 2014.
The 2014 edition of  (see the explanations there). Not only updated but significantly improved in content and form, with the inclusion of new countries and : better presentation of the results through graphics,
 With Andrey Rusakov and Jiwon Shin: Simple Concurrency for Robotics with the Roboscoop Framework, in IROS 2014 (IEEE/RSJ International Conference on Intelligent Robots and Systems, Chicago, 14-18 September 2014, IEEE Computer Press.
The first published presentation of the Roboscoop framework for developing reliable robotics applications, taking advantage of concurrency. We have applied Roboscoop to a number of systems, including the SmartWalker robot for assisting elderly persons better than with ordinary walkers.
 With H-Christian Estler, Martin Nordio and Carlo A. Furia: Awareness and Merge Conflicts in Distributed Software Development, in proceedings of ICGSE 2014, 9th International Conference on Global Software Engineering, Shanghai, 18-21 August 2014, IEEE Computer Society Press (best paper award).
A novel approach to handling configuration management in a distributed environment, with minimum overhead on the programmer's work. Part of Christian Estler's thesis work.
Hidden deep into a video lecture by Leslie Lamport is an interesting discussion about Quicksort, showing that recursion is neither essential to the algorithm nor even needed for it. He sketches an element non-recursive version. This article explains the idea and provides an implementation in Eiffel, which turns out to have just the right language mechanisms.
 With Marco Piccioni and H-Christian Estler: SPOC-supported introduction to Programming, in Proceedings of ITiCSE 2014, 9th Annual Conference on Innovation and Technology in Computer Science Education, June 23-25, 2014, Uppsala, Sweden.
A description of the experience with our first online course, directly associated with our ETH Introduction to Programming course and primarily aimed at our own students although in fact anyone can use it.
 With Benjamin Morandi and Sebastian Nanz: Safe and Efficient Data Sharing for Message-Passing Concurrency, in proceedings of COORDINATION 2014, 16th International Conference on Coordination Models and Languages, Berlin, 3-6 June 2014, Lecture Notes in Computer Science 8459, eds. E. KÃ¼hn ad R. Pugliese, 2014, pages 99-114.
The SCOOP concurrency model has a clear division of objects into “regions”, improving the clarity and reliability of concurrent programs by establishing a close correspondence between the object structure and the process structure. Each region has an associated “processor”, which executes operations on the region's objects. A literal application of this rule implies, however, a severe performance penalty. Benjamin Morandi found out that a mechanism for specifying certain processors as “passive” yields a considerable performance improvement. The paper describes the technique and its applications.
On the occasion of an article in InfoWorld about fashionable programming languages, an assessment of some of what they do wrong and what they just took over from Eiffel.
 With H.-Christian Estler, Carlo A. Furia, Martin Nordio and Marco Piccioni: Contracts in Practice, in FM 2014 (proceedings of 19th International Symposium on Formal Methods), Singapore, May 2014, Lecture Notes in Computer Science 8442, eds. C. Jones, P. Pihlajasaari and J. Sun, Springer, 2014, pages 230-246.
For almost anyone programming in Eiffel, as evidenced by Patrice Chalin's pioneering study of a few years ago (reference 2 of the bibliography), contracts are just a standard part of daily life. The present paper is a much larger study, making it possible to understand how developers actually use contracts when available.
It covers 21 programs, not just in Eiffel but also in JML and in Code Contracts for C#, totaling 830,000 lines of code, and following the program's revision history for a grand total of 260 million lines of code over 7700 revisions. It analyzes in detail whether programmers use contracts, how they use them (in particular, which kinds, among preconditions, postconditions and invariants), how contracts evolve over time, and how inheritance interacts with contracts.
 With Nadia Polikarpova, Julian Tschannen and Carlo A. Furia: Flexible Invariants Through Semantic Collaboration, in FM 2014 (proceedings of 19th International Symposium on Formal Methods), Singapore, May 2014, Lecture Notes in Computer Science 8442, eds. C. Jones, P. Pihlajasaari and J. Sun, Springer, 2014, pages 514-530.
One of the crucial issues in the verification of object-oriented programs is to provide a correct semantics for invariants. The “semantic collaboration” approach developed by Carlo Furia, Nadia Polikarpova and Julian Tschannen, simplifying techniques due among others to Leino, Leavens and Müller, is a sound solution. It relies on annotations provided by programmers to specify ownership and subject-observer properties. This technique has been extensively used in the AutoProof system , in particular for the verification of the EiffelBase 2 library .
A short essay emphasizing the role of programming language choices in the quality of the resulting programs.
Marked the final step in the implementation of void safety , freeing Eiffel programmers once and for all from the plague of null-pointer dereferencing: the time when we made “ ” (guaranteed non-void) the default. We never looked back!
 With Alexander Kogtenkov: Negative Variables and the Essence of Object-Oriented Programming, in Specification, Algebra, and Software, Kanazawa (Japan), 14-16 April 2014, Lecture Notes in Computer Science 8373, eds. Shusaku IIda, Jose Meseguer and Kazuhiro Ogata, Springer, 2014, pages 171-187.
A specification and verification technique that describes the specific nature of object-oriented programming and takes into account its principle of “general relativity”. It makes it possible to reason about object-oriented programs, handling properties of the global data structures that cannot even be expressed in the traditional approach relying on substitution. .
Loop invariants lie at the core of axiomatic techniques for program specification and verification. To design a loop or understand an existing loop is to design or understand its invariant. In this extensive survey article we review the concept, explain its role in program construction, propose a classification loop invariants, and review the loop invariants of many key algorithms across many areas of computer science. We also study techniques of invariant inference. All the examples have been mechanically verified using Boogie. We hope this article will contribute to the understanding of program construction and program correctness.
An analysis of the CMMI project management model (Capability Maturity Model Integration), indluding not only its limitations but also (in spite of the title) what is interesting about it.
 With Sebastian Nanz, Scott West, Kaue Soares Da Silveira: Benchmarking Usability and Performance of Multicore Languages, in ESEM 2013 (ACM/IEEE International Symposium on Empirical Software Engineering and Measurement), Baltimore, 10-11 October 2013, IEEE Computer Press, 2013, pages 183-192.
A performance comparison of four parallel languages: Chapel, Cilk, Go and TBB. Notably absent is SCOOP — that will come.
 With Marco Piccioni and Carlo A. Furia: An Empirical Study of API Usability, in ESEM 2013 (ACM/IEEE International Symposium on Empirical Software Engineering and Measurement), Baltimore, 10-11 October 2013, IEEE Computer Press, 2013, pages 5-14.
A systematic empirical study of API choices, assessed by interviewing programmers who were asked to try several variants of an API for a persistence library.
From the beginnings of Informatics Europe (the association of university departments and industrial research labs in computer science in Europe) it was clear that one of the principal tasks would be to collect the facts. The report is one of the first results of this effort. The principal author is Cristina Pereira, who collected and organized the relevant data over more than a year; I helped with the preparation of the final text.
 With Alexey Kolesnichenko and Christopher M. Poskitt: Applying Search in an Automatic Contract-Based Searching Tool, in SSBSE 2013 (5th Symposium on Search-Based Software Engineering), Saint Petersburg, 24-26 August 2013, Lecture Notes in Computer Science 8084, eds G. Ruhe and Y. Zhang, 2013, pages 318-323.
The core performance problem in automated random testing, as implemented in AutoTest (see the many references in this bibliography), is to maximize the likelihood of breaking a postcondition. This work, started by Alexey Kolesnichenko, uses search techniques to that effect.
 With Mischael Schill and Sebastian Nanz: Handling Parallelism in a Concurrency Model, in Multicore Software Engineering, Performance and Tools (MUSEPAT 2013), Saint Petersburg, 19-20 August 2013, Lecture Notes in Computer Science 8063, eds. J.M. LourenÃ§o and E.Farchi, Springer, 2013, pages 37-48.
The SCOOP mechanism provides a simple, safe and elegant approach to handle synchronization, but until now does not offer the kind of performance that one may expect for highly parallelizable programs as they arise for example in scientific computations. Mischael Schill's idea of slices adds library support for computations with arrays, with dramatic performance improvements.
 With Alexey Kolesnichenko and Sebastian Nanz: How to Cancel a Task, in Multicore Software Engineering, Performance and Tools (MUSEPAT 2013), Saint Petersburg, 19-20 August 2013, Lecture Notes in Computer Science 8063, eds. J.M. LourenÃ§o and E.Farchi, Springer, 2013, pages 61-72.
Alexey Kolesnichenko is studying useful design patterns for concurrent programs and in this particular paper explores a challenging problem: what happens when a program has started a number of parallel tasks and wants to cancel one of them? This is a survey paper on existing approaches, but it also proposes novel ways to handle the issue of task cancellation.
 With H-Christian Estler, Martin Nordio and Carlo A. Furia: Distributed Collaborative Debugging, in ICGSE 2013 (8th IEEE International Conference on Global Software Engineering, Bari, 26-29 August 2013 (best paper award).
 With Benjamin Morandi and Sebastian Nanz: Testing a Concurrency Model, in ACSD 2013 (13th IEEE International Conference on Application of Concurrency to System Design, Barcelona, 8-10 July 2013, IEEE Computer Press, 2013, pages 170-179.
How does one get a language mechanism, in this case the delicate details of a concurrency mechanism, right? One approach is to rely on Jose Meseguer's Maude specificaton framework, whose specifications are executable and hence can be executed. Benjamin Morandi did this for the SCOOP concurrency mechanism, and in the process was able to fine-tune some important semantic details, and try out various designs for aspects such as exception handling in a concurrent context. The paper describes an original and productive way to support innovative language design through experimentation.
Requirements can be conducted at multiple interwoven levels: formal, graphical, textual (natural language). Each level provides what it does best: precision, clear view of the structure, detailed explanation. The requirements are also object-oriented in the true sense of the term, based on classes, contracts and inheritance. I believe this is the right way to do requirements.
 With H-Christian Estler, Martin Nordio and Carlo A. Furia: Unifying Configuration Management with Awareness Systems and Merge Conflict Detection, in 22nd Australasian Software Engineering Conference, Melbourne (Australia), 4-7 June 2013.
 With Julian Tschannen, Carlo A. Furia and Martin Nordio: Program Checking With Less Hassle, in proceedings of VSTTE 2013 (Verified Software: Theories, Tools and Experiments), Atherton (California), May 2013, Lecture Notes in Computer Science 8164, eds. E. Cohen and A. Rybalchenko, Springer, 2013, pages 149-169.
A presentation of “two-step verification” as implemented in the EVE verification environment, which integrates a number of verification tools as part of a single IDE.
 With Sebastian Nanz, Faraz Torshizi and Michela Pedroni: Design of an Empirical Study for Comparing the Usability of Concurrent Programming Languages, in Information and Software Technology Journal Elsevier, volume 55, 2013.
(Revised and extended journal version of , best paper award of ESEM 2011.) An empirical study comparing the ease of learning of two concurrency models, SCOOP and Java threads. Since we are deeply involved in SCOOP, one of the most delicate aspects was to guard against experimenter bias. I discussed the background of this paper and methodological issues of empirical software engineering in a series of blog postings in June 2011.
 With Nadia Polikarpova, Carlo A. Furia, Yi Pei and Yi Wei: What Good are Strong Specifications?, in proceedings of ICSE 2013 (35th International Conference on Software Engineering), San Francisco, May 2013.
This is a continuation of our work on equipping software with extensive contracts expressing full specifications rather than the partial properties used in Design by Contract; see  and  for the initial forays into this area. The article shows that the extra effort of writing stronger specifications pays off in many respects, beginning with far more faults found in testing.
I gave the 2013 “Ershov lecture”, held annually (in Russian) in memory of the great Soviet computer scientist Andrey Ershov (see ). I talked about SCOOP and concurrency.
A refutation of the almost-universal but wrong claim that the term “Software Engineering” originated with the 1968 Garmisch-Partenkirchen NATO conference. Gives the correct origin.
Should we teach computer science in primary and secondary schools? To answer this question, Informatics Europe and ACM Europe started a joint task force in 2011. The resulting report is concise and makes strong points, emphasizing in particular the need to distinguish education in informatics from a mere training in digital literacy (the mastery of basic IT tools, the Web etc.). The distinction is often lost on the general public and decision-makers (and we will surely have to emphasize it again and again). The report has been widely publicized and has already had significant impact.
 With Carlo A. Furia, Manuel Oriol, Andrey Tikhomirov and Yi Wei:The Search for the Laws of Automatic Random Testing, in Proceedings of the 28th ACM Symposium on Applied Computing (SAC 2013), Coimbra (Portugal), ACM Press, 2013.
For several years I have been fascinated by the question of whether there exists a kind of natural law for the long-term behavior of automated testing: how does the number of bugs found evolve, and do we reach an asymptote? If there is a law of some kind with wide applicability, it provides a solid answer to the project manager's eternal question: Are we shipping yet?. (By comparing the bug detection rates of the current project to the general law, we can estimate how many bugs remain.) this paper provides a systematic analysis of automated testing in Eiffel, using AutoTest, and other languages, and derives a general law.
“ ” covers development of widely different kinds, subject to different criteria. This article describes a classification into three categories, subject to different concerns, tools and techniques.
The emergence of electronic media has fundamentally changed the model of scientific publication. This article describes the next steps. Elaborates on .
An essay of the importance (even with agile methods) of writing software that is correct by construction.
 With Marco Piccioni and Manuel Oriol: Class Schema Evolution for Persistent Object-Oriented Software: Model, Empirical Study, and Automated Support, in IEEE Transactions in Software Engineering, vol. 39, no. 2, February 2013.
One of the great unsolved issues of object-oriented programming is what to do with objects previously stored (in a file or a database) when the corresponding class description has changed. A basic solution was presented in Object-Oriented Software Construction  but a more complete and sophisticated approach is necessary. This article, based on Marco Piccioni's doctoral work and Manuel Oriol's insights, presents tools and libraries for persistent evolution, backed by an extensive empirical study of how classes actually change in the long term evolution of software projects
A discussion of the role of scientific conferences: past and future, accepted and desirable.
 With Julian Tschannen, Carlo A. Furia and Martin Nordio: Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach, in Tools for Practical Software Verification; International Summer School, LASER 2011, eds. Bertrand Meyer and Martin Nordio , Lecture Notes in Computer Science 7682, Springer, December 2012. On AutoProof see also     and the project page at autoproof.sit.org with a Web interface making it possible to try verification interactively.
As part of our work to develop an environment (EVE, the Eiffel Verification Enviroment) that integrates “Verification As Matter of Course”, we are building a proof system, Autoproof, based on Boogie. This article discusses the issues of handling advanced constructs of a modern language, such as agents (closures) and exceptions.
 (Editor, with Martin Nordio) Tools for Practical Software Verification; International Summer School, LASER 2011, Elba Island, Italy, Revised Tutorial Lectures; Lecture Notes in Computer Science 7682, Springer, December 2012.
Part of Benjamin Morandi's doctoral work with the participation of Sebatian Nanz, the description of tools to analyze the performance of concurrent programs based on the SCOOP model.
 With Scott West and Sebastian Nanz: Demonic Testing of Concurrent Programs, in Proc. of 14th International Conference on Formal Engineering Methods (ICFEM 2012), Kyoto, 12-16 November 2012, Lecture Notes in Computer Science, Springer, 2012.
Based on Scott West's doctoral work with Sebastian Nanz's participation, an approach to testing concurrent programs which creates “demonic” interferences to exercise worst-case scheduling behavior.
Analyzes the relationship between specifications and tests and why individual examples (tests) can never replace a general formula (specification). Informed a number of later publications, such as the discussion of use cases and other scenario-based requirements techniques   and an analysis of ChatGPT answers .
A short article derived from an entry in the Communications of the ACM blog , making fun of some research agencies' obsession with breakthrough research and arguing for the importance of incremental research.
 With Christian Estler, Martin Nordio, Carlo A. Furia, and Johannes Schneider: Agile vs. Structured Distributed Software Development: A Case Study, in 7th International Conference on Global Software Engineering (ICGSE), IEEE Computer Press, 2012 (best paper award).
A review of 66 projects in Europe, Asia and America comparing the results of applying agile versus more traditional techniques.
Presents the Eiffel Information System, providing connections between a program text and associated documents, with important consequences for project evolution and configuration management.
 With Benjamin Morandi and Sebastian Nanz: Can Asynchronous Exceptions Expire?, in Proc. of 5th International Workshop on Exception Handling (WEH 2012), ICSE, Zurich, June 2012, IEEE Computer Press, 2012.
What happens when a component of concurrent system triggers an exception and there is no one left to process it, since the original context is no longer alive or active? Based on Benjamin Morandi's doctoral work, this article examines various solutions meant to enforce the consistency of objects and of the computation.
Using a simple example from everyday life, an illustration of the difficulty of writing meaningful requirements.
 With Marco Trudel, Carlo A. Furia, Martin Nordio and Manuel Oriol: C to O-O Translation: Beyond the Easy Stuff, in Proc. of 19th Working Conference on Reverse Engineering (WCRE'12), eds. Rocco Oliveto and Denys Poshyvanyk, IEEE Computer Society, 2012.
Based on Marco Trudel's doctoral work, presents the description of a thorough C-to-Eiffel translator that goes “beyond the easy stuff” by handling the complete C language with all its tricks. The tool is able to produce O-O equivalents of large, practical C systems such as Vim and libgsl.
The first description of a comprehensive approach, under development, for verifying properties of object-oriented programs, illustrated by the complete proof of correctness of a list reversal algorithm.
The method combines four components: compositional logic, a framework for describing program semantics and proving program properties; negative variables to address the specifics of O-O programming, in particular qualified calls (see ); the alias calculus , which determines whether reference expressions can ever have the same value; and the calculus of object structures, a specification technique for the structures that arise during the execution of an object-oriented program.
 With Alexander Kogtenkov and Anton Akhi: Processors and their collection, in Proceedings of MSEPT 2012 (International COnference on Multicore Software Engineering, Performance and Tools), Prague, May 2012, eds. V. Pankratius and M. Philippsen, Lecture Notes in Computer Science, Springer, 2012.
In concurrent programming, particularly but not exclusively with SCOOP, a new notion arises: processors, mechanisms that can execute sequences of operations and be combined to form a parallel system. If processors are implemented in software, they can be created dynamically and, like objects, can become unreachable, raising a garbage collection problem. For this problem (which as far as we know has not been addressed by earlier literature) we devised a formal model and implemented an algorithm, now integrated in the Eiffel SCOOP implementation. The key observation is that processor collection and object collection are closely connected; it leads to defining the problem as a fixpoint equation, and solving it iteratively. As shown by the benchmarks in the paper, the resulting algorithm is as fast as the standard object collection mechanism, and can even be slightly faster in some cases because it skips some objects belonging to “dead” processors.
Domain Theory, as considered in this article, is the modeling of the subject domain of a program. No program verification for serious programs can proceed without a domain modeling effort. This article explains the concept and its importance. The work on MML , the mathematical library for AutoProof , and the verification of the EiffelBase 2 library  started from the concepts described here.
One of the contributions of the Eiffel language design is the use of a special variable, Result, to denote the result of a function and enforce Structured Programming rules by guaranteeing one-entry, one-exit blocks, without the need for a “return” instruction. This article explains the rationale for the mechanism and its design.
 With Benjamin Morandi and Sebastian Nanz: A formal Reference for SCOOP, in Empirical Software Engineering and Verification (LASER 2008-2010) , eds. Bertrand Meyer and Martin Nordio, Lecture Notes in Computer Science 7007, Springer, February 2012.
 With Yi Wei and Manuel Oriol: Is Coverage a Good Measure of Testing Effectiveness?, in Empirical Software Engineering and Verification (LASER 2008-2010) , eds. Bertrand Meyer and Martin Nordio, Lecture Notes in Computer Science 7007, Springer, February 2012.
To measure the effectiveness of tests, industry almost universally relies on branch coverage (often with the rule of thumb that 80% is good enough to ship). How good a measure is it really. against the only criterion that counts in the end — the number of remaining bugs? Not very good, our experiments with automatic testing, using AutoTest ) suggest. Although coverage correlates well with bugs initially, after a while coverage reaches close to 100%, thanks to AutoTest's algorithms, but AutoTest continues to find bugs for a long time. These results put into question the value of branch coverage as a criterion for test completeness.
 (Editor, with Martin Nordio) Empirical Software Engineering and Verification; International Summer School, LASER 2008-2010, Elba Island, Italy, Revised Tutorial Lectures; Lecture Notes in Computer Science 7007, Springer, February 2012.
Since 2004 our chair has been organizing the yearly LASER summer school on the Elba Island in Italy. Starting with the 2006 school we have been able to publish proceedings in a special LNCS sub-series. This is the second volume (see , , ) for others so far) of proceedings of the annual LASER summer school, which takes place every September on Elba island in Italy. It covers lectures from the 2008, 2009 and 2010 schools on topics of empirical software engineering and software verification. The volume includes two of our own papers: one on testing, assessing the value of branch coverage , and the other on concurrency, providing an operational semantics for SCOOP .
Libraries are better than specialized languages.
 With Stephan van Staden and Cristiano Calgagno: Freefinement, in Proceedings of the 39th Symposium on Principles of Programming Languages (POPL 2012), Philadelphia, 25-27 January 2012, ACM Press, 2012.
This artile is based on Stephan van Staden's doctoral work with the collaboration of Cristiano Calcagno and my role has been small. It describes an algorithm that constructs a sound refinement calculus from a verification system.
 Bertrand Meyer: Software Engineering and the Eiffel Programming Language, interview (also of Annie Meyer) by Charles Severance (text and video), in Computer (IEEE), vol. 45, no. 9, pages 6-8, September 2012.
A detailed interview on the history of Eiffel, Eiffel Software (the company) and the evolution of software engineering.
 With Martin Nordio, H.-Christian Estler, Julian Tschannen, Carlo Ghezzi and Elisabetta Di Nitto: How do Distribution and Time Zones affect Software Development? A Case Study on Communication, in Proceedings of the 6th International Conference on Global Software Engineering (ICGSE), IEEE Computer Press, 2011, pages 176-184.
Part of our ongoing study of distributed software development , , , , , , in particular through our DOSE course at ETH Zurich ,  with its project where students from diverse universities collaborate. Studies the consequence of a distributed mode of development on the quality of the software process.
 With Lucas Serpa Silva, Yi Wei and Manuel Oriol: Evolving the Best Testing Strategies for Contract-Equipped Programs, in APSEC 2011, 18th Asia Pacific Software Engineering Conference, Hanoi, 5-8 December 2011.
Evotec, described in this paper, extends our automatic random testing work (see  and many other testing publications in the present list) with genetic algorithms. The aim is to find, in an evolutionary way, the best testing strategies for contract-equipped programs. The results show that Evotec indeed finds more faults than previous strategies.
 With Yu Pei, Yi Wei, Carlo Furia and Martin Nordio: Code-Based Automatic Program Fixing, in ASE '11: 26th IEEE/ACM International Conference on Automated Software Engineering, Lawrence (Kansas), 6-10 November 2011.
Advances in the development AutoFix method and tool for automatic program correction , taking advantage of the presence of contracts to improve the quality of suggested fixes.
An article on the contributions of John McCarthy, pioneer of Artificial Intelligence, designer of LISP, founder and director of the Artificial Intelligence Laboratory at Stanford (SAIL), luminary of the mathematical theory of computation, co-designer of Algol 60, and one of the founders of programmer verification.
 With Yi Wei, Hannes Roth, Carlo Furia, Yu Pei, Alexander Horton, Michael Steinforder and Martin Nordio: Stateful Testing: Finding More Errors in Code and Contracts, in ASE '11: 26-th IEEE/ACM International Conference on Automated Software Engineering, Lawrence (Kansas), 6-10 November 2011.
“Stateful testing” uses dynamic contract inference to improve the efficiency of random testing. Note that the version of the paper currently available is a draft and will be revised for publication.
The “Gotthard Principle”: software design as iterations from both the abstract side (the intent) and the concrete side (the available mechanisms and APIs), each in the direction of the other, until they meet.
 With Julian Tschannen, Carlo A. Furia and Martin Nordio: Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques, in SEFM 2011, Software Engineering and Formal Methods, Montevideo, 14-18 November 2011, Lecture Notes in Computer Science, Springer Verlag, 2011.
The first published description of EVE, the Eiffel Verification Environment, combining tests, proofs and automatic correction, and more generally integrating all the software developments resulting from our group's work. See more about EVE on its project page. One of the novel aspects of EVE is that it provides a general framework to integrate diverse kinds of verification techniques, both static (proofs, currently using Boogie) and dynamic (tests, using the AutoTest framework).
Discusses the various roles of scientific publications. Part of an ongoing series of reflections on this topic; see e.g.  for a later elaboration.
Chides the IEEE 830-1998 requirements standard about a poorly thought-out example involving tests. See  for a modern replacement to the standard.
 With Sebastian Nanz, Faraz Torshizi and Michela Pedroni: Design of an Empirical Study for Comparing the Usability of Concurrent Programming Languages, in ESEM 2011 (ACM/IEEE International Symposium on Empirical Software Engineering and Measurement), 22-23 September 2011 (best paper award).
(There is a revised and extended journal version: .) An empirical study comparing the ease of learning of two concurrency models, SCOOP and Java threads. Since we are deeply involved in SCOOP, one of the most delicate aspects was to guard against experimenter bias. I discussed the background of this paper and methodological issues of empirical software engineering in a series of blog postings in June 2011.
Discussion of the value of injected faults in testing, in response to some criticisms of the ARTOO paper  by Arcuri and Briand.
 With Julian Tschannen, Carlo A. Furia and Martin Nordio: Verifying Eiffel Programs with Boogie, in Boogie 2011, First International Workshop on Intermediate Verification Languages, Wroclaw, August 2011, Lecture Notes in Computer Science, Springer Verlag, 2011.
As part of the EVE verification environment, we have used the Boogie intermediate language and tools from Microsoft Research as the underliing proof mechanism. This article describes the integration of Boogie and the results achieved.
An essay about the fundamental notion of purity in programming language design and software verification.
On the occasion of the first release of EiffelStudio including a full-fledged implementation of the SCOOP Eiffel concurrency mechanism, presents the key elements of SCOOP. For more detailed presentations, see among others .
One of the most significant practical obstacles in making program proofs practical is the difficulty of helping programmers find the proper contracts. An earlier article , building on , presented some basic techniques for inferring loop invariants. We have significantly progressed since then with our AutoInfer tool, which relies on dynamic analysis through AutoTest . The focus is on inferring complete postconditions, which fully specify the behavior of routines .
AutoInfer is completely automatic; as described in the article, it is able to infer 75% of the complete postconditions for a data structure library.
 With Marco Trudel, Manuel Oriol and Carlo Furia: Automated Translation of Java Source Code to Eiffel, in TOOLS Europe 2011 (Objects, Components, Models, Patterns), 49th International Conference, eds. Judith Bishop and Antonio Vallecillo, Lecture Notes in Computer Science 6705, Springer, June 2011, pages 20-35.
Marco Trudel is investigating and implementing techniques for realistic language translation, handling not only the simple constructs but the tricky ones as well, and supported by formal proofs of correctness.
 Steps Towards a Theory and Calculus of Aliasing, in International Journal of Software and Informatics, special issue (Festschrift in honor of Manfred Broy), Chinese Academy of Sciences, 2011, pages 77-116.
(Revised version of .) In verifying object-oriented programs, and any programs involving references or pointers, one is again and again confronted with the problem of aliasing: two expressions denoting the same object. Researchers have tried various approaches to address the issue, including shape analysis, separation logic and ownership types. The alias calculus developed in this article provides a simple, entirely automatic mechanism to compute all aliases induced by a program. The article contains a link to an implementation that the reader can download and try out. (2012 note: the implementation is now superseded by Alexander Kogtenkov's code integrated into EVE, the Eiffel Verification Environment.)
 With Martin Nordio, Carlo Ghezzi, Elisabetta Di Nitto, Giordano Tamburrelli, Julian Tschannen, Nazareno Aguirre and Vidya Kulkarni: Teaching Software Engineering using Globally Distributed Projects: the DOSE course, in Collaborative Teaching of Globally Distributed Software Development - Community Building Workshop (CTGDSD), Hawaii (at ICSE), May 2011.
A general report about our experience with the DOSE course, which covers issues of Distributed and Outsourced Software Engineering and includes a collaborative project carried out by student groups from three different universities. Altogether a dozen universities participate, in Western and Eastern Europe, the Americas, India and China. This report continues the work initially described in , , , .
 With Ilinca Ciupa, Alexander Pretschner, Manuel Oriol and Andreas Leitner: On the number and nature of faults found by random testing, in Software Testing, Verification and Reliability (Wiley), vol. 21, no. 1, March 2011, pages 3-28.
(Extended journal version of .) From the abstract:
[In comparing] faults found through random testing with those found through manual testing and with those found in field use of the software and recorded in user incident reports [we found that] none of the techniques subsumes any of the others; each brings distinct contributions.
Part of Benjamin Morandi's work on SCOOP, a complete description of the model's semantics. Superseded by .
 With Scott West and Sebastian Nanz: A Modular Scheme for Deadlock Prevention in an Object-Oriented Programming Model, in Proceedings of ICFEM 2010, 12th International Conference on Formal Engineering Methods, Shanghai, 17-19 November 2010, Lecture Notes in Computer Science 6447, Springer, 2010.
An approach to deadlock prevention in SCOOP. For a more recent tack on the same problem see .
Illustrates the notion of Galois connection, central to abstract interpretation in software verification, through the example of (human) language dictionaries.
Reflections on the achievements of Watts Humphrey, a pioneer of software project organization and management, author of the original CMM and of the Personal Software Process.
 With Ganesh Ramanathan, Benjamin Morandi, Scott West and Sebastian Nanz: Deriving Concurrent Control Software from Behavioral Specifications, in Proceedings of IROS 2010 (IEEE/RSJ International Conference on Intelligent Robots and Systems, Taipei, Taiwan, 18-22 October 2010), IEEE, 2010.
Under the impulse of Ganesh Ramanathan, we have built robots and programmed them using the SCOOP concurrency mechanism (see e.g. , , ). Using full-fledged concurrency seems to be a novelty in robotics; it is easy to see why when looking at the complexity of solutions using traditional multithreading techniques. By relying on SCOOP we are able to gain considerable flexibility in programming a hexapod robot, whose motion is modeled after a precise analysis of the corresponding mechanisms in some insects. The core program elements appear in the paper and demonstrate the simplicity and effectiveness of using the SCOOP model for such applications.
IROS is a robotics conference, not our usual kind of publication so far; this was our first submission to a robotics venue, but certainly not the last.
 With Alexander Kogtenkov and Emmanuel Stapf: Avoid a Void: The Eradication of Null Dereferencing, in Reflections on the Work of C.A.R. Hoare, eds. C. B. Jones, A.W. Roscoe and K.R. Wood, Springer, 2010, pages 189-211.
One of the most exciting recent developments of Eiffel is void safety: the static (compile-time) guarantee that no “null pointer dereferencing” (a call x.f where x is null, or “void”) will ever happen at run time. Such events are a major threat to programs written in O-O languages, a Sword of Damocles hanging at every moment. For Eiffel programmers the problem has been completely eradicated thanks to void safety.
While the basic ideas were contained in an ECOOP 2005 paper , going from the science to the final engineering took more than four years. This article discusses the details of the mechanism and its implementation, as well as the difficulties we encountered in getting it right.
 With Nadia Polikarpova and Carlo Furia: Specifying Reusable Components, in Verified Software: Theories, Tools, Experiments (VSTTE ' 10), Edinburgh, UK, 16-19 August 2010, Lecture Notes in Computer Science, Springer Verlag, 2010.
Nadia Polikarpova built and verified, as part of her PhD thesis, a fully specified library of fundamental data structures and algorithms, allowing the production of true “trusted components”  . The specifications use the Mathematical Model Library technique introduced in . The AutoProof verification environment  is able to prove the correctness of the library.
 With Carlo Furia: Inferring Loop Invariants using Postconditions, in Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, eds. Andreas Blass, Nachum Dershowitz and Wolfgang Reisig, Lecture Notes in Computer Science 6300, Springer, August 2010, pages 277-300.
In our work to make program proofs a normal, accepted, ongoing part of software development, we have found that a major obstacle, possibly the major obstacle, is programmers' reluctance to come up with loop invariants. There is a significant literature on invariant inference, but this work is different: we start from the postcondition, of which the loop invariant is typically a weakened version. Carlo Furia's system produces impressive results: it infers the invariants of all the classic algorithms tried so far. We are not yet, however, handling data structures with pointers. Current work is intended to correct this limitation, to extend the tools in various directions and to integrate it in the development environment.
Amazingly, the basic idea came when I was able to retrieve a copy of my IFIP 80 paper , which describes strategies for invariant weakening.
 (Editor, with Martin Nordio, Mathai Joseph and Andrey Terekhov) Software Engineering Approaches For Outsourced and Offshore Development (SEAFOOD 2010), 4th International Conference, Saint Petersburg, Russia, Lecture Notes in Business Information Processing 54, Springer, July 2010.
This fourth edition of the SEAFOOD conference series (see ) was for the first time held in Russia, whose outsourcing successes are less well-known than those of India but no less remarkable.
 With Benjamin Morandi and Sebastian S. Bauer: SCOOP - A contract-based concurrent object-oriented programming model, in Proceedings of LASER summer school on Software Engineering 2007/2008, ed. Peter Müller, Advanced Lectures on Software Engineering, Lecture Notes in Computer Science 6029, Springer, July 2010, pages 41-90.
The yearly LASER summer school, which we organize in September on Elba island off the coast of Tuscany in Italy, started in 2004; since 2007 we have started producing proceedings in a special LNCS sub-series, with chapters contributed by the school's speakers and their collelagues. This chapter is from the first volume, covering 2008 and 2009, was edited by Peter Müller (see ,  and ) for subsequent ones). It is based on my lectures on the SCOOP concurrency model, particularly on developments by Benjamin Morandi and Sebastian Bauer. It currently provides the most up-to-date description of SCOOP (superseding Piotr Nienaltowski's PhD thesis, on which it is based and which remains essential for a detailed understanding, as well as the chapter on concurrency in my own Object-Oriented Software Construction  which describes the rationale).
 With Yi Wei, Yu Pei, Carlo Furia, Lucas Silva, Stefan Buchholz and Andreas Zeller: Automated Fixing of Programs with Contracts, in ISSTA '10: Proceedings of the International Symposium on Software Testing and Analysis, Trento (Italy), 12-16 July 2010, ACM Press, 2010.
A recent development of our work at ETH: beyond automatic testing (see  and other publications on AutoTest), automatic correction of bugs after a failure. Once again the key is the presence of contracts in the code. The idea of automatic corrections may seem far-fetched or even absurd, and this work is only at the preliminary stage, but the first results are very encouraging; AutoFix, the tool, finds good fixes in a significant percentage of cases. It is being developed by Yu Pei and Yi Wei, as part of a more general project where we collaborate with Andreas Zeller's group at the University of Saarbrücken; see also our first joint paper on a related topic .
 With Martin Nordio, Cristiano Calcagno, Peter Müller and Julian Tschannen: Reasoning about Function Objects, in TOOLS EUROPE 2010, Málaga (Spain), 28 June - 2 July 2010, ed. J. Vitek, Lecture Notes in Computer Science, Springer, 2010.
Many imperative languages, in particular object-oriented ones, now offer the possibility of defining objects that represent encapsulated computations: agents in Eiffel , delegates in C#, blocks in Smalltalk, “closures” in some other languages. These mechanisms have long proved elusive for semantics and proofs. In this paper we present a semantics for function objects and show that it can be applied to perform effective proofs.
 With Stephan van Staden and Cristiano Calcagno: Verifying Executable Object-Oriented Specifications with Separation Logic, in ECOOP 2010: 24th European Conference on Object-Oriented Programming, Maribor (Slovenia), 21-25 June 2010, Lecture Notes in Computer Science, Springer, 2010.
Stephan van Staden and Cristiano Calcagno have developed advanced techniques for applying separation logic to proofs of object-oriented programs, complementing an array of other approaches in our effort to make continuous integrated verication a standard part of software development.
A set of slides from my talk at ICSE, describing our experience teaching at ETH discussing general principles of software engineering education.
 With Martin Nordio and Roman Mitin: Advanced Hands-on Training for Distributed and Outsourced Software Engineering, in ICSE 2010: Proceedings of 32th International Conference on Software Engineering, Cape Town, May 2010, IEEE Computer Society Press, 2010.
To support and extend our research on distributed software development we have since 2004 years run the DOSE course (Distributed and Outsourced Software Engineering). We practice what we study: since 2007 the software development project for the course is performed by groups of students involving teams from different universities. Current participating universities are from Switzerland, Italy (Politecnico di Milano), Hungary, Russia, Vietnam and Ukraine. The experience is difficult but rewarding. Our ICSE paper summarizes the results we have observed. For a continuation of this work and more extensive analysis, see 
 With Yi Wei, Serge Gebhardt and Manuel Oriol: Satisfying Test Preconditions through Guided Object Selection, in ICST ' 10: Proceedings of the Third International Conference on Software Testing, Verification and Validation, Paris, April 2010, IEEE Computer Society Press, 2008.
Automatic testing as we practice it through AutoTest (see  and many other references in this list) risks skipping the testing of certain routines entirely if the test generation algorithm never happens to produce inputs that satisfy their preconditions. Yi Wei, as part of his PhD thesis, aided by Serge Gebhardt (who did a master's thesis on the topic), Manuel Oriol and me, developed heuristic algorithms that dramatically reduce the number of such cases.
See comments on revised version .
Discusses equality, and whether it should always reflexive, using the example of floating-point numbers and NaN (Not a Number).
Presents powerful iteration mechanisms for Eiffel, then new.
A subsequent blog article (see the second link( gives examples.
A short article showing on an actual example how writing simple contracts immediately uncovers a bug that might otherwise remain undetected, or would be hard to isolate.
 With Michela Pedroni: Object-Oriented Modeling of Object-Oriented Concepts, in ISSEP 2010, Fourth International Conference on Informatics in Secondary Schools, Zurich, January 2010, eds. J. Hromkovic, R. Královic, J. Vahrenhold, Lecture Notes in Computer Science 5941, Springer, 2010.
As part of her PhD thesis Michela Pedroni developed the TrucStudio environment, which we call a “PDE”: a pedagogical development environment, similar to an IDE but devoted to building courses and curricula not programs. With TrucStudio you graphically manipulate visual entities that represent courses, lectures, topics, notions, “trucs” and relations (the “requires” relation, for example studying the notion of sinus requires having studied the notion of triangle, and the “specializes” relation). The approach is based on the concept of Truc .
We have not been successful at publishing this paper (we tried SIGCSE and ITICSE in vain). I think is a pity because the results, while not earth-shattering, provide important information to anyone teaching programming. For many years we systematically polled our students, at the beginning of the their first programming course (see ), about their prior knowledge. The results highlight how difficult it is to teach introductory programming today with such a diversity of initial student backgrounds. A chemistry professor can — I imagine — make reasonable assumptions about what his students know and don't know. Not so for us: the variety of experiences is staggering. The article gives a detailed picture based on the evaluation of hundreds of students over the years. It is currently a technical report; we continue to refine our study and hope eventually to publish it more broadly.
 With Valentin Dallmeier and Andreas Zeller: Generating Fixes from Object Behavior Anomalies, in ASE 2009: Proceedings of 24th IEEE/ACM International Conference in Automated Software Engineering, Auckland, New Zealand, 16-20 November 2009, IEEE Computer Society Press, 2009, pages 550-554.
A first step towards the AutoFix tool, which automatically proposes corrections (fixes) after a program failure. See  for more details.
 With Marco Piccioni, Manuel Oriol and Teseo Schneider: An IDE-based, Integrated Solution to Schema Evolution of Object-Oriented Systems, in ASE 2009: Proceedings of 24th IEEE/ACM International Conference in Automated Software Engineering, Auckland, New Zealand, 16-20 November 2009, IEEE Computer Society Press, 2009, pages 650-654.
One of the most difficult unsolved problems of object technology and database technology is what to do with existing objects, stored in a file or database, when the software evolves and they no longer match the latest corresponding class declarations. A basic approach was described in the second edition of Object-Oriented Software Construction, second edition  and is implemented, but it is just a first step. As part of his PhD work Marco Piccioni is developing, in collaboration with Manuel Oriol from the University of York and me, an advanced set of techniques and tools for schema evolution (as the problem is called). The particular advance reported in this ASE paper, integrating a student project by Teseo Schneider, is a solution based on IDE support rather than just the language or libraries.
A journal paper (based on a 2007 conference presentation ) surveying the compendium of techniques and tools that we have developed at ETH and Eiffel Software (the coauthors come from both organizations) in recent years for automatic testing, now fully integrated under the general name “AutoTest” in the EiffelStudio environment. “Automatic” testing in AutoTest is truly automatic: you provide a set of classes and let AutoTest exercise them until it finds bugs. You do not have to provide test cases; the magic come from built-in contracts in the Eiffel code. In addition to this test generation feature of AutoTest, there is also a test extraction mechanism: after an execution failure AutoTest will, on option, automatically create a reproducible test case which becomes part of the regression test suite. These techniques, in my experience, radically improve the practice of testing.
Makes a point that I believe to be important: when we have a software disaster, instead of just reporting it and then forgetting about it, we should force the responsible party to launch an investigation and publish the results. This is how airline travel became safe, and is also how software engineering can improve. I cam back to theis theme; see the second and third links for follow-up articles (29 November 2009, 24 May 2010).
One of the most ambitious research projects in our Chair is the development of a general framework for concurrent computation, SCOOP. It is widely accepted that concurrent programming is hard and will remain hard, but we disagree. More precisely it is OK that our work of building the framework should be tough, but that is to make concurrent programming for programmers already practicing object-oriented programming. This premise is, in my opinion, required to tame the concurrency beast and is the hypothesis behind SCOOP: if you can write an object-oriented program, you can write a concurrent object-oriented program at little extra learning effort. Piotr Nienaltowski's ETH thesis, defended was a major constribution to SCOOP and took the model to a new level, improving many aspects of the previous version (described in a chapter of ) and establishing a far more solid basis for the model.
The development of SCOOP also benefited from several years of collaboration with Jonathan Ostroff from York University (in Canada), especially on developing the proper theoretical models. This paper presents a detailed model for SCOOP, showing in particular how paying attention to contracts fundamentally determines how to handle concurrent computations.
An introductory programming text using novel techniques for teaching programming: objects and contracts from the start (and inheritance, and genericity, and agents, and all the modern techniques that make life worth living); use of contracts throughout; emphasis on a “light” formal approach; reliance on reuse of existing components; attractive examples, based on the Traffic graphical simulation library (150,000 lines of code) developed specially for this purpose; “Inverted curriculum” approach     ;in-depth treatment of recursion and other advanced topics, including an introduction to lambda calculus. The book is based on seven years of teaching the Introductory Programming course at ETH. Springer did an outstanding job of printing the book in four colors; it has hundreds of illustrations, including numerous photographs of famous computer scientists from my photo gallery.
This is the text whereby Ivar Jacobson and I launched the Semat initiative, Software Engineering Method and Theory, a project to re-found software engineering on the basis of sound theory. The initial leadership consisted of Ivar, Richard Soley and me. Today Ivar Jacobson leads the project.
 With Nadia Polikarpova and Ilinca Ciupa: A Comparative Study of Programmer-Written and Automatically Inferred Contracts, in ISSTA 2009: International Symposium on Software Testing and Analysis, Chicago, July 2009.
Michael Ernst's Daikon, and other tools developed in recent years, have shown the possibility of inferring loop invariants automatically from implementations. Daikon has been applied to languages like C and Java, which have no contract mechanism. As far as I know, there had been no attempt to apply them to a language with a built-in contract mechanism (well, here the “as far as I know” part is not necessary, since there is no such language in common use other than Eiffel), or to compare the results with the kind of contracts that programmers will actually write if they have the opportunity.
As part of her master's thesis — done at ITMO in Saint Petersburg, but supervised by Ilinca Ciupa and me at ETH — Nadia Polikarpova produced an Eiffel interface for Daikon. The result makes it possible to compare the kind of contracts that contract-conscious programmers write and that an inference tool can produce. Read the article to know who — people, computers — is good at what!
 With Gerald D. Everett: Point/CounterPoint: Test Principles, discussion about the article “Seven Principles of Software Testing” , in IEEE Software, vol. 26, no. 4, July-August 2009, pages 62-66.
IEEE Software has a “Point/Counterpoint” department for debates on articles. Robert Glass, the editor, offered it as a space for discussion when Mr. Everett complained about some of my “Seven principles of software testing” . The format is well thought out: point (by Mr. Everett in that case), response, counter-response, counter-counter-response, with strict limits on size. As to who is right in this case, you should judge.
 (Editor, with Olly Gotel and Mathai Joseph) Software Engineering Approaches For Outsourced and Offshore Development (SEAFOOD 2009), 3rd International Conference, ETH Zurich, July 2-3, 2009, Lecture Notes in Business Information Processing 35, Springer, July 2009
Proceedings of third SEAFOOD conference; see notes on the first one .
 With Martin Nordio, Cristiano Calcagno and Peter Müller: A Sound and Complete Program Logic for Eiffel, in Proceedings of TOOLS 2009 (Technology of Object-Oriented Languages and Systems), Zurich, June-July 2009, eds. M. Oriol and B. Meyer, Springer LNBIP 33 , June 2009.
A semantics for the Eiffel language, partly a byproduct of Martin Nordio's PhD work on proof-transforming compilation (see also ). One of the distinctive features of this effort is that it did not shy away from the most advanced and hard to model parts of the language.
 With Martin Nordio, Roman Mitin, Carlo Ghezzi, Elisabetta Di Nitto and Giordano Tamburelli: The Role of Contracts in Distributed Development, in Proceedings of SEAFOOD 2009 (Software Engineering Advances For Offshore and Outsourced Development), Zurich, June-July 2009, Lecture Notes in Business Information Processing 35, Springer Verlag, 2009 .
As noted in several other entries (see e.g.   ) we are actively working on distributed software engineering, in particular through our regular Distributed and Outsourced Software Engineering course (DOSE) involving a multi-site collaborate project for students. The first time around, in 2007, a number of projects did not complete, largely as a result of critical misunderstandings between groups. Starting in 2008, we became stricter in forcing students to document their interfaces through contracts; the result was a spectacular improvement in success rates. This article describes the issues and provides several concrete examples of where contracts made the difference between success and failure.
 (Editor, with Manuel Oriol) Objects, Components, Models and Patterns: 47th international TOOLS conference, Zurich, Switzerland, June/July 2009, Lecture Notes in Business Information Processing 33, Springer, June 2008.
2009 TOOLS conference proceedings, in LNBIP. See  for a general note about the conference series.
 (Editor, with Kay Berkling, Mathai Joseph and Martin Nordio) Software Engineering Approaches For Outsourced and Offshore Development (SEAFOOD), ETH Zurich, July 2-3, 2008, revised papers, Lecture Notes in Business Information Processing 16, Springer, May 2009.
Proceedings of second SEAFOOD conference; see notes on the first one .
As part of a study performed for Informatics Europe, we defined criteria that should be applied when evaluating the quality of research and especially of researchers in the area of computer science (informatics, IT etc.).  is the full Informatics Europe report; this Communications of the ACM is a shorter version.
We dispel an number of myths and show — from many other people's studies — how appallingly inadequate the ISI Web of Science is for computer science. The article has been widely quoted and we have had many statements of thanks from computer scientists in many countries, whom it has helped to convince their governing and evaluating bodies to use reasonable, scientifically sound criteria to evaluate computer science work.
This is the full version, with bibliography, of our analysis of which criteria are appropriate, and which not, in evaluating computer science research and researchers. See the comments on the Communications of the ACM version .
Federico Biancuzzi and Shane Warden interviewed, over the course of several years, the developers of almost all major programming languages. The result is a set of informal but remarkably detailed presentations which taught me a lot, when the book came out, about other people's languages. They interviewed me at length about Eiffel; the resulting chapter is probably the most detailed reference in existence about the background for Eiffel and the circumstances of its creation and development.
Functional programming is experiencing a new popularity, but strangely many people seem to misunderstand the limitations of functional languages for building serious industrial software. This article assesses the functional and object-oriented paradigms against objectives of modularity, extendibility and reusability. The result demonstrates (at least I think it does, read the article to see if you agree) that the object-oriented paradigm is vastly superior — especially since modern O-O languages other than Java have integrated the most powerful contributions of functional languages.
 With Ilinca Ciupa, Manuel Oriol and Alexander Pretschner: Finding Faults: Manual Testing vs. Random+ Testing vs. User Reports, in ISSRE '08, Proceedings of the 19th IEEE International Symposium on Software Reliability Engineering, Redmond, November 2008.
We compared the relative effectiveness of automated testing with AutoTest (see e.g. , manual testing, and bugs actually reported by users in the field. The analysis is that none of them subsumes the others; in particular, automatic and manual testing complement each other. See also  and .
 Design and Code Reviews in the Age of the Internet, in Communications of the ACM, vol. 51, no. 9, September 2008, pages 66-71. (Journal version of SEAFOOD 2008 paper .)
In recent years I have extensively practiced distributed software engineering, that is to say, development by teams that are geographically scattered. This experience has influenced our teaching  , , but the initial impetus was in an industrial setting, at Eiffel Software. One of the techniques that we have found essential for successful distributed software development is a modern revision of the venerable software engineering technique of code reviews, profoundly transformed to take advantage of today's technology and to be useful to distributed teams. We now apply the principles and setup described in the article not only to industrial development but also to our courses and to the production of our research software, whether distributed or local.
 (Editor, with Jerzy R. Nawrocki and Bartosz Walter) Balancing Agility and Formalism in Software Engineering, CEE-SET 2007, Second IFIP TC2 Central and East European Conference on Software Engineering Techniques, October 10-12, 2007, Poznán, Poland, revised selected papers, Lecture Notes in Computer Science 5082, Springer, 2008.
CEE-SET evolved from a purely Polish event to a conference showcasing software engineering advances in the entire Central and Eastern EUropean region. Jerzy Nawrocki invited me to participate in this transformation and I am happy to be associated with the conference series.
A short note describing general principles of testing and dispelling some commonly held misconceptions. It triggered a discussion published in IEEE Software .
 (Editor, with Jim Woodcock) VSTTE: Verified Software: Theories, Tools, Experiments, ETH Zurich, 10-13 October 2005, revised papers and transcripts, Lecture Notes in Computer Science 4171, Springer, 2008.
VSTTE 2005, the first in the VSTTE series, was the launching event of the Software Verification Grand Challenge initiatied by Tony Hoare. The proceedings provide a fascinating snapshot of the state of the art on software verification, and perspectives on new research. They include not only papers but also a transcript of the discussions at the conference.
 Design and Code Reviews in the Age of the Internet , in Proceedings of SEAFOOD 2008 (Software Engineering Advances For Offshore and Outsourced Development, eds. K. Berkling, M. Joseph, M. Nordio and B. Meyer, Springer LNBIP 16, 2009 . ( is the journal version.)
See comments on the Communications of the ACM version .
 Eiffel as a Framework for Verification, in VSTTE 2005 (Verified Software: Tools, Theories, Experiments), eds. B. Meyer and J. Woodcock, Lecture Notes in Computer Science 4171, Springer, 2008 ().
A short contribution to VSTTE describing Eiffel verification work.
 With Martin Nordio and Peter Müller: Proof-Transforming Compilation of Eiffel Programs, in Proceedings of TOOLS EUROPE 2008, Zurich, 30-June-4 July 2008, eds. R. Paige and B. Meyer, Lecture Notes in Business Information Processing 11, Springer, 2008 (), pages 316-335.
Based on Martin Nordio's PhD thesis, this paper expands on the idea of Proof-Carrying Code originally introduced by Necula and Lee, applying it to proofs of full functional correctness rather than just security properties. It shows how to take a proof-equipped program and translate everything, program and proof, all the way down to bytecode.
 (Editor, with Richard Paige) Objects, Components, Models and Patterns: 46th international TOOLS conference, Zurich, Switzerland, June/July 2008, Lecture Notes in Business Information Processing 11, Springer, June 2008.
2008 TOOLS conference proceedings, in LNBIP. See  for a general note about the conference series.
 With Ilinca Ciupa, Andreas Leitner and Manuel Oriol: ARTOO: Adaptive Random Testing for Object-Oriented Software, in ICSE 2008: Proceedings of 30th International Conference on Software Engineering, Leipzig, 10-18 May 2008, IEEE Computer Society Press, 2008.
 With Ilinca Ciupa, Alexander Pretschner, Andreas Leitner and Manuel Oriol: On the Predictability of Random Tests for Object-Oriented Software, in ICST'08: Proceedings of IEEE International Conference on Software Testing, Verification and Validation 2008, Lillehammer (Norway), April 2008, IEEE Computer Society Press, 2008 (best paper award).
 With Michela Pedroni, Manuel Oriol and Lukas Angerer: Automatic Extraction of Notions from Course Material, in Proceedings of SIGCSE 2008 (39th Technical Symposium on Computer Science Education), Portland (Oregon), 12-15 March 2008, ACM SIGCSE Bulletin, vol. 40, no. 1, ACM Press, 2008, pages 251-255.
Part of our work on modeling courses, curricula and other pedagocical concepts through trucs  and the TrucStudio environment . As part of her PhD work and a project by Lukas Angerer, in collaboration with Manuel Oriol, Michela Pedroni developed techniques for analyzing course materials — lecture notes, slides ... — and automatically recognizing pedagogical concepts.
 With Marie-Hélène Nienaltowski and Michela Pedroni: Compiler Error Messages: What Can Help Novices?, in Proceedings of SIGCSE 2008 (39th Technical Symposium on Computer Science Education), Portland (Oregon), Texas, 12-15 March 2008, ACM SIGCSE Bulletin, vol. 40, no. 1, ACM Press, 2008, pages 168-172.
Part of our experimental research on programming education. Marie-Helene Nienaltowski (as part of her PhD at the University of London, in collaboration with our group) and Michela Pedroni studied the reaction of beginning students to error messages of various kinds, to find out which error reporting styles work best as feedback for novices. See also .
 With Marco Piccioni: The Allure and Risks of a Deployable Software Engineering Project: Experiences with Both Local and Distributed Development, in Proceedings of IEEE Conference on Software Engineering & Training (CSEE&T), Charleston (South Carolina), 14-17 April 2008, ed. H. Saiedian, pages 3-16.
 With Till Bay and Michela Pedroni: By students, for students: a production-quality multimedia library and its application to game-based teaching, in JOT (Journal of Object Technology), vol. 7, no. 1, pages 147-159, January 2008.
The EiffelMedia library started by Till Bay and Michela Pedroni gave rise, over the years, to a large number of student developments at ETH, over many years, covering many aspects of multimedia. This article draws the pedagogical lessons.
I was invited to write an article comparing the state of French research to the situation in other countries. The article triggered some approval but also many negative reactions. I believe the observations are essentially still applicable and would hope that the system reforms itself in the ways I suggested.
 With Andreas Leitner, Manuel Oriol, Ilinca Ciupa and Andreas Zeller: Efficient Unit Test Case Minimization, in ASE'07: 22nd IEEE/ACM International Conference on Automated Software Engineering, Atlanta (Georgia), November 2007.
This work grew out of Andreas Leitner's thesis, and benefitted from the collaboration of Manuel Oriol and Ilinca Ciupa at ETH as well as Andreas Zeller in Saarbrücken. The need for minimization is a consequence of adopting an automatic, and hence random, approach to testing: sometimes a test case will hit a failure, revealing a fault (bug), only after taking many detours. If you want — as you should — to make the test part of your regression test suite, you will need to find another test case that reveals the same failure but in a much shorter time, avoiding all the detours. The techniques developed by Andreas Leitner, based in part on Zeller's work on delta debugging, are in theory neither complete (they could fail in individual cases) nor sound (they are not guaranteed to reproduce the failure); in practice, however, they produce excellent results. Minimization techniques are now a standard part of AutoTest .
 With Marco Piccioni and Manuel Oriol: IDE-integrated Support for Schema Evolution in Object-Oriented Applications, in Workshop on Reflection, AOP and Meta-Data for SOftware Evolution (RAM-SE 07), 2007.
This workshop paper was our first ETH publication on schema evolution. It served as a first step towards the ASE paper ; see the comments there.
 (Editor, with Mathai Joseph) Software Engineering Approaches For Outsourced and Offshore Development (SEAFOOD), ETH Zurich, February 5-6, 2007, revised papers, Lecture Notes in Computer Science 4716, Springer, October 2007.
The SEAFOOD conference series, started in 2007 with Mathai Joseph from Tata Consulting Services, addresses a fundamental aspect of today's software development scene: distributed development, in particular through outsourcing. The conferences have had the benefit of contributions by authors from many different countries and organizations, including some seldom heard in software engineering conferences.
 (Editor, with Jean Bézivin) Objects, Components, Models and Patterns: 45th international TOOLS conference, Zurich, Switzerland, 24-28 June 2007, Special issue of theJOT (Journal of Object Technology), Vol. 6, no. 9, October 2007.
2007 TOOLS conference proceedings, published in JOT. See  for a general note about the conference series.
 With Andreas Leitner, Ilinca Ciupa, Manuel Oriol and Arno Fiva: Contract-Driven Development = Test Driven Development - Writing Test Cases, in ESEC/FSE'07: European Software Engineering Conference and ACM SIGSOFT Symposium on Foundations of Software Engineering, Dubrovnik (Croatia), September 2007.
Test-Driven Development (TDD) promotes the excellent idea of testing software continuously. Using manually generated test cases as specifications is, however, not sufficient. A general specification is always superior to an individual test case.
Starting from this observation, Andreas Leitner proposed a development process, which he called Contract-Driven Development (CDD). CDD retains the best of TDD but derives tests from contracts (rather than pretending a set of tests is a specification). With CDD you will run an program element before it has had an implementation (in TDD style), with the explicit goal of breaking it and deriving a useful test case, to be replayed in subsequent regression testing. The principal originality of the supporting tool is the mechanism for constructing test cases automatically from execution failures. This facility is now present in the production version of EiffelStudio (see eiffel.com), as the “test extraction” component of the built-in AutoTest framework.
This ESEC/FSE paper describes the core concepts and their first experimental implementation.
 With Lisa (Ling) Liu and Bernd Schoeller: Using Contracts and Boolean Queries to Improve the Quality of Automated Test Generation, in TAP: Tests And Proofs (), ETH Zurich, February 12-13, 2007, eds. B. Meyer and Y. Gurevich, Lecture Notes in Computer Science 4454, Springer, August 2007, pages 114-130.
Since program tests cannot be exhaustive, the central problem of software testing is to find representative partitions of the state set; a partition is representative if a test exercise elements from all the partition's state sets has a good chance of catching faults. To obtain partitions, we need to abstract the state (as also happens in model checking). The conjecture of this paper is that in object-oriented programming a good abstraction criterion is to partition the state according to the values of the boolean queries of a class.
Indeed in well-designed object-oriented software important information about a class is provided by boolean-valued queries (attributes or functions) that characterize alternative possibilities. A list is empty or not, modifiable or not; a bank account is overdraft or not, insured or not, interest-bearing or not; and so on.
This article introduces a notion of boolean-value coverage and describe the results of experiments suggesting that maximizing this criterion significantly improves the fault-detection effectivness of automatically generated test suites.
 (Editor, with Yuri Gurevich) TAP: Tests And Proofs, First International Conference, ETH Zurich, February 12-13, 2007, revised papers, Lecture Notes in Computer Science 4454, Springer, August 2007.
The proceedings of the first TAP conference, now a yearly event held in conjunction with TOOLS. TAP was created to explore the convergence of two software verification approaches, tests and proofs, which are still often the provinces of different communities but have much to bring to each other.
 With Ilinca Ciupa, Andreas Leitner and Manuel Oriol: Experimental Assessment of Random Testing for Object-Oriented Software, in ISSTA'07: International Symposium on Software Testing and Analysis, London, July 2007.
For a long time, random testing was dismissed as ineffective. Developments of these past few years, including by us as part of the AutoTest project, have shown that contrary to conventional wisdom random testing can be an outstanding technique for finding faults entirely automatically. This assessment paper studies the effectiveness of random testing strategies.
 With Ilinca Ciupa, Lisa (Ling) Liu, Manuel Oriol, Andreas Leitner and Raluca Borca-Muresan: Systematic evaluation of test failure results, in Workshop on Reliability Analysis of System Failure Data (RAF 2007), Cambridge (UK), 1-2 March 2007.
A short workshop position paper on principles of evaluating testing strategies. For some applications of these principles see .
 With Andreas Leitner, Ilinca Ciupa and Mark Howard: Reconciling Manual and Automated Testing: the AutoTest Experience, in 40th Hawaii International Conference on System Sciences, Hawaii, January 2007.
Describes the early stage of the AutoTest tool for automatic testing. For an update see e.g. .
 With Ilinca Ciupa, Andreas Leitner and Lisa (Ling) Liu: Automatic testing of object-oriented software, in SOFSEM 2007 (Current Trends in Theory and Practice of Computer Science), January 20-26, 2007, ed. Jan van Leeuwen, Lecture Notes in Computer Science, Springer, 2007.
A conference presentation of our automatic testing framework, AutoTest. The 2009 journal version  is more complete and up to date.
Jean Ichbiah is known in particular for his design of Ada. In the later part of his career he had a successful commercial venture in an area unrelated to programming language design. I was privileged to know him from early on. We had many discussions over the years on software topics; we often had different views but I learned tremendously from him.
Ichbiah died far too young. I wrote this text to collect my thoughts on this uniquely influential figure in the history of our field.
 Dependable Software, in Dependable Systems: Software, Computing, Networks , eds. J Kohlas, B. Meyer, A. Schiper, Lecture Notes in Computer Science, Springer, September 2006.
This article sounds pretty silly to me now. Still, for the sake of openness I am leaving the link.
The final product of the DICS project (Dependable Information and Communication Systems) funded by the Hasler foundation. A number of papers present various aspects of software dependability; one of them is a general survey of reliability techniques .
 With Marie-Hélène Ng Cheong Vee (Marie-Hélène Nienaltowski) and Keith L. Mannock: Empirical study of novice error paths, Proceedings of workshop on educational data mining at the 8th interna-tional conference on intelligent tutoring systems (ITS 2006), 2006, pages 13-20.
What kind of errors do novice programmers make, and how can we benefit from this knowledge to improve our teaching of programming? See also .
Are design patterns fundamentally different from software components? This is indeed the view in the design pattern literature. In that view, a pattern cannot be reused off the shelf: it has to be programmed and adapted anew for every application that uses it. This approach is disappointing for anyone interested in reusability as promoted by object technology: a truly reusable solution should be reusable as it is, in black box style.
With Karine Arnout we investigated whether we could actually go beyond this accepted view of design patterns, and turn the standard patterns (to start with, those in the “Gang of Four” book) into a library of reusable components. Her PhD thesis (2006) shows that a large part of these patterns can indeed be wrapped as ready-to-use components; the twist is that you need advanced language features, such as Eiffel's agents (O-O closures ), multiple inheritance, constrained genericity, and contracts to keep everything under control.
This IEEE Computer article shows a successful componentization, applied to one of the most delicate patterns: Visitor. Companion articles   presents the cases of the Observer and Factory patterns.
 With Ilinca Ciupa, Andreas Leitner and Manuel Oriol: Object distance and its application to adaptive random testing of object-oriented programs, in Proceedings of the 1st international workshop on Random testing, ACM, July 2007, pages 55-63.
This ICSE paper is part of our work around automatic testing and the AutoTest tool (surveyed in ). It introduces in particular the notion of object distance, developed by Ilinca Ciupa as part of her PhD thesis; the goal is to generalize adaptive random testing (a technique devised by T.Y. Chen) from basic values to objects. With this measure, the distance between two objects involves their basic fields, their types, and, recursively, the distance between the objects to which they contain references. The concepts were developed further in the ICSE paper on ARTOO .
 With Stephanie Balzer and Patrick Eugster: Can aspects implement contracts?, in RISE 2005 (Rapid Integration of Software Engineering techniques), Second International Workshop, Heraklion, Grece, September 8-9 2005, eds. Nicolas Guelfi and Anthony Savidis, Lecture Notes in Computer Science 3943, Springer, 2006, pages 145-157.
The aspect-oriented literature regularly cites the addition of contracts as one of the examples where aspect-oriented programming can be useful. Well, AOP is an interesting idea, but it needs better examples to convince the world of its usefulness.
Stephanie Balzer wanted to test the claim. In collaboration with Patrick Eugster and me, she tried to find out whether it is possible, in a language that does not natively have Design by Contract mechanisms, to emulate them through aspects.
The answer is a clear no: contracts do not crosscut. Aspects are simply inadequate to represent contracts.
The paper was written too quickly and its form is not ideal; even the code examples are not syntactically correct. I bear the responsibility for not checking it more thoroughly before publication. But the substance is correct and up to date. No one who reads this paper can continue with a straight face to sustain that contracts are an example application of aspects.
A Truc, or Testable, Reusable Unit of Cognition, is a unit of teachable knowledge that can be given a precise description following a standard structure: definition, names, prerequisites, examples, applications, common misconceptions etc. This article presents the notion of Truc and explains the central role it can play in structuring, evaluating and comparing educational efforts and artifacts: courses, textbooks, curricula. The TrucStudio Pedagogical Development Environment  is based on this concept.
A report on the first European Computer Science Summit, which led to the formation of Informatics Europe.
 With Bernd Schoeller and Tobias Widmer: Making Specifications Complete Through Models, in Architecting Systems with Trustworthy Components, eds. Ralf Reussner, Judith Stafford and Clemens Szyperski, Lecture Notes in Computer Science, Springer, 2006.
The contracts that programmers write by default are partial. For example it is easy to specify that a push (x) in STACK class increases the count of elements by one and results in x being the new top, but harder to state the equally important property that other elements of the stack are still present and still at their original positions.
The technique that this article describes relies on mathematical models to express the full semantics of classes. The basic idea is to associate with every class, such as STACK, a mathematical model which defines that semantics. In this example the model can be a sequence. Then all operations are specified in terms of the model. The old contracts, for example the postconditions count = old count + 1, are now theorems deduced from these more complete properties.
Since everything should be in the software (“Single Product Principle”), the model classes themselves are written in Eiffel, using a restricted, purely functional subset of the language. The corresponding library is called MML (Mathematical Model Library) and includes concepts such as sets, queues and relations.
Since this paper was published we have continued to develop the approach and have applied it to the full specification and verification of a practical library of fundamental data structures; see .
While there had been many discussions of the political and economic aspects of software outsourcing, this article was the first (to my knowledge) to discuss the technical consequences of this massive phenomenon. The article takes a software engineering perspective of outsourcing. I decided to write it when I saw that the list of topics in the Call for Papers of the 2006 International Conference on Software Engineering — held, of all places, in Shanghai — did not even include anything related to outsourcing or distributed development. Our group at ETH has been actively working on distributed and outsourced software engineering — DOSE, the current name of the course that we have been teaching since 2003 with Peter Kolb (originally Software Engineering for Outsourcing). Several publications have followed this IEEE Computer paper, on research and education aspects of distributed development; see in particular , , , . The SEAFOOD conference series (Software Engineering Advances For Outsourced and Offshore Development)     also followed from this article.
 Attached Types and their Application to Three Open Problems of Object-Oriented Programming, in ECOOP 2005 (Proceedings of European Conference on Object-Oriented Programming, Edinburgh, 25-29 July 2005), ed. Andrew Black, Lecture Notes in Computer Science 3586, Springer, 2005, pages 1-32.
The basic ideas of the mechanism that made Eiffel void-safe: immune to “null pointer errors” that plague most other languages. This paper was presented at ECOOP as a keynote and describes the initial steps; a more recent article  presents the final version of the mechanism.
 The Dependent Delegate Dilemma, in Engineering Theories of Software Intensive Systems, Proceedings of the NATO Advanced Study Institute on Engineering Theories of Software Intensive Systems, Marktoberdorf, Germany, 3 to 15 August 2004, eds. Manfred Broy, J Gruenbauer, David Harel and C.A.R. Hoare, NATO Science Series II: Mathematics, Physics and Chemistry, vol. 195, Springer, June 2005.
(This article is an early step in a line of publications on the semantics of class invariants.  from 2023 is the current final version, superseding all of them.) The name “Dependent Delegate Dilemma” describes one of the fundamental open issues in object-oriented programming: the possibility that a call to a feature of a class, which is really a callback indirectly triggered by a routine of that class, finds the object in an inconsistent state — a state not satisfying the class invariant — because the routine has not finished its current execution.
A typical example is a class representing marriageable people, with an invariant that states that if a person is married then the spouse of its spouse is the object itself:
A procedure marry (other) will run into trouble when it tries to set the spouse field of other: the original object does not yet satisfy the invariant at that point.
The article proposes a simple solution: to require that if a callback is possible the feature must satisfy both the object-oriented correctness rule, which includes the invariant, and the classic Hoare rule, which does not.
Other solutions have been proposed, notably language mechanisms for Spec# by Peter Müller and Rustan Leino, but I find this one easier to explain and use. It is not necessarily the last word; in particular the paper does not do a good job of explaining how to apply the rule modularly. We are working on a new paper proposing a more general solution.
 (Editor) ECMA standard: Eiffel Analysis, Design and Programming Language, approved as International Standard 367 by ECMA International, 21 June 2005; revised edition, December 2006, approved by the International Standards Organization as the ISO standard ISO/IEC 25436:2006.
 The Power of Abstraction, Reuse and Simplicity: An Object-Oriented Library for Event-Driven Design, in From Object-Orientation to Formal Methods: Essays in Memory of Ole-Johan Dahl, eds. Olaf Owe, Stein Krogdahl, Tom Lyche, Lecture Notes in Computer Science 2635, Springer, 2004, pages 236-271.
This paper is a general discussion of event-driven design, starting from the Observer pattern and showing that a much better solution is possible: entirely reusable, based on a single library class, more flexible, type-safe, and handling event arguments properly. The solution fundamentally relies on Eiffel's agents ; it has been implemented as part of a library.
The result is a publish-subscribe scheme that seems impossible to beat in terms of ease of use: to subscribe to an event, use e.g. my_window.left_click.subscribe (agent p), where p is a routine taking two arguments representing the mouse coordinates; to publish an event with coordinates x and y, just use e.g. left_click.publish ([x, y]). Then all the subscribed operations will be triggered on the corresponding objects, with x and y passed as arguments.
The paper builds on this example to develop a general discussion of object-oriented methodology.
I hope that no one having read this paper will want to program an Observer manually ever again.
The solution it presents is also discussed in detail in Touch of Class , a sign of how fast new ideas in software can trickle down from research to first-year teaching.
 V pamiat' Andreia Petrovicha Ershov (in memory of Andrey Petrovich Ershov, in Russian), in Andrey Petrovich Ershov - Ucheny i Chelovek (Ershov, the Scientist and the Man), ed. A.G. Marchuk, Novosibirksk, Press of the Siberian Division of the Russian Academy of Sciences, 2006, pages 316-317.
Andrey Ershov is the founding father of Russian computer science. Knuth credits him with inventing, among other things, hash tables; he also introduced the theory of partial evaluation. He was the only Soviet computer scientist with extensive ties in the West. I was fortunate to meet and befriend him and we had many discussions over the years. This text, in Russian, is an after-dinner speech I gave in Novosibirsk at the 2004 edition of PSI, the bi-annual conference that was established in Ershov's memory.
 with Karine Arnout: Uncovering Hidden Contracts: The .NET example , in Computer (IEEE), vol. 36, no. 11, November 2003, pages 48-55. Short version of .
Even though this is the journal version, the conference version  is more detailed. See the comments on that entry.
 The Outside-In Method of Teaching Introductory Programming, in Perspective of System Informatics, Proceedings of fifth Andrei Ershov Memorial Conference, Akademgorodok, Novosibirsk, 9-12 July 2003, eds. Manfred Broy and Alexandr Zamulin, Lecture Notes in Computer Science 2890, Springer, 2003, pages 66-78.
A presentation of our techniques for teaching introductory programming. It was delivered at a time when I was preparing to teach the first session of the ETH Introductory Programming course, delivered every year since 2003 and resulting in the Touch of Class textbook . The “Outside-In” method is another name for the “inverted curriculum”     .
The PSI conference series is dedicated to the memory of Andrey Ershov, a great Russian computer scientist who died far too early (see ).
 With Karine Arnout: Finding implicit contracts in .NET components, in Formal Methods for Components and Objects, First International Symposium, FMCO 2002, Leiden, The Netherlands, November 2002, Revised Lectures, eds. Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf and Willem-Paul de Roever, Lecture Notes in Computer Science 2852, Springer, 2003, pages 285-318. Extended version of .
Karine Arnout and I investigated libraries written in languages that do not support contracts, in this case .NET libraries in C#, to see if we could find contracts anyway. In other words: are the contracts that Eiffel programmers write an artifact of using the language, a figment of the Eiffel programmer's imagination, since other programmers don't have them; or are the contracts intrinsically there anyway, missed by those other programmers?
It is a clear conclusion of this paper that the contracts are there: it's not the Eiffel programmers who are deluded, but the non-Eiffel programmers who miss part of the picture. We were able through analysis of the specifications, particularly exception cases, to reconstruct the contracts.
Many people reading this paper and its journal variant in IEEE Computer asked us why we did not go further and try to infer the contracts automatically. That was not the purpose of this work; instead, it was focused on the design methodology question: are contracts conceptually necessary or not? At the time, I thought that contract inference was a bad idea: if you extract contracts from the code, you will document what is there, including the bugs. The purpose of specification is to provide an independent view. (This is the “assertion inference paradox .) Since then, however, Michael Ernst's Daikon tool and other work have shown the value of contract inference, which we now use as a complement to programmer-written contracts. We have studied this complementarity in depth; see e.g. ,  and other papers in preparation.
A presentation of SCOOP with special emphasis on the .NET implementation.
 The Outside-In Method of Teaching Introductory Programming, in OO 2003: 9th IPSJ-SIGSE Symposium on Object-Orientation, Information Processing Society of Japan, ed. Mikio Aoyama, Tokyo, August 2003. (See revised version: .)
 Towards Practical Proofs of Class Correctness, in ZB 2003: Formal Specification and Development in Z and B, Proceedings of 3rd International Conference, Turku, Finland, June 2003, eds. Didier Bert, Jonathan P. Bowen, Steve King and Marina Waldén, Lecture Notes in Computer Science 2651, Springer, 2003, pages 359-387. (with formating and color)
Invited presentation at an Z and B (formal specification) conference. A step in the contiuned development of a basis for proving contract-equipped programs. See also .
 The Grand Challenge of Trusted Components, in ICSE '03: Proceedings of 25th International Conference on Software Engineering, Portland, Oregon, May 2003, IEEE Computer Society Press, 2003, pages 660-667.
This ICSE keynote built on previous discussions of the concept of trusted components  to present a unified blueprint for progress in software engineering. It was given shortly after I started at ETH and has defined the framework for most of our work ever since.
Continuation of .
 View of Software Engineering Challenged, interview (also of Eugene Spafford) by Kathy Kowalenko in The Institute (bulletin of the IEEE, Institute of Electrical and Electronic Engineering), March 2003.
One of the challenges in automated verification of object-oriented programs is to deal with pointers (references). This series of papers is a step along the way. The idea is to use simple, intuitive set-theoretical models.  is the continuation.
Have you learned programming language phonetics? No? If so it is high time to correct this grave deficiency in your education by reading the article.
 A Framework for Proving Contract-Equipped Classes, in Abstract State Machines 2003, Advances in Theory and Practice, 10th International Workshop, Taormina (Italy), March 3-7, 2003, eds. Egon Börger, Angelo Gargantini, Elvinia Riccobene, Springer, 2003, pages 108-125.
Invited presentation at an ASM conference. A step in our continued effort to prove the correctness of object-oriented software, taking advantage on the presence of contracts in the code. Explains in particular how to take advantage of inheritance. See also .
 In memory of Kristen Nygaard and Ole-Johan Dahl, in JOT (Journal of Object Technology), vol. 1, no. 4, pages 7, 14-15, September 2002, also with texts by Ole Lehrmann Madsen and Kristen Nygaard.
I was fortunate to discover Simula 67 — the first object-oriented language — early and to use it extensively over several years and became active in Simula circles (even becoming president of the Association of Simula Users at some point). I had the privilege of getting to know Kristen Nygaard, Simula's co-designer and advocate, quite closely. He was a formidable figure, one of the most impressive scientists I have met; he was in fact not just a scientist but also a successful politician. I was shocked to hear of his premature death — shortly after that of his co-designer, Ole-Johan Dahl, whom I knew less well — and wrote this eulogy to try to summarize my understanding and admiration of their contributions.
In 2002 we started an effort to produce an international standard, which culminated four years later with the ECMA standard and one year after that in the ISO standard . This article was written at the time of the launch of the effort and described its goals and scope.
Describes the implementation of Eiffel on .NET, expanded from  so that it would cover the full language. Explains in particular how multiple inheritance was implemented on top of a framework that natively supports single inheritance only, and how Eiffel achieved full interoperability with other .NET .NET languages such as C# and Visual Basic .NET.
Multi-language programming: how .NET does it, 3-part article in Software Development, May, June and July 2002. Part 1: Polyglot Programming; Part 2: Respecting other object models; Part 3: Interoperability: at what cost, and with whom? Multi-language: HTML, as published: (2 and 3 forthcoming).
What attracted us to the .NET framework — initially as part of Microsoft's “Project 7”, prior to the official release — was its genuine support for multiple languages in a single framework.
This three-part article explains in detail the .NET model for multi-language interoperability, and how to implement a language on .NET so that the resulting programs can interacte freely with components coming from other languages such as C# and Visual Basic .NET.
The article contains in particular a full description of how we implemented Eiffel's multiple inheritance model on top of a framework that only supports single class inheritance.
The idea was to start a series of regular reviews that would examine books in depth and comment on forma as well as substance. This first review showed the way. Unfortunately, I did not find the time to continue the series.
Having overloading in an object-oriented language destroys the simplicity and consitency of the type system. I know this is not a dominant view, but this article explains in detail why in-class (syntactic) overloading is not only useless but harfmul in an O-O context.
Part of the Eiffel column in JOOP .
 .NET is coming, in Computer (IEEE), vol. 34, no. 8, August 2001, pages 92-97. Translation: Russian in Otkrytye Systemy (Open Systems Publications), #11-2001, November 2001. .NET overview as published (PDF);
One of the first introductions to the .NET framework, written from a programmer's perspective.
Published in the IEEE Computer “Object and Component Technology” column .
 EiffelStudio: A Guided Tour, Technical Report TR-EI-68/GT, Interactive Software Engineering Inc., July 2001. Replaces .
 With Tanit Talbi and Emmanuel Stapf: A metric framework for object-oriented development, in TOOLS 39 (Technology of Object-Oriented Languages and Systems, Santa Barbara, USA, 29 July-3 August 2001), Santa Barbara, USA, pages 164-172, 2001.
EiffelStudio offers an extensive set of metric facilities, enabling programmers and project managers to obtain precise quantitative information about the state of a project. The framework is not limited to a predefined collection of metrics but allows users to define new metrics of interest. Tanit Talbi, under the supervision of Emmanuel Stapf, wrote the first version of the metrics framework. This article describes the principles and basic functionalities.
Since then, Yi Wei at ETH has developed the framework further, providing an open-ended query language for obtaining quantitative and qualitative information about a system.
 An Eiffel Tutorial, Technical Report TR-EI-66/TU, Interactive Software Engineering Inc., July 2001. (Adapted, revised and extended from .)
 Software Engineering in the Academy, in Computer (IEEE), vol. 34, no. 5, May 2001, pages 28-35. Translations: Russian in Otkrytye Systemy (Open Systems Publications), #07-08-2001, October 2001; Chinese (Jian Hu). as published (PDF) ; ;
Before I joined, ETH asked me to write a “vision statement” on teaching, presumably because my background was not as a full-time academic. I thought I might just as well reach for a publication of general interest rather than just an internal paper, hence this paper, a broad discussion of the issues and principles of teaching software engineering in a university environment.
All programming languages offer some sort of conversion mechanism between values and variables; for example you can usually use an integer as a real (floating-point) number. Most such conversion mechanisms are, however, ad hoc; they break the consistency of the type system, especially in an object-oriented context; and they are often limited to predefined types, excluding the possibility of conversions for new programmer-defined types.
As part of the work that led to the Eiffel standard  we devised a general conversion mechanism that does not suffer from these deficiencies. It is compatible with the object-oriented paradigm, enjoying a carefully devised relationship with inheritance; it is safe and promotes reliability; it avoids any confusion on the program reader's part as to whether, for example, a given assignment will involve inheritance, conversion, or neither of these mechanisms (the assignment cannot involve both); it is applicable both to predefined types, defined in Eiffel by library classes, and to any programmer-defined class.
The mechanism has been part of Eiffel for many years and is widely used. It is fundamental for example for the fully compatible use of Eiffel on .NET: Eiffel strings and .NET strings are safely and silently converted back and forth.
This paper describes conversion principles and their application to the Eiffel mechanism. It was published as part of the Eiffel column in JOOP .
A video course, one of the first comprehensive introductions to .NET, taped and published shortly after the appearance of the .NET framework. Includes a discussion of the multi-language support in .NET and its implications for software engineering.
 With Christine Mingins, Raphael Simon and Emmanuel Stapf: Eiffel on the Web: Integrating Eiffel Systems into the Microsoft .NET Framework, MSDN (online article), July 2000. Also in Chinese and Japanese translations. Describes an initial implementation, now obsolete; replaced by . (obsolete). Also: and
Describes the initial implementation of Eiffel on .NET, one of the first (with COBOL) ports of a non-Microsoft compiler to the framework. The solutions retained were temporary: as described in the article Eiffel for .NET (temporarily dubbed “Eiffel#”) supported single inheritance only, but this was soon corrected, thanks to sophisticated techniques sketched in  and ; the language supported on .NET is all of Eiffel, with full interoperability with other .NET languages such as C# and Visual Basic .NET.
How do contracts apply to components other than object-oriented classes? Part of the Software Development column .
 Agents, iteration and introspection, draft book chapter from forthcoming Standard Eiffel , May 2000.
A description of the Eiffel agent mechanism as introduced in  providing function objects (full lambda expressions) in a convenient way, compatible with the rest of the object-oriented paradigm.
Agents are essential for applications such as event-driven design and publish-subscribe, as well as for mathematical computations and many others.
A discussion of the requirements that software components must satisfy to be composable. Part of the Software Development column .
 The Ethics of Free Software, in Software Development, March 2000, Vol. 8, no. 3, pages 32-36. Reprinted in The Unified Process: Transition and Production Phases, eds. Scott W. Ambler and Larry L. Constantine, CMP Books, 2002, pages 194-199.
Free, open-source software has been one of the most important developments in software engineering. I love free software, both as a user and as a producer. But I cannot stand the grandiose self-certifications of sainthood by some of the free software zealots, and their slandering of commercial software developers and more generally anyone who does not entirely agree with them. Free software is not, contrary to what such people would like the world to believe, an ethical choice; it is a business model.
Such is the central point of this article. I researched in some depth the ethical arguments of some of the most outspoken advocates and found some pretty ugly connotations. The article advocates a peaceful coexistence between the open-source and commercial software development communities, on the basis of complementarity and mutual respect. It did not only bring me friends.
A presentation of agent-based programming , adding techniques from functional programming techniques to the object-oriented framework.
Even the best things have an end; this was the last article of the Computer (IEEE) “Object and Component Technology” column . I was given a bit more space than usual and used the opportunity to reflect on the progress object and component technology, its successes, and the remaining challenges.
Software reliability is a difficult goal. Dogmatism does not pay: success requires using many different techniques, developed by different communities and addressing different issues. This article reviews some of the available techniques.
Published in the IEEE Computer “Object and Component Technology” column .
The major extension of Eiffel after the Eiffel 3 step  was the addition of a carefully designed agent mechanism adding the power of function objects, also called closures in other contexts, and providing the full power of lambda expressions. Agents enrich object-oriented programming with many of the attractions of functional languages (see  for a comparison of the functional and O-O approaches from the viewpoint of modular architecture).
Agents are essential for applications such as event-driven design and publish-subscribe, as well as for mathematical computations and many others. Dismissing our initial concerns, they turned out to be entirely compatible with and complementary to the other fundamental object-oriented mechanisms.
This paper, written in collaboration with the people who were most influential in the design of the mechanism, introduced agents. It was published in the Eiffel column in JOOP .
For a more complete description of agents and many examples of their use, see .
Editorial for a special issue on component-based development, which helped convince a large audience of the fundamental role of components in modern software engineering.
From the time of Eiffel 3 (1990, as documented in ) to 1997 the language remained unchanged; then it was time for an important update which included fundamental new concepts such as agents , accompanied by cleanup and simplification of existing parts. The paper describes this important step in the evolution of the language. See  for the principles guiding that evolution.
Initially “object-oriented colum”, my IEEE Computer column  was extended to “Object and Component Technology” in 1999 to acknowledge the growing importance of component-based development and its complementarity with O-O ideas. This particular installment explained the reasons for the change.
Grady Booch, Clemens Szyperski and I had a lot of fun, for about four years, arguing with each other through our alternating shots at writing the object technology column of Software Development. Some of the articles I contributed have their own entries elsewhere in this list.
 Principles of Language Design and Evolution, in Millenial Perspectives in Computer Science (Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare), eds. Jim Davies, Bill Roscoe and Jim Woodcok, Cornerstones of Computing, Palgrave, Basingstoke-New York, 2000, pages 229-246. (the text as intended)
A general reflection about language design, specifically focused on an aspect that few people have discussed: evolving a language after its initial design and while it is already used by a significant community concerned with compatibility.
The paper was presented at the Oxford “retirement” symposium in honor of Tony Hoare (quotes needed since he has continued, at Microsoft, to be as active as ever). The title is an homage to his 1973 Principles of Programming Programminganguage Design POPL paper.
Announces the open-sourcing of the EiffelBase library of fundamental data structures and algorithms, a showcase for careful object-oriented design. Since then the rest of the EiffelStudio environment has also been released under an open-source license.
Part of the Eiffel column in JOOP .
What kind of metrics are appropriate for object-oriented programming?
Published in the IEEE Computer “Object and Component Technology” column .
A fundamental difference exists between two kinds of descriptions: explicit, which describe things by what they are, and implicit, which describe them by what they have. This distinction is not always well understood; in particular it is not because a specification is formal (expressed through mathematics rather than in programming terms) that it is implicit; it can still be constructive, a kind of abstract implementation. Implicit specifications are fundamentally more abstract and general (a point already made in  and ).
Much of the power of object technology is due to the implicitness of its description style, a legacy of its underlying theory, abstract data types. This short column explains the benefits.
Published in the IEEE Computer “Object and Component Technology” column .
Discusses how best to achieve the portability of programs across platforms.
Part of the Eiffel column in JOOP .
Introduced the concept of trusted component. See also .
Can object-oriented techniques be applied to real-time and embedded developments? Th is is still a controversial topic, but the experience reported in this paper (development of an Eiffel-based laser printer system at HP) shows that the technology is ready.
One of a regular series of papers in JOOP, before it officially became the Eiffel column .
An installment of the IEEE Computer “Object and Component Technology” column .
Explains one of the principal roles of object technology and Eiffel in particular: to serve as a wrapping technology for code written in older (legacy) approaches. The object-oriented approach is particularly good at building the higher-level structure of systems; the internals of the modules making up such structures do not all have to be written in an O-O way, especially if the implementations already exist and can be reused. O-O structuring mechanisms such as classes, information hiding, genericity, single and multiple inheritance, deferred classes, all under the protection and documentation of contracts, can play a major role in reengineering legacy code. Eiffel is particularly suited for that purpose, with its ambitious object-oriented model and its sophisticated interface for incorporating external software written in such languages as C and C++.
Part of the Eiffel column in JOOP .
 An Overview of Eiffel, in The Handbook of Programming Languages, Vol. 1, Object-Oriented Languages, ed. Peter H. Salus, Macmillan Technical Publishing, 1998. (See  for updated version.) Revised version (detailed Eiffel tutorial): or
Peter Salus put together a volume on object-oriented languages, with chapters on the major languages, typically written by their designers or people closely involved. I wrote the Eiffel chapter; in later revisions it served as the basis for other tutorials, including introductory material on the ( Eiffel documentation site.
Other chapters in the volume are also interesting. The chapter by Adele Goldberg on Smalltalk has very interesting details &8212; not available elsewehere, except for a PBS documentary of which an excerpt exits on Youtube &8212; on the history of Smalltalk and Parcplace and how she unsuccessfully tried to prevent Steve Jobs from gaining insider access to the technology.
This short paper is not well known, but I think the ideas it introduced are important. It describes a quality-focused software process, incorporating some of what is now known as techniques of agile development, in particular an emphasis on constant iteration and continuous testing.
Published in the IEEE Computer “Object and Component Technology” column .
Jean-Marc Jézéquel pointed out to me the relevance of the Ariane-5 software-induced crash was to discussions of programming methodology, and the deficiencies of the recommendations in the official accident report. We wrote this paper as a result. It shows how fundamental techniques of Design by Contract are to successful reuse, and how their systematic application avoids such software catastrophes.
Published in the IEEE Computer “Object and Component Technology” column .
 Object-Oriented Software Construction, second edition, Prentice Hall, 1296 pages, January 1997. Translations: Spanish (Prentice Hall Latin America), French (Eyrolles), Russian (Russkaia Redaktsia / Internet Universitet, Moscow, 2005), Serbian (CET, Belgrade, 2003), Japanese (IT Architects, 2007).
September 2022: I have been able to reconstruct the book and put it entirely on line for free usage. See the link on the right.
Ever since the Journal of Object-Oriented Programming began publication I had regularly contributed articles, as reflected in this bibliography. In 1997 Richard Wiener, the editor of JOOP, invited me to turn this collaboration into a regular column on Eiffel-related themes. This was the opportunity for many articles that touched on diverse aspects of object-oriented design methodology and its language implications. Methodology, rather than language details, is indeed the focus of the articles, most of which appear under their own entries.
JOOP played a key role in accompanying and supporting the development of object technology. Its original owner sold the business in 2000 and the following year the new publisher, who had promised to continue JOOP, stopped publication. This was such a blow to the community that we decided to take things over and started the successor journal, JOT (Journal of Object Technology), at ETH, with the first issue coming out in May of 2002. Published every other month, plus special issues, JOT is a free-access, open journal, available at jot.fm. Richard Wiener was editor-in-chief of JOT for eight years. Others (including Oscar Nierstrasz then Alfonso Pierantonio) have taken over since 2010.
Ed Yourdon was preparing a special issue of his magazine on the then brand new UML and asked me for a contribution. He told me that what he received was not quite what he expected, but was gracious enough to publish it anyway (and said he was “rolling on his sides with laughter” when he first read it).
The article is a pamphlet and not shy about my views of UML at the time. As to whether I still hold these views today — I have too many friends in the UML community to answer that question. Suffice it to say that when it comes to the UML lecture in our software engineering or software architecture courses, I tend surprisingly to be out of town that week and regrettably have to ask someone else to do it.
How best to teach object technology. Published in the IEEE Computer “Object and Component Technology” column .
This was my first paper on the problem of schema evolution: what to do with objects that have been stored in a file or database when the text of the corresponding classes has changed? It defines the basic concepts, including the fundamental consistency requirement, based on class invariants (see ), and the steps involved involved in handling evolution: detection, notification, correction. The problem and solution were described in more detail in Object-Oriented Software Construction, second edition ; they were implemented thereafter and are included in the EiffelStudio environment. Recent work at ETH   explores more advanced techniques.
Published in the IEEE Computer “Object and Component Technology” column .
Object technology is rightly praised for its ability to “model reality”. This phrase is an oversimplification, however; our O-O programs are models not reality but of other models of some part of the world, “real” or not. The article discusses the complex relationship between the reality and our models of it.
Inheritanc3 is one of the most brilliant contributions of object technology to quality software development. While some authors take a restricted view of inheritance, reserving it for a specific kind of subtyping, this article shows that inheritance is best understood as a rich notion with many different styles of application. Specifically, it proposes a taxonomy of uses of inheritance, with in the end twelve different kinds. Many of them accept multiple inheritance, a technique that has received a bad rap because of some poor language designs, but turns out to be indispensable for successful software architecture.
This paper was part of the IEEE Computer “Object and Component Technology” column . The material was reused in one of the chapters of inheritance in the second edition of Object-Oriented Software Construction .
This invited contribution summarizes some of the key arguments for using Eiffel.
One of a regular series of papers in JOOP, before it officially became the Eiffel column .
Few people deny that reuse is desirable, but it can be hard to achieve. This short article discusses the more advanced contributions of object technology to reuse.
Published in the IEEE Computer “Object and Component Technology” column .
First installment of the IEEE Computer Object-Oriented Column, later renamed later “Components and Object Technology” . Set the tone for the couple dozen articles that followed.
For four years IEEE Computer carried, in most issues, installments of this column on object and component technology;
The column provided a great opportunity to address many different issues in a concise format dictated by the constraints of the publication; many of the ideas were later developed further in longer articles and in books. The articles elicited, in the journal itself, many interesting responses and comments from readers.
Revised version of .
 Static Typing, in OOPSLA 95 (Object-Oriented Programming, Systems, Languages and Applications), Atlanta, 1995. (Appears in the supplementary OOPSLA proceedings, ACM SIGPLAN OOPS Messenger, vol. 6, no. 4, October 1995, pages 20-29. See .)
Keynote presentation at OOPSLA 1995. Analyzes typing issues and solutions for object-oriented languages, including in particular the need for covariance and the problems it raises. A good part of the material also appears, revised and extended, in the chapter on typing of the second edition of Object-Oriented Software Construction .
IEEE Software asked a number of people for their views on the future of software technology.
 On the Role of Methodology: Advice to the Advisors, in Object-Oriented Technology for Database and Software Systems (Montreal, 1995), eds. V. S. Alagar and R. Missaoui (eds.), World Scientific Publishers, Singapore, 1995, pages 1-5.
A set of rules for programming methodologists — meta-methodology if you like. This text was my contribution to the proceedings of a conference to which I had given an invited talk. The organizers were disappointed when they received it: they found it too short; apparently a big proceedings volume was needed to justify the conference to the the sponsoring agency. The reader should judge, but I think that the points made by the article, regardless of length, are important; some of the literature on agile methods (for example) would have been well-advised to apply them. The material was reused and extended in a methodology chapter of the second edition of Object-Oriented Software Construction .
Published several books on Eiffel-related topics, including the Jézéquel-Mingins-Train book on design patterns in Eiffel, the Weedon-Thomas introduction to the language, and the McKim-Mitchell discussion of Design by Contract.
 Object Success: A Manager's Guide to Object-Orientation, its Impact on the Corporation, and its Use for Reengineering the Software Process, Prentice Hall, 1995. Translation: German (Carl Hanser Verlag).
March 2023: I have been able to reconstruct the book. It is now available for free use on the Web, fully hyperlinked. See the URL on the right.
Original version of the Kernel Library standard for Eiffel. The work continues under the auspices of the ECMA Eiffel standard committee (TC49-TG4, see ).
One of a regular series of papers in JOOP, before it officially became the Eiffel column . Discusses issues of programming education.
 ISE Eiffel: The Environment (manual), Technical Report TR-EI-39/IE, Interactive Software Engineering Inc., 1994-2000 (successive editions). Original text derived from .
The manual for EiffelBench, the predecessor of EiffelStudio. Revision of .
Presents a full-fledged method for constructing high-quality libraries of reusable components, building on the principles of , and its application to the design of the EiffelBase libraries as they existed at the time, and their entire specification.
A tool for high-level graphical analysis and design. In application of the seamlessness principles of the Eiffel method the ideas were later incorporated into EiffelStudio, so that one can freely go back and forth between textual and graphical views, the tool ensuring that they remain compatible at all times (by reflecting on each the changes made on the other).
Based on the EiffelBench (now EiffelStudio) environment as it was back then, and as such obsolete, but introduces a number of concepts that should be applied to make an IDE truly object-oriented — that is to say, consistent with the O-O method and language it supports — and that are still relevant.
Manual for a GUI builder associated with the EiffelVision library.
 Systematic Concurrent Object-Oriented Programming, in Communications of the ACM, 36, 9, September 1993, pp. 56-80 (part of special issue .
The world is still waiting for a comprehensive solution to the problem of concurrent programming. SCOOP (Simple, Concurrent Object-Oriented Programming, where the S first stood for “Sequential” and then for “Systematic”) is our proposal. It is still in development; this Communications of the ACM paper, picking up on the initial version , described the basis.
The basic idea of SCOOP is to make concurrent programming easy, by taking full advantage of the benefits of object-oriented programming and contracts. Although some details have changed and the model continues to be improved — see in particular  and  —, this Communications of the ACM article is still a good place to read about the key concepts and the rationale.
This special issue came out of TOOLS conferences and provided a diverse view of state-of-the-art work in concurrent O-O programming. It included the first article on SCOOP .
Discusses how object-oriented principles affect the nature of the development environment (IDE) and can serve as a guide for the user interface and the interaction with the programmer. Based on an early version of the EiffelStudio IDE (then called EiffelBench).
One of a regular series of papers in JOOP, before it officially became the Eiffel column .
 Towards an Object-Oriented Curriculum, in Journal of Object-Oriented Programming, Volume 6, Number 2, May 1993, pages 76-81. (Revised as .)
The first in a series of publications describing a general approach to teaching introductory programming, known as the “inverted curriculum” (a term first used by Bernie Cohen for teaching electrical engineering, in an article that John Potter first brought to my attention).
The basic idea is that we should start with reusable components and teach students first to reuse them through their contracts, then to study them internally, then to extend them, then to build their own. Many later articles developed the concepts further, culminating in the ETH course and the Touch of Class introductory programming textbook .
One of a regular series of papers in JOOP, before it officially became the Eiffel column .
 First Steps with EiffelBench, Technical Report TR-EI-38/IE, Interactive Software Engineering Inc., 1993-1997 (successive editions). Replaced by .
Introduction to this IDE, the predecessor of EiffelStudio.
A comparison between the two languages, contrasting not only individual language features but the design principles behind them.
 Towards an Object-Oriented Curriculum, in TOOLS 11, Technology of Object-Oriented Languages and Systems, Santa Barbara, August 1993, eds. Raimund Ege, Madhu Singh and B. Meyer, Prentice Hall 1993, pages 585-594. (Revised version of .) or
 An Overview of Object-Oriented Technology, in Object-Oriented Applications, eds. B. Meyer and J.-M. Nerson , Prentice Hall, 1993.
General introduction to object-oriented principles and techniques.
A collection of chapters by several authors, describing a number of interesting applications written in Eiffel, with many discussions of issues of object-oriented architecture.
 Design by contract: building bug-free O-O software, in Hotline on Object-Oriented Technology, volume 4, Number 2, December 1992, pages 4-8. Revised version (2000) online at eiffel.com. Translations: German in ComputerWoche, February 1994; Russian in Otkrytye Systemy (Open Systems Journal), vol. 6, no. 32, 1998, pages 34-38; Chinese by Jian Hu.
Survey paper on Design by Contract. Obviously people found it useful since it was reprinted and translated in many different places.
Simula 67 is at the root of all subsequent object-oriented languages and developments. I used Simula extensively and benefitted tremendously from it. On the occasion of its 25-th anniversary, this invited paper reflects on the contributions of Simula.
 Applying “Design by Contract ”, in Computer (IEEE), 25, 10, October 1992, pages 40-51. (Invited paper in special object-oriented issue; slightly revised version of .) Republished in Object-Oriented Systems and Applications, ed. David Rine, IEEE Computer Society Press, 1994.
This was intended to be the first paper on Design by Contract, but it ended up being published long after other descriptions, notably the Design by Contract chapter of Object-Oriented Software Construction  in 1988 and my contribution to the Capri book . I wrote the paper in 1986 and sent it to IEEE Computer in early 87; it languished for more than five years in the refereeing circuit, with three referees saying that it was great and three that it was terrible, and the editor-in-chief not making a decision. Finally in 1992 I was invited to contribute to a special issue on O-O and happily provided the text.
Today (April 2015) it has over 2250 citations on Google Scholar. A good encouragement to persist if you think you have a good idea and the world does not recognize it right away!
 Object-Oriented Software Engineering, instructional video film, Europace (new edition of 1988 program ) and Interactive Software Engineering, September 1992.
 Object-Oriented Design and Programming, 18-hour instructional video film, Europace (training organization for major industrial companies in the European Union), September 1988. Two-hour live follow-up lecture and panel, December 1991.
A reflection on the challenges raised by the successes of object technology.
One of a regular series of papers in JOOP, before it officially became the Eiffel column .
 Eiffel: The Language, Prentice Hall, 1991. Second revised printing, 1992. Translations: French (InterEditions). Third edition in preparation (see ).
Known as “ETL”, this book describes an older version of the language and still serves as a good survey of the concepts, although to know what Eiffel really is today you should consult the ECMA/ISO standard .
ETL tries to be three books in one: introduction; manual; reference. To achieve this goal, it intersperses discussions at various levels of discourse.
The reference part systematically gives three descriptions for every construct: syntax, validity constraints (expressing the static semantics, e.g. type rules) and semantics. It uses a system of “road signs” to make sure the reader always knows the category of every description element.
The description is more precise than the definitions of most other languages. In particular, the 90 or so validity constraints are of the “if and only if” form. For other languages you generally find “only if” rules, telling you what you may not write, which is important but not enough. Take an assignment x := y. You will be told that you must provide a type for y with that of x; somewhere else you read that x may not be a read-only entity (such as a formal argument); yet somewhere else there will be more conditions. But as a programmer I want to know what I may write: I want necessary and sufficient conditions. The Eiffel rules in ETL are of the form “An assignment x := y is valid if and only if it satisfies the following conditions: (1)... (2)... ”. This style is more difficult for the language designer, who must make sure not to forget any case, but they provide a contract to the programmer, who knows that if he satisfies all the given conditions he is entitled to proper processing by the compiler and a guaranteed semantics at execution time.
The BNF variant for syntax is also original; called BNF-E, it requires a single production to define every construct and does not allow nesting (for example, no choice inside an aggregate or repetition). The result is a slightly bigger grammar, but I find it more readable, and more manageable as a language evolves.
Proceedings of a fascinating spring school on object technology organized in Capri in 1988 by Carlo Ghezzi and Dino Mandrioli. Speakers also included Mehdi Jazayeri and Peter Wegner. The first chapter  is a general introduction to Design by Contract.
 The New Culture of Software Development in Advances in Object-Oriented Software Engineering, eds. D. Mandrioli and B. Meyer , Prentice Hall, 1991, pp. 51-64. (Revised version of TOOLS 1 article ; see also the JOOP article .)
A discussion of how object technology affects the very essence of software development. Published as part of our Capri volume .
 Design by Contract, in Advances in Object-Oriented Software Engineering, eds. D. Mandrioli and B. Meyer , Prentice Hall, 1991, pp. 1-50.
A presentation of the principles of library design, buttressed by the experience with EIffelBase and other Eiffel libraries. The book Reusable Software  refines and extends the ideas.
Description of an early version of the SCOOP concurrency model. Introduced many of the key ideas (processors, minimal extension of the object-oriented framework, reinterpretation of preconditions as wait conditions). The next iteration, as described in the 1993 Communications of the ACM paper , is the basis for the current versions of SCOOP. The up-to-date reference is .
A tutorial paper introducing practicing programmers to assertion- and exception-based techniques for building correct software.
September 2022: I have been able to reconstruct the book and put it entirely on line for free usage. See the link on the right
 The New Culture of Software Development, in Journal of Object-Oriented Programming, Volume 3, Number 4, pages 76-81, November-December 1990. (Revised version of TOOLS 89 article ; see also the book chapter version .)
Discusses the effect of an object-oriented mode of development on the fundamental practices of software engineering. Part of a set of successive revisions of the same basic article first presented at TOOLS in 1989.
One of a regular series of papers in JOOP, before it officially became the Eiffel column .
This Prentice Hall series published many important books by excellent authors on diverse aspects of component and object technology.
 Eiffel: An Introduction, in Object-Oriented Programming Systems, Tools and Applications, ed. J.J. Florentin, Chapman & Hall, 1991, pp 149-182. Also appears in New Computing Techniques in Physics Research, eds. D. Perret-Gallix and W. Wojcik, Editions du CNRS, Paris, 1990, pp. 191-208.
A general presentation of Eiffel, in tutorial style, covering the essentials as of 1991.
 The New Culture of Software Development: Reflections on the Practice of Object-Oriented Design, in TOOLS 1 (Technology of Object-Oriented Languages and Systems, Paris, November 1989), SOL, Paris, pages 13-23, 1989. (Revised versions: in JOOP  and as a book chapter .)
The object-oriented method suggests an attractive approach to parsing, superior conceptually (but not performance-wise) to the usual Yacc-style technique. The idea, which we implemented as the EiffelParse library, is to model a grammar as a set of classes, one for each nonterminal. One of the advantages is that grafting semantic processing becomes much easier, especially if several kinds of processing are needed — for a compiler, a pretty-printer, a syntax-directed editor etc.
The library cannot match the performance of more standard approaches but remains useful in applications where flexibility is more important than raw speed. It is also a good teaching tool.
Discusses in some depth why object-oriented programming should use strong typing, and what kind of type system it requires.
One of a regular series of papers in JOOP, before it officially became the Eiffel column .
A discussion of typing issues.
What does static typing mean in an object-oriented context?
Many people see object-oriented programming as the next thing after structured programming. This made no sense to me, particularly since I had learned both from the Structured Programming volume (Dahl, Dijkstra, Hoare), where the first monograph by Dijkstra presented structured programming, the second by Hoare presented a structured approach to data modeling, and the third by Dahl (with Hoare) presented Simula 67, i.e. O-O techniques. I took the opportunity of an invitation by the Structured Programming journal to present the conceptual path that led from structured programming to the full implementation of O-O ideas in Eiffel.
 (Co-editor, with others including: Jean Bézivin, Roger Duke, Raimund Ege, Timothy Korson, Christine Mingins, Jean-Marc Nerson, Jean-François Perrot, John Potter, Wolfgang Pree, Madhu Singh, Mario Tokoro) TOOLS EUROPE, USA, PACIFIC and ASIA conferences (Technology of Object-Oriented Languages and Systems) 1 to 38, Paris, Sydney, Melbourne, Dortmund, Santa Barbara, Versailles, Zurich, published by SOL (vol. 1), Angkor (volume 2), Prentice Hall (vols. 4 to 26) and IEEE Computer Society Press (vol. 27 on), 1989 to 2003. (Volumes since 2007, published by JOT then Springer Lecture Notes in Computer Science, are listed separately.)
The TOOLS conference series is one of the longest-running conferences in software engineering and specifically in the area of object technology, component-based development, patterns and model-based development. Going back to 1988, it has had almost 50 sessions and provided a venue for many of the innovations in the field over the years. Now organized by ETH Zurich, typically in the week across June and July and not necessarily in Zurich, the conference continues to thrive.
The proceedings provide a unique record of the progress of software technology over more than two decades.
Explains why multiple inheritance, in its full glory, is essential to proper software design.
One of a regular series of papers in JOOP, before it officially became the Eiffel column .
Explains why global variables are an impediment to software quality, and how Eiffel provides an object-oriented mechanism to handle shared information: once routines. The lesson has not really been heeded in other languages, which continue to provide static functions and other constructs incompatible with object-oriented concepts and principles of modular design.
One of a regular series of papers in JOOP, before it officially became the Eiffel column .
The first publication, I think, to talk not only about the Eiffel method and language but also about the environment — a very early and primitive version of it.
One of the first publications about Eiffel. Computer Language, which I believe no longer exists, was an industry-oriented publication reaching a broad audience. I wasn't too excited to see that the article had been published under the rubric “Exotic Language of the Month Club”, although it turned out not to matter at all.
I believe that Eiffel's exception handling is among the major contributions of the method and language. This article presented the first — as far as I know — coherent discussion of what it means to have a “normal” or “abnormal” executions, and as a result the first satisfactory definition of exceptions. There had been good work on exceptions before, notably by Brian Randell and Flaviu Cristian, but they lacked a notion of correctness, which this paper obtains through contracts.
The paper was rejected at the first ECOOP 1987 in Paris, under dubious conditions, and I was sufficiently taken aback not to want to resubmit it elsewhere, although the ideas made their way to other publications such as Object-Oriented Software Construction  . The printout included here (link above right) ends with a note on the process, showing how angry I was at the time. The anger has subsided, but the ideas described in the paper remain important. While exception mechanisms that appeared since then in C++ and Java (try...catch...) are carefully designed and widely used, programmers still commonly misunderstand what an exception is and when exception handling is appropriate.
An introduction to Eiffel, often revised and extended since then.
 Object-Oriented Software Construction, Prentice Hall, 592 pages, 1988. Translations: German (Carl Hanser Verlag), French (InterEditions), Italian (Jackson publishing), Japanese (ASCII Corp.), Dutch (Prentice Hall), Chinese, Rumanian. (See  for second edition, now available online.)
This first edition sold something like 150,000 copies and was widely translated. Many people told me over the years that they “understood O-O” through it. The second edition supersedes it, although it loses the concision of the original.
Proceedings of the 1987 ICSE, of which I was program chair with Larry Druffel.
The first extensive published description of Eiffel. It was very difficult to publish about Eiffel at the time; I am deeply grateful to Robert Glass, the editor of the Journal of Systems and Software, for accepting the paper. JSS remains one of the best journals in the field.
Replaced by  and later EiffelStudio manuals.
 With Jean-Marc Nerson and Masanobu Matsuo: Safe and Reusable Programming using Eiffel, in Proceedings of First European Software Engineering Conference (ESEC 87), Strasbourg (France), September 8-11, 1987, Lecture Notes in Computer Science, Springer, 1987.
 With Mananobu Matsuo, Yasutsugu Doi, Hiroshi Matsumoto and Jean-Marc Nerson: The Cépage structural editor (in Japanese), in Japanese Society for Computer Science, Tokyo, July 1987, pages 391-405.
 Reusability: the Case for Object-Oriented Design, in IEEE Software, vol. 4, no. 2, March 1987, pages 50-62. Republished in the following volumes: Selected Reprints in Software, ed. M. Zelkowitz, IEEE Press, 1987; Software Reusability, ed. T. Biggerstaff, Addison-Wesley, 1988; Object-Oriented Computing, IEEE Press, 1988. (In the list of most influential Software papers in the 25th-anniversary list of IEEE Software.
A widely cited paper that explained the link between object-oriented techniques and software engineering concerns such as reusability.
The first publication — after the UCSB technical report  — specifically devoted to describing Eiffel as a method and language.
I gave several hundred sessions of this course, usually over two days, and still occasionally present an updated version. It covers the essential concepts of object technology with particular emphasis on design methodology and Design by Contract.
ArchiText (originally called Cépage), a sophisticated syntax-directed editor adaptable to any language, was the first product of Eiffel Software.  and  described the original prototype; this article presents the released version of the tool. See  about the display algorithm and its supporting theory.
 Genericity versus inheritance, in The Journal of Pascal, Ada and Modula-2, 1987. (Revised version of OOPSLA '86 paper .)
See the comments for reference .
Reuse has always been at the center of the Eiffel method, and the basic libraries were actually devised before the language was finalized. This is the original library manual; many revisions later, some of the material turned into the book Reusable Software .
 Genericity versus inheritance, in ACM Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA), Portland (Oregon), September 29 - October 2, 1986, pages 391-405. (See also journal version: .)
My paper at the first OOPSLA conference. It explained, for the first time as far as I know, why a sufficiently expressive object-oriented language must support both inheritance and genericity. It used Eiffel, which had both from the start, as an illustration.
Most people thought that the argument was academic and that genericity was superfluous (except the Ada camp, which thought that genericity was enough and inheritance was too complicated). C++ did not have genericity then; templates were added several years later. Java did not have genericity when it was introduced in 1995; it got generics, at great cost and suffering, ten years later. .NET and C# did not have genericity when they were introduced in 1999; they got generics several years later. Recent versions of Ada have introduced inheritance.
The survey article on software engineering for a technical encyclopedia. See also the entry on programming languages .
An algorithm description, with correctness and performance analysis. The purpose of the algorithm is to search for strings in a text, where the set of search strings may change as the execution processes; an example is an application to build a book index automatically (truly automatically, with the system actually looking in the text for words selected so far).
 With Alain Bossavit: Transformation de Programmes: Une Application à la Programmation des Super-Ordinateurs (Program Transformation: An Application to Supercomputer Programming), in Journées AFCET-Ada, December 1984.
This ICSE paper describes a simple mathematical framework, based on binary relations, for reasoning about software concepts. The core idea is that we can discuss software artifacts through a mathematical theory. It is well known that one can formally describe the semantics of individual program elements, but there still has been far less work on formalizing the abstract properties and interconnections of higher-level objects of software engineering such as modules, compilation units, projects, teams, deadlines and such. An example of work in that direction is Lee Osterweil's “Software processes are software too”.
The SKB system (Software Knowlege Base) described in the article provides a set of general relations charactizing software development, a theory describing the general mathematical properties of these relations, and application to the modeling of specific projects.
The ideas are still relevant, for example to the work of Semat . On one specific point I would use a different approach today: the paper assumes that descriptions will be entered separately from the software texts; I have learned that such an approach — applied for example by UML modeling — does not scale. It it raises the unsurmountable problem of maintaining consistency when things start to change in either the software or the descriptions. The “Single Model Principle” embodied in the Eiffel method and environment holds that all information about a software system, at any level of abstraction, should be in the system text or extractable, through tools, from that text. This guarantees that we avoid the “Dorian Gray Syndrome”: inconsistent evolution paths between what we think we know about the system and what the system truly is.
The SKB ideas can be applied in conformance to the Single Model Principle; this remains an exciting potential endeavor.
The book under review unfortunately reflected some pretty worrisome misunderstandings, and the review was not too shy about pointing them out.
 On Formalism in Specifications, in IEEE Software, vol. 3, no. 1, January 1985, pages 6-25 (cover feature). (Translated and adapted from .) Republished in T. Colburn, J. Fetzer, and T. Rankin (eds.), Program Verification: Fundamental Problems in Computer Science, Kluwer Academic Publishers, Dordrecht, Netherlands, 1993. Also in Dutch translation: Over het gebruijk van formalismen in specificaties, in Informatie, jaargang 28 nr. 5-6, 1986.
This is an advocacy paper for the use of formal techniques in software specification. Some of the important points are a list of common mistakes in requirements documents (“The Seven Sins of the specifier”), and the advice of having a roundtrip between informal and formal: if you start from informal (natural language, say English) requirements and write a formal version — as the paper does — don't stop there but produce a new English text that reflects the mathematical description. This gives a different kind of natural language requirements, possibly surprising at first but more precise and usable. The description of the Eiffel language  is written in such a style.
After my experience with Z I developed the M method as an attempt to make formal specifications more practical and in particular more scalable. The notation has modular mechanisms, including inheritance and other object-oriented techniques, for developing and managing large specifications of complex systems. Other priorities prevented me from continuing the development of M, but this initial work taught me a lot. In particular many of the fundamental ideas and notations found their way into Eiffel.
Describes an algorithm for smart display of program texts on a fixed-size area: instead of forcing users to scroll up and down, the tool automatically adapts the view to the available space, collapsing and expanding syntactic structures as needed. The resulting user experience is more comfortable than with usual approaches to program display (which typically are not specifically designed for programs but just display them as any other texts). The algorithm relies on a small mathematical theory, expressed in the form of an abstract data type specification. It was designed and implemented as part of our ArchiText tool    . I hope to get back to it some day and include it in EiffelStudio.
The first description of Eiffel, published as a technical report at UCSB. Thanks to the help of the ETH library I was able recently to locate a copy from Hannover (see the link to the PDF). The language has obviously changed, but the key concepts are there. Also notable is the emphasis on components and reuse: a good part of the report is devoted to code for reusable library classes — the seed of what has now become EiffelBase. Eiffel was devised to write elegant analysis, design and code, and it is significant that the first writeup ever showed program examples in full.
 With Alain Bossavit: An Application of Program Transformation to Supercomputer Programming, pages 27-38 in Vector and Parallel Processors in Computational Science (Eds. Duff and Reid), special issue of Computer Physics Communications, North-Holland Publishing Company, Amsterdam, 1985. (Revised version of the VAPP conference presentation, Oxford, 1984; see .)
Part of my collaboration with Alain Bossavit on bringing modern programming techniques to scientific computing. The focus here is on applying mathematically rigorous program transformations to derive an efficient parallel algorithm (for a vector computer) from a sequential version.
A case study in recursion removal: the description of a highly compact algorithm for the Tower of Hanoi problem. Presented in its final form without explanations, the algorithm would be hard to understand, but it follows from a systematic sequence of transformations. The algorithm and its derivation actually come from , first published in 1978.
 With Alain Bossavit: An Application of Program Transformation to Supercomputer Programming (invited presentation), in Vector and Parallel Processors in Computational Sciences (Proceedings of VAPP Conference, Oxford, 28-31 August 1984), eds. I.S. Duff and J.K. Reid, North Holland, 1984, pages 27-38. ( is the journal version).
I learned a lot from Alain Bossavit in my collaboration with him on software issues of numerical computation. See the comments on the journal version, .
First iteration of what became the Software Knowledge Base paper at ICSE 1985 .
 With Jean-Marc Nerson: Cépage : Un Editeur structurel Pleine Page, in Second Colloque de Génie Logiciel (Second Conference on Software Engineering), AFCET, Nice (France), June 1984, pages 153-158. See  for English translation.
 A System Description Method, in International Workshop on Models and Languages for Software Specification and design, Orlando (Fl.), eds. Robert G. Babb II and Ali Mili, Report DIUL-RR-8408 (Université Laval, Département d'Informatique, Quéebec), March 1984, pages 42-46. (For a fuller description, see the UCSB report .)
A short description of the M specification method; see .
 An Introduction to the Art of Writing Correct Programs, course notes, March 1984 (Revised January 1985), Report TRCS84-05, Computer Science Department, University of California, Santa Barbara (course notes for CS130A).
I hope some day to find a copy of this report, which — as I remember it — describes systematic program development from specifications, strongly influenced by Dijkstra.
English translation (not by me) of ; the comment on that entry.
 The human factor has knocked three times: review of three books on human factors in interactive systems (Card, Moran, Newell; Ledgard, Singer, Whiteside; Shneiderman), in TSI (Technology and Science of Informatics), vol. 3, no. 3, pages 205-208 (English Edition) 1984.
Review of several books on software system ergonomics, including an important book by Shneiderman, and a highly original and still puzzling volume by Card, Moran and Newell that deserves to be better known.
A criticism of an example in Gries's book The Science of Programming. The example was a supposedly systematic derivation of a program from a specification; the specification had a couple of mistakes, but the program was right, which I found fishy. Gries said it was only a typo; I thought something deeper was involved. Years later we met and he was gracious enough not to bear a grudge. I still think I may have had a point, but of course once you have left a sufficiently long trail of publications yourself you start thinking twice about making a big fuss about a mistake by someone else.
It did not help that the published version of my note was the wrong one: not the final, carefully typeset and proofread version that I sent to the SEN editor for publication (if you are criticizing someone for two mistaken occurrences of “less than or equal” instead of by “less than”, you'd better be careful about your own notations) but the manually annotated draft that I has sent a few months before to ask for an informal opinion of the material's suitability for publication.
A software engineer's view of the issues of scientific and engineering software.
 Towards a Two-Dimensional Programming Environment, in Proceedings of the European Conference on Integrated Computing Systems, (ECICS 82), Stresa (Italy), 1-3 September 1982, eds. Pierpaolo Degano and Erik Sandewall, North-Holland, 1983, pages 167-179. (English version, revised, of .) Republished in Readings in Artificial Intelligence, Tioga Press, Palo Alto, 1983.
Description of work towards providing advanced object-oriented techniques for software development. We were constrained by the rather conservative OS environment in which we wre working, but were able all the same to take advantage of Simula 67 and two-dimensional displays. The conference where this paper was presented was one of the first large-scale gatyherings of O-O enthusiasts (including Jean Bézivin and Adele Goldberg), long before object technology became mainstream.
Working in a traditional environment (Fortran, IBM operating systems) I strived to apply modern principles of programming methodology, including object-oriented technques. In particular I developed a set of strict principles for building software packages that provided a close equivalent to O-O libraries. The article describes these principles and presents some of the packages they helped develop, which were widely used for many years. It includes a presentation of the concept of abstract data type that several people told me they had found useful.
 Vers un Environnement Conversationnel à deux dimensions, in Journées BIGRE, Grenoble, 27-29 January 1982. (For revised English version see .)
See the comments on the English version .
Review, originally published in TSI , of a book on compilation.
An avid reader of software books, I took advantage of my position as editor-in-chief of TSI to publish a number of reviews of interesting books. The journal had both a French and English editions (nowadays it is mostly English).
A survey of commercial and academic static analysis tools.
 With Alain Bossavit: The Design of Vector Programs, in Algorithmic Languages (Proceedings of IFIP International Symposium on Algorithmic Languages, Amsterdam, 26-29 October 1981), eds. Jaco de Bakker and R.P. van Vliet, North-Holland Publishing Company, Amsterdam, 1981, pages 99-114.
This work applied constructive techniques of programming  to numerical algorithms. Our organization had received the first Cray-I computer in continental Europe and we were busy understanding how to develop correct vectorized algorithms.
The publication is the proceedings of a symposium held in Amsterdam in honor of the 65th birthday of Aad van Wijngaarden, the creator of Algol 68. It was a rather eventful and even at times tense conference, not least because of frequent comments by Edsger Dijkstra. I never quite knew what Dijkstra thought of my work; imagine my surprise when not long ago — that is to say, almost three decades later — I stumbled upon a trip report about that very conference, where he mentions my talk (and others, such as Manfred Broy's) favorably.
 With Bertrand Heilbronn and Alain Poujol: Avantages et Limites des Spécifications formelles: Une Expérience industrielle (Benefits and Limitations of Formal Specifications: An Experiment in Industry), in Journées AFCET-AUTOMATIQUE sur la Validation des Spécifications fonctionnelles, AFCET, Paris, 23 October 1981.
An application of formal techniques to safety-critical software.
 With Gérard Brisson and Françoise Vapné-Ficheux: Ensorcelé: Entrées et Sorties Sans Format (A General-Purpose Input-Output Package) (manual), Atelier Logiciel no. 4, 7, Electricité de France, Clamart (France), April 1981 (Fourth Edition).
 With Michel Demuynck: Les Langages de Spécification, followed by À la Recherche de la Spécification Idéale (two survey papers on specification languages), in Zéro-Un Informatique, no. 150 et 151, April and May 1981, pp. 62-70, 65-70.
A version of our specification language survey  intended for a wider audience (01-Informatique is an industry-oriented computer weekly).
 A Three-Level Approach to Data Structure Description, and Notational Framework, in ACM-NBS Workshop on Data Abstraction, Databases and Conceptual Modelling, Pingree Park, Colorado, 25-26 June 1981, eds. Michael Brodie and Steven Zilles; proceedings appear as the January 1981 issues of the SIPLAN, SIGMOD, SIGART newsletters, pages 164-166.
This short paper presents the three levels of description for data structures and, in general, software artifacts: functional, constructive (logical) and physical. This concepts are important for a good understanding of object technology. Influenced by abstract data type theory and Codd's relational work, they come from  and were further refined in .
 With Eric de Drouas: A Vector Computer: The Cray-1 and how to program it (1-hour instructional video film on vector programming on the Cray-1), Electricité de France, Clamart (France), 1981, French and English versions.
An instructional film, with animation and sound, on how to program the Cray-1 vector computer. An essential component of the presentation was our use, to illustrate the machine's fundamental cycle, of the second movement of Haydn's “clock” symphony.
Techniques de l'Ingénieur is a technical encyclopedia. They asked me to write the general entry on programming languages (and also, a few years later, the entry on software engineering ). It describes the state of programming languages at the time. I was invited to contribute a revision a few years later but unfortunately no longer had the time.
The first event in a series of national conferences on software engineering in France.
 A Basis for the Constructive Approach to Programming, in Information Processing 80 (Proceedings of the IFIP World Computer Congress), Tokyo, October 6-9, 1980), ed. S. H. Lavington, North-Holland Publishing Company, Amsterdam, pages 293-298, 1980.
I was able only recently to recover this paper and found it still useful. It follows the lead of Dijkstra and others to describe program construction from specifications; the core point is that in many cases one can obtain loop invariants and the corresponding loops simply by weakening postconditions. The article identifies and applies a few heuristics such as constant relaxation and uncoupling. The most striking example is Newton's square root algorithm, which follows almost trivially from merely applying uncoupling. The paper was strongly influenced by my collaboration with Alain Bossavit      .
The IFIP 80 session at which I presented this paper was chaired by Harlan Mills, whose warm encouragement was critical.
More recent (and far more sophisticated) work led by Carlo Furia  picks on some of the ideas of this paper.
Examples of our early work applying object-oriented programming, using Simula 67, to the building of software tools.
 Un Calculateur Vectoriel: Le Cray-1 et sa Programmation (Version 2) (A Vector Computer: The Cray-1 and how to Program It), Atelier Logiciel no. 24, HI-34552/01, Electricité de France, Clamart (France), June 4, 1980.
 With Jean-Raymond Abrial and Stephen A. Schuman: A Specification Language, in On the Construction of Programs, Cambridge University Press, eds. R. McNaughten and R.C. McKeag, 1980. (Description of early version of the Z specification language.)
This is the first article describing the Z specification language. (Chapter 8 of  described an even earlier version.) Afterwards Oxford University became interested in Z and transformed it significantly.
 Sur le Formalisme dans les Spécifications (On formalism in Specifications), in GLOBULE (Newsletter of the AFCET Software Engineering Working Group), no. 1, pages 81-122 1979. (For revised English version see .)
I am particularly grateful to Axel van Lamsweerde for expressing his appreciation of this paper, initially published in a newsletter. This gave me the idea of writing a revised English version that ended up being widely quoted . See the comments on that paper.
 With Alain Bossavit: On the Constructive Approach to Programming: The Case of “Partial Choleski Factorization” (A Tool for Static Condensation in Numerical Analysis), in Advances in Computer Methods for Partial Differential Equations III (IMACS Symposium, Bethlehem, Pennsylvania), eds. Vichnevetsky and Stepleman, pages 287-291 1979.
Another outcome of my collaboration with Alain Bossavit to apply modern programming methodology to scientific computing applications. In this case the derivation applies to a classical linear algebra method, Choleski factorization.
 With Alain Bossavit: Sur la Programmation rationnelle des Algorithmes numériques (On the systematic development of numerical algorithms), in Bulletin de la Direction des Etudes et Recherches d'Electricité de France, Série C (Informatique), Clamart (France), no. 2, 1979.
Part of my collaboration with Alain Bossavit on bringing modern programming techniques to scientific computing applications. The focus is on systematic development from specifications through refinement.
 Quelques concepts importants des langages de programmation modernes et leur expression en Simula 67 (Some Important Concepts of Modern Programming Languages and their Expression in Simula 67), in Bulletin de la Direction des Etudes et Recherches d'Electricité de France, Série C (Informatique), Clamart (France), no. 1, 1979, pages 89-150 Also in GROPLAN 9, AFCET, 1979.
A presentation of object-oriented programming and the Simula language. I had started by that time to use Simula extensively; the reception to O-O ideas was tepid, however — even in the academic community where Pascal and Ada were all the rage. There were exceptions, in particular Jacques André and Jean Bézivin in France.
The paper was first presented at a very stimulating meeting of GROPLAN, the French programming language interest group (i.e. similar to SIGPLAN), in Corsica, where I also first heard about abstract interpretation from Patrick and Radhia Cousot.
 With Michel Demuynck: Les Langages de Spécification (Specification Languages), in Bulletin de la Direction des Etudes et Recherches d'Electricité de France, Série C (Informatique), Clamart (France), no. 1, 1979, pages 39-60.
An early survey of specification languages. See also  for a later version. The impetus whas that we had become excited about Z (in its version of the time) and wanted to showcase it.
 With Michel Demuynck: Les Langages de Spécification: Vers une meilleure Compréhension des Problèmes, et des Programmes plus fiables (Specification Languages: Towards More Reliable Programs), in Convention Informatique, Paris, September 1978.
The initial version of .
 With Jean-Raymond Abrial: Course notes on formal specification; case study (automated directory system), INRIA-EDF-CEA Summer School on Programming Methodology, Le-Bréau-sans-Nappe, France, July 1978.
An algorithm description.
We wrote this book fresh out of school and managed to convince the publisher to include everything (other publishers wanted us to trim it down to 250 pages). It is a compendium of programming methodology, programming techniques, fundamental algorithms and data structures. It emphasizes program correctness, through assertion techniques, and software architecture. The chapter on programming methodology contains the first ever published description of the Z specification language anywhere (as far as I know), in a very early form. The book was extremely successful in France, both as a textbook and for engineers in industry; incredibly, it still seems to be in print.
The Russian translation was also widely circulated and I still meet people from Russia who tell me this is where they learned programming. There never was an English translation: I accepted Prentice Hall's and Tony Hoare's suggestion that I do the translation myself — a huge mistake, as I started rewriting the book instead of translating it, and never finished, although that effort, titled Applied Programming Methodology, fed later work. In particular the object-oriented pseudocode that I used throughout, an extension of the notation in Méthodes de Programmation, led directly to Eiffel.
A series of some 50 reports, some on methodology, some describing software development tools that we built. A few are listed individually in other references of this bibliography, but there were many more.
Reported on our experience of teaching modern programming techniques in an industrial setting, to programmers previously trained in very traditional ways.
 La Description des Structures de Données (The Description of Data Structures), in Bulletin de la Direction des Etudes et Recherches d'Electricité de France, Série C (Informatique), Clamart (France), 1976.
A theoretical and practical discussion of abstract data types, expanding on the initial work of Liskov and Zilles and including many ideas that were also found in Guttag's work published a year later. Unfortunately I never wrote an English version.
Discussion of a first experience of teaching programming in an engineering school.
Course notes for an early course. I always had a special fondness for Algol W (more than for its successor, Pascal) and found it an excellent teaching vehicle.
Meyer home - Publications - Events - Software engineering home - CS home