New paper: Theory of Programs






Programming, wrote Dijkstra many years ago, is a branch of applied mathematics. That is only half of the picture: the other half is engineering, and this dual nature of programming is part of its attraction. Descriptions of the mathematical side are generally, in my view, too complicated. This article [1] presents a mathematical theory of … Read more




Framing the frame problem (new paper)






Among the open problems of verification, particularly the verification of object-oriented programs, one of the most vexing is framing: how to specify and verify what programs element do not change. Continuing previous work, this article presents a “double frame inference” method, automatic on both sides the specification and verification sides. There is no need to … Read more




A gold medal






The French National Research Center (CNRS) has just awarded [1] its annual gold medal to Gérard Berry, a great recognition for an outstanding computer scientist. I first discovered Berry’s work through a brilliant 1976 article, Bottom-Up Computation of Recursive Programs [2], which explained recursion using methods of denotational semantics, and should really figure in collections … Read more




Computing: the Art, the Magic, the Science






  My colleagues and I have just finished recording our new MOOC (online course), an official ETH offering on the EdX platform. The preview is available [1] and the course will run starting in September. As readers of this blog know, I  have enthusiastically, under the impulsion of Marco Piccioni at ETH, embraced MOOC technology … Read more




Reading Notes: Single-Entry, Single-Exit






  It is remarkable that almost half a century after Dijkstra’s goto article, and however copiously and reverently it may be cited, today’s programs (other than in Eiffel) are still an orgy of gotos. There are not called gotos, being described as constructs that break out of a loop or exit a routine in multiple … Read more




New article: passive processors






  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, … Read more




PhD positions in concurrency/distribution/verification at ETH






As part of our “Concurrency Made Easy” ERC Advanced Investigator Grant project (2012-2017), we are offering PhD positions at the Chair of Software Engineering of ETH Zurich. The goal of the project is to build a sophisticated programming and verification architecture to make concurrent and distributed programming simple and reliable, based on the ideas of … Read more




Saint Petersburg Software Engineering Seminar: 14 January 2014 (6 PM)






There will be two talks in the Software Engineering Seminar at ITMO, 18:00 local time, Tuesday, January 14, 2014. Please arrive 10 minutes early for registration. Place: ITMO, Sytninskaya Ulitsa, Saint Petersburg. Andrey Terekhov (SPBGU): Programming crystals (I do not know whether this talk will be in Russian or English. An abstract follows but the … Read more