About

Rustan Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. He is known for his work on programming methods and program verification tools, and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.

Prior to Microsoft Research, Leino worked at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and hosts the Verification Corner channel on youtube. In his spare time, he plays music and, recently having ended his tenure as cardio exercise class instructor, is trying to learn to dance.

Projects

Project Everest – Verified Secure Implementations of the HTTPS Ecosystem

Established: May 31, 2016

Summary Project Everest aims to build and deploy a verified HTTPS stack. The HTTPS ecosystem (HTTPS and TLS protocols, X.509 public key infrastructure, crypto algorithms) is the foundation on which Internet security is built. Unfortunately, this ecosystem is extremely brittle,…

Ironclad

Established: October 2, 2014

An Ironclad App lets a user securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a formal abstract specification of the app's behavior. This does more than eliminate implementation…

Jennisys

Established: February 7, 2012

This is where programs begin. Jennisys is a programming language that emphasizes clean public interfaces and lets programmers describe the data structures they intend a private implementation to use. Code is underemphasized, and Jennisys attempts to synthesize code automatically from…

The Verification Corner

Established: January 8, 2010

The Verification Corner is a video series on YouTube that explains different concepts of software verification.         Stepwise refinement - 10/8/2010: In this episode, Kuat Yessenov and Rustan Leino, Principal Researcher in the…

Dafny: A Language and Program Verifier for Functional Correctness

Established: December 23, 2008

Dafny is a programming language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. The Dafny programming language is designed to support the static verification of programs. It is imperative,…

Chalice

Established: December 23, 2008

Chalice is an experimental language that explores specification and verification of concurrency in programs. The language supports dynamic object creation, dynamic thread creation (fork and join), mutual-exclusion and readers-writers locks, monitor invariants, thread pre- and postconditions. The language allows fine-grained…

Boogie: An Intermediate Verification Language

Established: December 10, 2008

Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for C and the verifiers for…

Spec#

Established: June 11, 2004

Spec# is a formal language for API contracts (influenced by JML, AsmL, and Eiffel), which extends C# with constructs for non-null types, preconditions, postconditions, and object invariants. Spec# comes with a sound programming methodology that permits specification and reasoning about…

Publications

2016

2015

2014

2013

2012

2011

The 1st Verified Software Competition: Extended Experience Report
Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, Rustan Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiβ, in FM'11 Proceedings of the 17th international conference on Formal methods, June 20, 2011, View abstract, Download PDF

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1995

Projects

Other

Biography

Biography

bioRustan Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. He is known for his work on programming methods and program verification tools, and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.

Prior to Microsoft Research, Leino worked at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and hosts the Verification Corner channel on youtube. In his spare time, he plays music and, recently having ended his tenure as cardio exercise class instructor, is trying to learn to dance.

For more details than you want, see my curriculum vitae.

Pronunciation guide

Here is a rebus to help you say my name (pictures by Klas Leino).

rebus

  • roost – a support where birds rest
  • ten – the number
  • lei – a Hawaiian flower necklace
  • no – not so

Stress the first syllable of each name.  Never mind the fact that “t” appears twice in the rebus.

What’s in a name?

OLYMPUS DIGITAL CAMERASome people are surprised, even confused, by the structure of my name.  But it’s really quite simple: I have 3 given names (with initials K.R.M.) and 1 family name (Leino), where the middle one (Rustan) of the 3 given names has been designated as the one that I go by.  That’s all.  Nevertheless, it has happened that my name has been listed as if I were two people.  While some friends jealously have suggested that this seems to be a great way to double my number of publications, I just find it annoying and unprofessional.  To the left is a picture that proves I am but one person.  Now, please go check your BibTeX files.

Verification

verification-corner

In the Press

Leino in the press

pressWhy, don’t take it from me.  See what the press has to say.

Leino's Miscellany

Leino’s miscellany

miscellanyThis corner of the web contains a collections of miscellaneous thoughts and ponderings by yours truly.  You can also find some of my early KRML notes at mathmeth.com.

Subscripts in technical presentations

Any technical writer who uses formulas or variables ought to consider the issues brought up in this short article.  [PDF]  K. Rustan M. Leino.  Real estate of names Information Processing Letters, 77(2-4):169-171, February 2001.

ASCII implication

Many operators in programming languages have standard representations, like + and < .  Logical implication (Þ), however, is an operator that different programming/specification languages have chosen to represent in different ways, particularly when the language uses ASCII characters.  I wish to make a recommendation to such language designers:  choose ==> over =>.  Here’s why:

If you think of the boolean type as an enumeration consisting of the values false and true, then many languages would let you compare these values with the ordering ≤.  In ASCII, you would then write false < = true.  Similarly, if you think of the booleans as forming a lattice, then common choice is to make false be the bottom element and true the top element, so then, too, does false < = true make sense.  The ordering in the lattice in fact the implication ordering, so ≤ is the same as Þ.  In typeset mathematics, one is used to this, but in ASCII, it would be confusing that both false < = true and false => true would hold.  So don’t choose => as your implication symbol; choose something else, like ==>.

Also, if you have implication, chances are you would also want reverse implication, Ü (“follows from”, or as Jan van de Snepscheut jokingly used to say, “explies”).  If you had chosen => for implies, the natural choice for explies would then be < =.  But this would be disastrous, because then you’d have both false < = true and true => false!  So, don’t choose => as your implication symbol; instead, consider ==> for implies and < == for explies.

Finally, although binding powers of operators are not always chosen the same way by different people, I like giving conjunction and disjunction higher binding power than implication.  To make the visual appearance of expressions suggestive of the binding powers, you want to make lower-precedence operators occupy more horizontal space.  A simple way to achieve that is to make operators longer.  Using 3 characters for implication instead of 2 thus achieves this effect:  your eyes would naturally read A && B ==> C && D as (A && B) ==> (C && D), not A && (B ==> C) && D.  So, don’t choose => as your implication operator, choose ==>.

Type setting variable declarations in LaTeX

If you have written papers that include variable declarations, you might have noticed that the type setting of “x : T” in TeX and LaTeX puts a lot of space on both sides of the colon.  If so, you probably want to use “colon” instead of “:“.  The idea behind “colon” is to give an appropriate amount of space in exactly this situation.  So write “x colon T“.  Similarly, “to” is defined to give the symbol and spacing to write function types, as in “f colon A to B“.

If you’re like me, you might also want some more space between such variable declarations.  Unless I’m cramped for space, I write “x colon T,~ y colon U“.

Group Pictures

Group pictures

Rustan Leino is a Principal Researcher in the RiSE group at Microsoft Research, where he works on various programming language and verification projects.

I entered the RiSE logo contest with this:

krml-rise-logo

This is the Programming Languages and Methods (PLM) part of RiSE, June 2008:

Zhaozhong NiPeter MüllerRustan LeinoMike Barnett

plm-2008-fullsize

Here is a picture I made of the PLM group in early 2006:

Daan LeijenWolfram SchulteMike BarnettManuel FähndrichRustan LeinoKRML 2006

plm-2006-fullsize

A hip photo of the pop group Bodies Without Organs (BWO) inspired me to make the following picture of my two summer 2006 research interns and me:

bwo-specsharp-medium          bwo

Prior to the formation of PLM, I worked in the Software Productivity Tools (SPT) group, for which I had also made a picture:

spt-group-picture-full-size

Music

music

Puzzles

puzzleHere are some mathematical puzzles that I have enjoyed. Most of them are of the kind that you can discuss and solve at a dinner table, usually without pen and paper. So as not to spoil your fun, no solutions are given on this page, but for some problems I have provided some hints.

Half the area of an L

new[I was asked this puzzle by Vlad Rusu, who in turn heard it from Grigore Rosu and family]

Two arbitrary rectangles are placed to form an “L”. That is, the lower left-hand corner of the two rectangles share the same point. (What I’m trying to say is that there’s an “L” whose “I” and “_” parts have arbitrary widths and heights.) Using only a (pen and a) straightedge (that is, no measuring device and no compass), figure out a way to, with a single straight cut, divide the “L” into two pieces of equal area.

A game of 2014 cards

new[I got this problem from Radu Grigore, who I think told me it was a problem used in the 2009 Math Olympics. I suppose perhaps the problem then involved 2009 cards.]

There is a table with a row of 2014 cards. Each card has a red side and a blue side. We’ll say that a card is red if the color on its visible face is red, and analogously for blue. Two players take turns to do the following move: select any 50 consecutive cards where the left-most card is red, then flip each of those 50 cards (thus, for those 50 cards, turning red cards into blue cards and blue cards into red cards). Both players look at the cards from the same side of the table, so “left-most” means the same to both of the players (that is, you can think of one of the ends of the table as being designated as the left end). When it is a player’s turn, if that player cannot make a move (that is, if there is no way to select 50 consecutive cards the left-most one of which is red), then that player loses and the other player wins. If you are one of the players and all cards are initially red, can you be sure to win, and if so, do you want to be the player who goes first or second?

Evaluating a polynomial

new[Prakash Panangaden told me this problem]

There is a polynomial and you have access to a function that evaluates that polynomial at a given number. You don’t know the degree of the polynomial, nor do you know any of the coefficients of its terms. However, you are told that all coefficients are non-negative integers. How many times do you need to call the evaluation function in order to identify the polynomial (that is, to figure out the values of its coefficients)?

Picking the larger of two cards

new[Roger Wattenhofer told me this puzzle]

Someone picks, at their will, two cards from a deck of cards. The cards have different numbers, so one is higher than the other. (In other words, the person picks two distinct numbers in the inclusive range 1 through 13.) The cards are placed face down on a table in front of you. You get to choose one of the cards and turn it face up. Now, you will select one of the two cards (one of whose face you can see, the other one you can’t). If you select the highest card, you win. Design a card-selection strategy for which your chance of winning is strictly greater than 50%.

Enclosing land by fence pieces

[I got this puzzle from Serdar Tasiran.]

You are given one 44-meter piece of fence and 48 one-meter pieces of fence. Assume each piece is a straight and unbendable. What is the large area of (flat) land that you can enclose using these fence pieces?

Planar configuration of straight connecting lines

[Radu Grigore told me this problem. I think may have heard it 20 years earlier from Jan van de Snepscheut.]

Given an even number of points in general positions on the plane (that is, no three points co-linear), can you partition the points into pairs and connect the two points of each pair with a single straight line such that the straight lines do not overlap?

Reducing nearby enemies

[I got this puzzle from Jason Koenig.]

You are given an irreflexive symmetric (but not necessarily transitive) “enemies” relation on a set of people. In other words, if person A is an enemy of a person B, then B is also an enemy of A. How can you divide up the people into two houses in such a way that every person has at least as many enemies in the other house as in their own house?

[Hint: As Radu Grigore pointed out to me, solving the Planar configuration of straight connecting lines puzzle may provide a hint to solving this puzzle.]

Transporting bananas

[Rupak Majumdar told me this intriguing puzzle.]

You have 3000 bananas that you want to transport a distance of 1000 km. The transport will be done by a monkey. The monkey can carry as many as 1000 bananas at any one time. With each kilometer traveled (forward or backward), the money consumes 1 banana. How many bananas can you get across to the other side?

Car and key hide-and-seek

[A puzzle Aistis Simaitis gave me inspired this puzzle.]

In a room are three boxes that on the outside look identical. One of the boxes contains a car, one contains a key, and one contains nothing. You and a partner get to decide amongst yourselves to each point to two boxes. When you have made your decision, the boxes are opened and their contents revealed. If one of the boxes your partner is pointing to contains the car and one of the boxes you are pointing to contains the key, then you will both win. What strategy maximizes the probability of winning, and what is the probability that you will win?

Handshakes at a dinner party

[Pamela Zave shared this problem with me.]

Hilary and Jocelyn are throwing a dinner party at their house and have invited four other couples. After the guests arrive, people greet each other by shaking hands. As you would expect, a couple do not shake hands with each other and no two people shake each other’s hands more than once. At some point during the handshaking process, Jocelyn gets up on a table and tells everyone to stop shaking hands. She also asks each person how many hands they have shaken and learns that no two people on the floor have shaken the same number of hands. How many hands has Hilary shaken?

Rectifying a pill mistake

[This is a slight rewording of a problem I got from Phil Wadler, who said he read the problem on xkcd.]

A man has a medical condition that requires him to take two kinds of pills, call them A and B. The man must take exactly one A pill and exactly one B pill each day, or he will die. The pills are taken by first dissolving them in water.

The man has a jar of A pills and a jar of B pills. One day, as he is about to take his pills, he takes out one A pill from the A jar and puts it in a glass of water. Then he accidentally takes out two B pills from the B jar and puts them in the water. Now, he is in the situation of having a glass of water with three dissolved pills, one A pill and two B pills. Unfortunately, the pills are very expensive, so the thought of throwing out the water with the 3 pills and starting over is out of the question. How should the man proceed in order to get the right quantity of A and B while not wasting any pills?

Chomp

[Clark Barrett told me this problem.]

Given is a (possibly enormous) rectangular chocolate bar, divided into small squares in the usual way. The chocolate holds a high quality standard, except for the square in the lower left-hand corner, which is poisonous. Two players take turns eating from the chocolate in the following manner: The player whose turn it is points to any one of the remaining squares, and then eats the selected square and all squares positioned above the selected square, to the right of the selected square, or both above and to the right of the selected square. Note, although the board starts off rectangular, it may take on non-rectangular shapes during game play. The object of the game is to avoid the poisonous square. Assuming the initial chocolate bar is larger than 1×1, prove that the player who starts has a winning strategy.

Hint: To my knowledge, no efficient strategy for winning the game is known. That is, to decide on the best next move, a player may need to consider all possible continuations of the game. Thus, you probably want to find a non-constructive proof. That is, to prove that the player who starts has a winning strategy, prove just the existence of such a strategy; in particular, steer away from proofs that would construct a winning strategy for the initial player.

Alternating T-shirt colors

[I received this puzzle from Vladislav Shcherbina, but I changed gloves into T-shirts to emphasize the people rather than the spaces between them.]

Ten friends walk into a room where each one of them receives a hat. On each hat is written a real number; no two hats have the same number. Each person can see the numbers written on his friends’ hats, but cannot see his own. The friends then go into individual rooms where they are each given the choice between a white T-shirt and a black T-shirt. Wearing the respective T-shirts they selected, the friends gather again and are lined up in the order of their hat numbers. The desired property is that the T-shirts colors now alternate.

The friends are allowed to decide on a strategy before walking into the room with the hats, but they are not otherwise allowed to communicate with each other (except that they can see each other’s hat numbers). Design a strategy that lets the friends always end up with alternating T-shirt colors.

Digit sums of multiples of 11

[I got this one from Madan Musuvathi.]

Some multiples of 11 have an even digit sum. For example, 7*11 = 77 and 7+7 = 14, which is even; 11*11 = 121 and 1+2+1 = 4, which is even. Do all multiples of 11 have an even digit sum? (Prove that they do or find the smallest that does not.)

Weighing piles of coins

[I got this puzzle from Dave Detlefs, who read it in an MIT Alumni magazine. This puzzle is a bit more involved than most puzzles on my page, so you may want a paper and pen (and some tenacity) for this one. Once you get into it, though, it’s a hard puzzle to put aside until you’ve solved it.]

There are two kinds of coins, genuine and counterfeit. A genuine coin weighs X grams and a counterfeit coin weighs X+delta grams, where X is a positive integer and delta is a non-zero real number strictly between -5 and +5. You are presented with 13 piles of 4 coins each. All of the coins are genuine, except for one pile, in which all 4 coins are counterfeit. You are given a precise scale (say, a digital scale capable of displaying any real number). You are to determine three things: X, delta, and which pile contains the counterfeit coins. But you’re only allowed to use the scale twice!

Guessing each other's coins

[I got this puzzle from Raphael Reischuk, who also has a little puzzle collection.]

You and a friend each has a fair coin. You can decide on a strategy and then play the following game, without any further communication with each other. You flip your coin and then write down a guess as to what your friend’s coin will say. Meanwhile, your friend flips her coin and writes down a guess as to what your coin says. There’s a third person involved: The third person collects your guesses and inspects your coins. If both you and your friend correctly guessed each other’s coins, then your team (you and your friend) receive 2 Euros from the third person. But if either you or your friend (or both) gets the guess wrong, then your team has to pay 1 Euro to the third person. This procedure is repeated all day. Assuming your object is to win money, are you happy to be on your team or would you rather trade places with the third person?

The duck and the fox

[I got this problem from Koen Claessen.]

A duck is in circular pond. The duck wants to swim ashore, because it wants to fly off and this particular duck is not able to start flying from the water. There is also a fox, on the shore. The fox wants to eat the duck, but this particular fox cannot swim, so it can only hope to catch the duck when the duck reaches the shore. The fox can run 4 times faster than the duck can swim. Is there always a way for the duck to escape?

Dropping eggs

[I think I’ve heard some version of this problem before, but heard this one from Sophia Drossopoulou and Alex Summers.]

There’s a certain kind of egg about which you wonder: What is the highest floor of a 36-story building from which you can drop an egg without it breaking? All eggs of this kind are identical, so you can conduct experiments. Unfortunately, you only have 2 eggs. Fortunately, if an egg survives a drop without breaking, it is as good as new–that is, you can then conduct another dropping experiment with it. What is the smallest number of drops that is sure to determine the answer to your wonderings?

Age of children

[I got this problem from the book In code: a mathematical journey by Sarah Flannery and David Flannery.]

A (presumed smart) insurance agent knocks on a door and a (presumed smart) woman opens. He introduces himself and asks if she has any children. She answers: 3. When he then asks their ages (which for this problem we abstract to integers), she hesitates. Then she decides to give him some information about their ages, saying “the product of their ages is 36”. He asks for more information and she gives in, saying “the sum of their ages is equal to our neighbors’ house number”. The man jumps over the fence, inspects the house number, and the returns. “You need to give me another hint”, he begs. “Alright”, she says, “my oldest child plays the piano”. What are the ages of the children?

Capturing a pirate ship

[Howard Lederer sent me this problem.]

You’re on a government ship, looking for a pirate ship. You know that the pirate ship travels at a constant speed, and you know what that speed is. Your ship can travel twice as fast as the pirate ship. Moreover, you know that the pirate ship travels along a straight line, but you don’t know what that line is. It’s very foggy, so foggy that you see nothing. But then! All of a sudden, and for just an instant, the fog clears enough to let you determine the exact position of the pirate ship. Then, the fog closes in again and you remain (forever) in the thick fog. Although you were able to determine the position of the pirate ship during that fog-free moment, you were not able to determine its direction. How will you navigate your government ship so that you will capture the pirate ship?

3-person duel

[I got this problem from Johannes Kinder, who said he heard it from his brother. I reformulated the setting.]

A particular basketball shootout game consists of a number of duels. In each duel, one player is the challenger. The challenger chooses another player to challenge, and then gets one chance to shoot the hoop. If the player makes the shot, the playing being challenged is out. If the player does not make the shot, or if the player chooses to skip his turn, then the game continues with the next duel. A player wins when only that player remains.

One day, this game is played by three players: A, B, and C. Their skill levels vary considerably: player A makes every shot, player B has a 50% chance of making a shot, and player C has a 30% chance of making a shot. Because of the difference in skill levels, they decide to let C begin, then B, then A, and so on (skipping any player who is out of the game) until there is a winner. If everyone plays to win, what strategy should each player follow?

[For this follow-up question, it will be helpful to have a paper and pen–not because the calculations are hard, but because it helps in remembering the numbers.]

If A, B, and C follow their winning strategies (as determined above), which player has the highest chance of winning the game?

The genders of the neighboring family's children

[This problem was inspired by some basic probability questions mentioned in a lecture by Eric Hehner (and that can be formalized and solved by calculation using this Probability Perspective), and some subsequent discussions with him, Itay Neeman, Jim Woodcook, Ana Cavalcanti, and Leo Freitas.]

The house next door has some new neighbors. They have two children, but you don’t know what mix of boys and girls they are. One day, your wife tells you “At least one of the children is a girl”. What is the probability that both are girls?

Your wife then tells you “The way I found out that at least one of the children is a girl is that I saw one of the children playing outside, and it was a girl”. Now, what is the probability that both are girls?

Finding a hermit

[Claude Marché told me this puzzle. At first, it seems quite similar to “Catching a spy” (below), but the solution is entirely unrelated.]

There are five holes arranged in a line. A hermit hides in one of them. Each night, the hermit moves to a different hole, either the neighboring hole on the left or the neighboring hole on the right. Once a day, you get to inspect one hole of your choice. How do you make sure you eventually find the hermit?

Witches at a coffee shop

[I got this puzzle from Alex Pintilie.]

Two witches each makes a nightly visit to an all-night coffee shop. Each arrives at a random time between 0:00 and 1:00. Each one of them stays for exactly 15 minutes. On any one given night, what is the probability that the witches will meet at the coffee shop?

Lemmings on a ledge

[Vladislav Shcherbina told me this problem.]

A ledge is 1 meter long. On it are N lemmings. Each lemming travels along the ledge at a constant speed of 1 meter/minute. A lemming continues in the same direction until it either falls off the ledge or it collides with another lemming. If two lemmings collide, they both immediately change their directions. Initially, the lemmings have arbitrary starting positions and starting directions. What is the longest time that may elapse before all lemmings have fallen off the ledge?

[Michael Jackson suggested the following variation of the problem: Suppose the ledge is not horizontal, but is leaning. A lemming now travels up the ledge at a speed of 1 meter/minute and travels down the ledge at a speed of 2 meters/minute. What is the longest time before all lemmings have fallen off?]

Poisoned wine

[I got this problem from Vladislav Shcherbina.]

You have 240 barrels of wine, one of which has been poisoned. After drinking the poisoned wine, one dies within 24 hours. You have 5 slaves whom you are willing to sacrifice in order to determine which barrel contains the poisoned wine. How do you achieve this in 48 hours?

Dropping 9-terms from the harmonic series

[Rajeev Joshi told me this problem.]

The harmonic series–that is, 1/1 + 1/2 + 1/3 + 1/4 + …–diverges. That is, the sum is not finite. This is in difference to, for example, a geometric series–like ½0 + ½1 + ½2 + ½3 + …–which converges, that is, has a finite sum.

Consider the harmonic series, but drop all terms whose denominator represented in decimal contains a 9. For example, you’d drop terms like 1/9, 1/19, 1/90, 1/992, 1/529110. Does the resulting series converge or diverge?

[More generally, you may consider representing the denominator in the base of your choice and dropping terms that contain a certain digit of your choice.]

[Here is a follow-up question suggested by Gary Leavens.]

Consider again the harmonic series, but drop a term only if the denominator represented in decimal contains two consecutive 9’s. For example, you’d drop 1/99, 1/992, 1/299, but not 1/9 or 1/909. Does this series converge or diverge?

Finding a restaurant in a park

[Michael Jackson told me this problem, as a variation of a problem he got from Koen Claessen.]

A park contains paths that intersect at various places. The intersections all have the properties that they are 3-way intersections and that, with one exception, they are indistinguishable from each other. The one exception is an intersection where there is a restaurant. The restaurant is reachable from everywhere in the park. Your task is to find your way to the restaurant.

The park has strict littering regulations, so you are not allowed to modify the paths or intersections (for example, you are not allowed to leave a note an intersection saying you have been there). However, you are allowed to do some bookkeeping on a pad of paper that you bring with you at all times (in the computer-science parlance, you are allowed some state). How can you find the restaurant?

You may assume that once you enter an intersection, you can continue to the left, continue to the right, or return to where you just came from.

[As an alternative puzzle, suppose you must continue through an intersection, turning either left or right, but not turning around to exit the intersection the way you just entered it.]

Opening boxes in a prison courtyard

[I got this problem from Clark Barrett, who got it from Robert Nieuwenhuis. Just when you thought you had heard all variations of prisoners and boxes…]

100 prisoners agree on a strategy before playing the following game: One at a time (in some unspecified order), each of the prisoners is taken to a courtyard where there is a line of 100 boxes. The prisoner gets to make choices to open 50 of the boxes. When a box is opened, it reveals the name of a prisoner (the prisoners have distinct names). The names written in the boxes are in 1-to-1 correspondence with the prisoners; that is, each name is found in exactly one box. If after opening 50 boxes, the prisoner has not found his own name, the game is over and all the prisoners lose. But if the prisoner does find the box that contains his name among the 50 boxes he opens, then the prisoner is taken to the other side of the courtyard where he cannot communicate with the others, the boxes are once again closed, and the next prisoner is brought out into the courtyard. If all prisoners make it to the other side of the courtyard, they win.

One possible strategy is for each prisoner to randomly select 50 boxes and open them. This gives the prisoners 1 chance out of 2100 to win–a slim chance, indeed. But the prisoners can do better, using a strategy that for a random configuration of the boxes will give them a larger chance of winning. How good a strategy can you develop?

Frugal selection of weights to determine the weight of a thing

[Matthew Parkinson told me this problem, or a slight variation thereof.]

You are given a balance (that is, a weighing machine with two trays) and a positive integer N. You are then to request a number of weights. You pick which denominations of weights you want and how many of each you want. After you receive the weights you requested, you are given a thing whose weight is an integer between 1 and N, inclusive. Using the balance and the weights you requested, you must now determine the exact weight of the thing.

As a function of N, how few weights can you get by requesting?

Initializing an array in constant time

[Unlike most problems on this page, this problem requires some computer science knowledge. Many years ago, I read a solution to this problem in one of Donald Knuth’s books (I think). The algorithm intrigued me and stuck in my mind.]

Consider the following array operations. Init(N,d) initializes an array of N elements so that each element has value d. Once Init has been called, the following two operations can be applied: For any i such that 0 < = i < N, Get(i) returns the array element at position i and Set(i,v) sets the array element at position i to the value v.

Given any amount of memory you want, implement the three operations so that each operation has an O(1) time complexity.

Translation error in a cookbook

[This problem is a bit fuzzier than most on this page, just because I don’t know for sure that the cookbook publisher made a translation error. But I hope you’ll still enjoy the problem.]

Recently, I received a wonderful cookbook. In an appendix, it shows a table that converts oven temperatures between Celsius and Fahrenheit. (Side remark: Approximate oven temperatures are actually really simple to convert in your head–just double the number of degrees Celsius to get the number of degrees Fahrenheit. For oven temperatures, this will be within 10 F of the exact answer.)

The table has a footnote that says “If your oven has a fan, reduce the recipe temperature by 68 F”. I have a strong hunch that this footnote suffers from a translation error. How many degrees Fahrenheit should it have said to reduce the temperature by? (No knowledge of convection ovens required.)

Making a square larger

[I got this problem from Radu Grigore.]

You are given four points (on a Euclidian plane) that make up the corners of a square. You may change the positions of the points by a sequence of moves. Each move changes the position of one point, say p, to a new location, say p’, by “skipping over” one of the other 3 points. More precisely, p skips over a point q if it is moved to the diametrically opposed side of q. In other words, a move from p to p’ is allowed if there exists a point q such that q = (p + p’) / 2.

Find a sequence of moves that results in a larger square. Or, if no such sequence is possible, give a proof of why it isn’t possible. (The new square need not be oriented the same way as the original square. For example, the larger square may be turned 45 degrees from the original, and the larger square may have the points in a different order from in the original square.)

Catching a spy

[I got this problem from Radu Grigore.]

A spy is located on a one-dimensional line. At time 0, the spy is at location A. With each time interval, the spy moves B units to the right (if B is negative, the spy is moving left). A and B are fixed integers, but they are unknown to you. You are to catch the spy. The means by which you can attempt to do that is: at each time interval (starting at time 0), you can choose a location on the line and ask whether or not the spy is currently at that location. That is, you will ask a question like “Is the spy currently at location 27?” and you will get a yes/no answer. Devise an algorithm that will eventually find the spy.

Average clan size

[I got this problem from Ernie Cohen, who I think had made it up. Itay Neeman suggested the use of “clans” instead of Ernie’s original “families”, because “clans” has a stronger connotation of the groups being disjoint.]

The people in a country are partitioned into clans. In order to estimate the average size of a clan, a survey is conducted where 1000 randomly selected people are asked to state the size of the clan to which they belong. How does one compute an estimate average clan size from the data collected?

Colored balls in boxes

[I got this little problem from Leonardo de Moura.]

There are three boxes, one containing two black balls, another containing two white balls, and another containing one black and one white ball. You select a random ball from a random box and you find you selected a white ball. What is the probability that the other ball in the same box is also white?

Mixed up airplane seats

[I got this problem from Rajeev Joshi, who I think said he heard it from Jay Misra.]

An airplane has 50 seats, and its 50 passengers have their own assigned seats. The first person to enter the plane ignores his seat assignment and instead picks a seat on random. Each subsequent person to enter the plane takes her assigned seat, if available, and otherwise chooses a seat on random. What is the probability that the last passenger gets to sit in her assigned seat?

Multiples in the Fibonacci series

[Carroll Morgan told me this puzzle.]

Prove that for any positive K, every Kth number in the Fibonacci sequence is a multiple of the Kth number in the Fibonacci sequence.

More formally, for any natural number n, let F(n) denote Fibonacci number n. That is, F(0) = 0, F(1) = 1, and F(n+2) = F(n+1) + F(n). Prove that for any positive K and natural n, F(n*K) is a multiple of F(K).

Coins in a line

[Rajeev Joshi told me this problem. He got it from Jay Misra.]

Consider a game that you play against an opponent. In front of you are an even number of coins of possibly different denominations. The coins are arranged in a line. You and your opponent take turns selecting coins. Each player takes one coin per turn and must take it from an end of the line, that is, the current leftmost coin or the current rightmost coin. When all coins have been removed, add the value of the coins collected by each player. It is possible that you and your opponent end up with the same value (for example, if all coins have the same denomination). Develop a strategy where you take the first turn and where your final value is at least that of your opponent (that is, don’t let your opponent end up with coins worth more than your coins).

Determining the number of one hat

[This problem was told to me by Clark Barrett, who got it from his father. It may sound reminiscent of the Three hat colors problem, but it’s different in many ways.]

N people team up and decide on a strategy for playing this game. Then they walk into a room. On entry to the room, each person is given a hat on which one of the first N natural numbers is written. There may be duplicate hat numbers. For example, for N=3, the 3 team members may get hats labeled 2, 0, 2. Each person can see the numbers written on the others’ hats, but does not know the number written on his own hat. Every person then simultaneously guesses the number of his own hat. What strategy can the team follow to make sure that at least one person on the team guesses his hat number correctly?

Voting on how to distribute coins

[This problem was communicated to me by Sophia Drossopoulou.]

100 coins are to be distributed among some number of persons, referred to by the labels A, B, C, D, …. The distribution works as follows. The person with the alphabetically highest label (for example, among 5 people, E) is called the chief. The chief gets to propose a distribution of the coins among the persons (for example, chief E may propose that everyone get 20 coins, or he may propose that he get 100 coins and the others get 0 coins). Everyone (including the chief) gets to vote yes/no on the proposed distribution. If the majority vote is yes, then that’s the final distribution. If there’s a tie (which there could be if the number of persons is even), then the chief gets to break the tie. If the majority vote is no, then the chief gets 0 coins and has to leave the game, the person with the alphabetically next-highest name becomes the new chief, and the process to distribute the 100 coins is repeated among the persons that remain. Suppose there are 5 persons and that every person wants to maximize the number of coins that are distributed to them. Then, what distribution should chief E propose?

[This problem and its solution caused my niece Sarah Brown to send me the following article from The Economist, which considers a human aspect of situations like these.]

Subsequence of coin tosses

[I got this problem from Joe Morris, who created it.]

Each of two players picks a different sequence of two coin tosses. That is, each player gets to pick among HH, HT, TH, and TT. Then, a coin is flipped repeatedly and the first player to see his sequence appear wins. For example, if one player picks HH, the other picks TT, and the coin produces a sequence that starts H, T, H, T, T, then the player who picked TT wins. The coin is biased, with H having a 2/3 probability and T having a 1/3 probability. If you played this game, would you want to pick your sequence first or second?

Children and light switches

[I got this problem from Mariela Pavlova.]

A room has 100 light switches, numbered by the positive integers 1 through 100. There are also 100 children, numbered by the positive integers 1 through 100. Initially, the switches are all off. Each child k enters the room and changes the position of every light switch n such that n is a multiple of k. That is, child 1 changes all the switches, child 2 changes switches 2, 4, 6, 8, …, child 3 changes switches 3, 6, 9, 12, …, etc., and child 100 changes only light switch 100. When all the children have gone through the room, how many of the light switches are on?

Finding a counterfeit coin

[Ernie Cohen sent me this puzzle, and I also heard it from a student who got it from Ernie at Marktoberdorf.]

You have 12 coins, 11 of which are the same weight and one counterfeit coin which has a different weight from the others. You have a balance that in each weighing tells you whether the two sides are of equal weight, or which side weighs more. How many weighings do you need to determine: which is the counterfeit coin, and whether it weighs more or less than the other coins. How?

Cutting cheese

[I got this problem many years ago, likely from Jan van de Snepscheut.]

You’re given a 3x3x3 cube of cheese and a knife. How many straight cuts with the knife do you need in order to divide the cheese up into 27 1x1x1 cubes?

Fair soccer championship

[I got this question from Sergei Vorobyov.]

The games played in the soccer world championship form a binary tree, where only the winner of each game moves up the tree (ignoring the initial games, where the teams are placed into groups of 4, 2 of which of which go onto play in the tree of games I just described). Assuming that the teams can be totally ordered in terms of how good they are, the winner of the championship will indeed be the best of all of the teams. However, the second best team does not necessarily get a second place in the championship. How many additional games need to be played in order to determine the second best team?

Path on the surface of the Earth

[I must have heard this problem ages ago, but as I remembered it, one was always satisfied after finding just one solution. It was a math professor at the Kaiserslautern Technical University who brought asking for all solutions to my attention.]

Initially, you’re somewhere on the surface of the Earth. You travel one kilometer South, then one kilometer East, then one kilometer North. You then find yourself back at the initial position. Describe all initial locations from which this is possible.

Random point in a circle

[I heard this nice problem from Sumit Gulwani.]

You’re given a procedure that with a uniform probability distribution outputs random numbers between 0 and 1 (to some sufficiently high degree of precision, with which we need not concern ourselves in this puzzle). Using a bounded number of calls to this procedure, construct a procedure that with a uniform probability distribution outputs a random point within the unit circle.

Mixing vinegar and oil

[I read this problem in a puzzle book I have.]

You have two jars. One contains vinegar, the other oil. The two jars contain the same amount of their respective fluid.

Take a spoonful of the vinegar and transfer it to the jar of oil. Then, take a spoonful of liquid from the oil jar and transfer it to the vinegar jar. Stir. Now, how does the dilution of vinegar in the vinegar jar compare to the dilution of oil in the oil jar?

Psycho killer

[I got this problem from Carroll Morgan.]

A building has 16 rooms, arranged in a 4×4 grid. There is a door between every pair of adjacent rooms (“adjacent” meaning north, south, west, and east, but no diagonals). Only the room in the northeast corner has a door that leads out of the building.

In the initial configuration, there is one person in each room. The person in the southwest corner is a psycho killer. The psycho killer has the following traits: If he enters a room where there is another person, he immediately kills that person . But he also cannot stand the site of blood, so he will not enter any room where there is a dead person.

As it happened, from that initial configuration, the psycho killer managed to get out of the building after killing all the other 15 people. What path did he take?

A special squarish age

[Chuck Chan created this little puzzle. Greg Nelson suggested introducing the name “squarish” in order to simplify the problem statement.]

Let’s say that a number is squarish if it is the product of two consecutive numbers. For example, 6 is squarish, because it is 2*3.

A friend of mine at Microsoft recently had a birthday. He said his age is now squarish. Moreover, since the previous time his age was a squarish number, a squarish number of years has passed. How many years would he have to wait until his age would have this property again?

Passing alternating numbers of coins around

[This problem appears as a sample question on the web page for the Putnam exam.]

A game is played as follows. N people are sitting around a table, each with one penny. One person begins the game, takes one of his pennies (at this time, he happens to have exactly one penny) and passes it to the person to his left. That second person then takes two pennies and passes them to the next person on the left. The third person passes one penny, the fourth passes two, and so on, alternating passing one and two pennies to the next person. Whenever a person runs out of pennies, he is out of the game and has to leave the table. The game then continues with the remaining people.

A game is terminating if and only if it ends with just one person sitting at the table (holding all N pennies). Show that there exists an infinite set of numbers for which the game is terminating.

The exact batting average

[I heard this problem from Bertrand Meyer, who had heard it was once given on the Putnam exam.]

At some point during a baseball season, a player has a batting average of less than 80%. Later during the season, his average exceeds 80%. Prove that at some point, his batting average was exactly 80%.

Also, for which numbers other than 80% does this property hold?

Summing pairs of numbers to primes

[I got this problem from Jay Misra, who got it from Gerard Huet.]

For any even number N, partition the integers from 1 to N into pairs such that the sum of the two numbers in each pair is a prime number.

Hint: Chebyshev proved that the following property (Bertrand’s Postulate) holds: for any k > 1, there exists a prime number p in the range k < p < 2*k.

Right triangle with a 23

[Madan Musuvathi asked me this question.]

Find two positive integers that together with 23 are the lengths of a right triangle.

[Madan first told me 17, which I could solve right away, because I had just finished reading Mark Haddon’s novel The curious incident of the dog in the night-time, which toward the end mentions that a triangle with sides n2+1, n2-1, and 2*n, where n>1, is a right triangle. Madan then asked me about 23.]

[A follow-up question.]

There’s a simple technique that, given any odd positive integer, allows you to figure out the other two integer sides of a right triangle in your head (or with pen and paper if the numbers get too large). Find this technique.

Hint: Think of every number as a multiset of prime factors, so that multiplying the prime factors gives you the number. Move one of the addends of the Pythagorean Theorem to the other side and factor it (a technique I recently learned from Raymond Boute).

The worm and the rubber band

[Jay Misra told me this problem.]

A rubber band (well, a rubber string, really) is 10 meters long. There’s a worm that starts at one end and crawls toward the other end, at a speed of 1 meter per hour. After each hour that passes, the rubber string is stretched so as to become 1 meter longer than it just was. Will the worm ever reach the other end of the string?

Placing coins on a table

[I got this problem from Amit Rao.]

Two players are playing a game. The game board is a circular table. The players have access to an ample supply of equal-sized circular coins. The players alternate turns, with each turn adding a single coin to the table. The coins are not allowed to overlap. Once a coin is placed on the table, it is not allowed to be moved. The player who has no place to put his next coin loses. Develop a winning strategy for the player who starts. (The table is large enough to accommodate at least one coin.)

Determining a hidden digit

[I got this problem from Olean Brown, who had pointed me to the following web page that claims to read your mind.]

Think of a positive integer, call it X. Shuffle the decimal digits of X, call the resulting number Y. Subtract the smaller of X,Y from the larger, call the difference D. D has the following property: Any non-zero decimal digit of D can be determined from the remaining digits. That is, if you ask someone to hide any one of the non-zero digits in the decimal representation of D, then you can try to impress the other person by figuring out the hidden digit from the remaining digits. How is this done? Why does it work?

Boris and Natasha

[I got this problem from Todd Proebsting.]

Boris and Natasha live in different cities in a country with a corrupt postal service. Every box sent by mail is opened by the postal service, the contents stolen, and the box never delivered. Except: if the box is locked, then the postal service won’t bother trying to open it (since there are so many other boxes whose contents are so much easier to steal) and the box is delivered unharmed.

Boris and Natasha each has a large supply of boxes of different sizes, each capable of being locked by padlocks. Also, Boris and Natasha each has a large supply of padlocks with matching keys. The padlocks have unique keys. Finally, Boris has a ring that he would like to send to Natasha. How can Boris send the ring to Natasha so that she can wear it (without either of them destroying any locks or boxes)?

Burning ropes to measure time

[I first got this problem from Ernie Cohen. Apparently, it has appeared as a Car Talk Puzzler, but I’ve been unable to find it on their web site.]

Warm-up: You are given a box of matches and a piece of rope. The rope burns at the rate of one rope per hour, but it may not burn uniformly. For example, if you light the rope at one end, it will take exactly 60 minutes before the entire rope has burnt up, but it may be that the first 1/10 of the rope takes 50 minutes to burn and that the remaining 9/10 of the rope takes only 10 minutes to burn. How can you measure a period of exactly 30 minutes? You can choose the starting time. More precisely, given the matches and the rope, you are to say the words “start” and “done” exactly 30 minutes apart.

The actual problem: Given a box of matches and two such ropes, not necessarily identical, measure a period of 15 minutes.

Flipping cards

[I have heard several versions of this problem. I first heard it from Bertrand Meyer, who got the problem from Yuri Gurevich.]

You’re given a regular deck of 52 playing cards. In the pile you’re given, 13 cards face up and the rest face down. You are to separate the given cards into two piles, such that the number of face-up cards in each pile is the same. In separating the cards, you’re allowed to flip cards over. The catch: you have to do this in a dark room where you cannot determine whether a card is face up or face down.

Three hat colors

[I think I got this puzzle from Lyle Ramshaw, who I think got it from some collection of problems or maybe the American Mathematical Monthly.]

A team of three people decide on a strategy for playing the following game. Each player walks into a room. On the way in, a fair coin is tossed for each player, deciding that player’s hat color, either red or blue. Each player can see the hat colors of the other two players, but cannot see her own hat color. After inspecting each other’s hat colors, each player decides on a response, one of: “I have a red hat”, “I had a blue hat”, or “I pass”. The responses are recorded, but the responses are not shared until every player has recorded her response. The team wins if at least one player responds with a color and every color response correctly describes the hat color of the player making the response. In other words, the team loses if either everyone responds with “I pass” or someone responds with a color that is different from her hat color.

What strategy should one use to maximize the team’s expected chance of winning?

For example, one possible strategy is to single out one of the three players. This player will respond “I have a red hat” and the others will respond “I pass”. The expected chance of winning with this strategy is 50%. Can you do better? Provide a better strategy or prove that no better strategy exists.

[Here’s a related problem, which I got from Jim Saxe.]

In this variation, the responses are different. Instead of “red”, “blue”, “pass”, a response is now an integer, indicating a bet on having the hat color red. Once the responses have been collected, the team’s score is calculated as follows: Add the integer responses for those players wearing red hats, and subtract from that the integers of those players wearing blue hats. For example, if the three players respond with 12, -2, -100 while wearing blue, red, blue, respectively, then the team’s score is (-2) – (12) – (-100) = 90. The team wins if and only if its score is strictly positive.

For example, any strategy used in the first game can be used with this second game by replacing “I have a red hat” with 1, “I have a blue hat” with -1, and “I pass with 0”. Such a strategy wins anytime the strategy would have produced a win in the first game; plus, this strategy may win in some cases where the strategy would not produce a win in the first game. For example, for hat colors red, red, red, the strategy “red”, “red”, “blue” loses in the first game, whereas 1, 1, -1 still wins in the second game. Hence, playing this second game can only increase the team’s expected chance of winning.

[Further generalizations.]

Of course, you can generalize these two problems from 3 players to N players. The solution to the first problem with N players may require more mathematical sophistication than the solution to the second problem with N players.

The line of persons with hats

[Ernie Cohen told me this problem.]

100 persons are standing in line, each facing the same way. Each person is wearing a hat, either red or blue, but the hat color is not known to the person wearing the hat. In fact, a person knows the hat color only of those persons standing ahead of him in line.

Starting from the back of the line (that is, with the person who can see the hat colors of all of other 99 persons), in order, and ending with the person at the head of the line (that is, with the person who can see the hat color of no one), each person exclaims either “red” or “blue”. These exclamations can be heard by all. Once everyone has spoken, a score is calculated, equal to the number of persons whose exclamation accurately describes their own hat color.

What strategy should the 100 persons use in order to get as high a score as possible, regardless of how the hat colors are assigned? (That is, what strategy achieves the best worst-case score?)

For example, if everyone exclaims “red”, the worst-case score is 0. If the first 99 persons exclaim the color of the hat of the person at the head of the line and the person at the head of the line then exclaims the color he has heard, the worst-case score is 1. If every other person exclaims the hat color of the person immediate in front and that person then repeats the color he has just heard, then the worst-case score is 50. Can you do better?

[Here’s a generalization of the problem.]

Instead of using just red and blue as the possible hat colors and exclamations, use N different colors.

The prisoners and the switch

[Tom Ball told me (a close variation of) this problem. The problem has been featured as a Car Talk Puzzler under the name Prison Switcharoo (beware: the Car Talk problem page also contains an answer).]

N prisoners get together to decide on a strategy. Then, each prisoner is taken to his own isolated cell. A prison guard goes to a cell and takes its prisoner to a room where there is a switch. The switch can either be up or down. The prisoner is allowed to inspect the state of the switch and then has the option of flicking the switch. The prisoner is then taken back to his cell. The prison guard repeats this process infinitely often, each time choosing fairly among the prisoners. That is, the prison guard will choose each prisoner infinitely often.

At any time, any prisoner can exclaim “Now, every prisoner has been in the room with the switch”. If, at that time, the statement is correct, all prisoners are set free; if the statement is not correct, all prisoners are immediately executed. What strategy should the prisoners use to ensure their eventual freedom?

(Just in case there’s any confusion: The initial state of the switch is unknown to the prisoners. The state of the switch is changed only by the prisoners.)

As a warm-up, you may consider the same problem but with a known initial state of the switch.

Table with four coins

[This problem has crossed the desk of Jan van de Snepscheut, but it may have been due to someone else.]

A square table has a coin at each corner. Design an execution sequence, each of whose steps consists of one of the following operations:

  • ONE: The operation chooses a coin (possibly a different one with each execution of the operation) and flips it.
  • SIDE: The operation chooses a side of the table and flips the two coins along that side.
  • DIAG: The operation chooses a diagonal of the table and flips the two coins along that diagonal.

such that at some point during the execution (not necessarily at the end), a state where all coins are turned the same way (all heads or all tails) obtains.

Stabilizing nodes from an anchor

[I got this problem from Jay Misra, who had received it from Edsger Dijkstra. This particular description of the problem borrows from a description given by Michael Jackson.]

In a finite, undirected, connected graph, an integer variable v(n) is associated with each node n. One node is distinguished as the anchor. An operation OP(n) is defined on nodes:

OP(n):if node n is the anchor, then do nothing,else set v(n) to the value 1 + min{v(m)}, where m ranges over all neighbors of n that are distinct from n.

An infinite sequence of operations n),OP(m), …> is executed, the node arguments n, m, … for the operations being chosen arbitrarily and not necessarily fairly. Show that eventually all v(n) stabilize. That is, that after some finite prefix of the infinite sequence of operations, no further operation changes v(n) for any node n.

Points on a circle

[This problem was told to me by Dave Detlefs, who got it from the following impressive collection of math problems.]

Given N points randomly distributed around the circumference of a circle, what is the probability that all N points lie on the same semi-circle?

The electrician problem

[I learned about this problem from Greg Nelson, who phrased the problem in terms of a tall building and elevator rides. Here, I instead say a mountain and helicopter rides, which is the way Lyle Ramshaw had heard the problem and which more forcefully emphasizes the price of each ride. As a computer scientist, I like this problem a lot, because of the variety of solutions of different computational complexities.]

You’re an electrician working at a mountain. There are N wires running from one side of the mountain to the other. The problem is that the wires are not labeled, so you just see N wire ends on each side of the mountain. Your job is to match these ends (say, by labeling the two ends of eachwire in the same way).

In order to figure out the matching, you can twist together wire ends, thus electrically connecting the wires. You can twist as many wire ends as you want, into as many clusters as you want, at the side of the mountain where you happen to be at the time. You can also untwist the wire ends at the side of the mountain where you’re at. You are equipped with an Ohm meter, which lets you test the connectivity of any pair of wires. (Actually, it’s an abstract Ohm meter, in that it only tells you whether or not two things are connected, not the exact resistance.)

You are not charged [no pun intended] for twisting, untwisting, and using the Ohm meter. You are only charged for each helicopter ride you make from one side of the mountain to the other. What is the best way to match the wires? (Oh, N>2, for there is no solution when N=2.)

The hidden card

[I learned about this problem from Lyle Ramshaw. See also puzzles 19 and 20 on the following large collection of mathematical puzzles.]

In this problem, you and a partner are to come up with a scheme for communicating the value of a hidden card. The game is played as follows:

  • Your partner is sent out of the room.
  • A dealer hands you 5 cards from a standard 52 card deck.
  • You look at the cards, and hand them back to the dealer, one by one, in whatever order you choose.
  • The dealer takes the first card that you hand her and places it, face up, in a spot labeled “0”‘. The next three cards that you hand her, she places, similarly, in spots labeled “1”, “2”, and “3”. The last card that you hand her goes, face down, in a spot labeled “hidden”. (While you control the order of the cards, you have no control over their orientations, sitting in their spots; so you can’t use orientation to transmit information to your partner.)
  • Your partner enters the room, looks at the four face-up cards and the spots in which they lie and, from that information (and your previously-agreed-upon game plan), determines the suit and value of the hidden card.

Question: What is the foolproof scheme that you and your partner settled on ahead of time?

As a follow-up question, consider the same problem but with a 124-card deck.

Knight, knave, commoner

[Communicated to me by Carroll Morgan.]

A king has a daughter and wants to choose the man she will marry. There are three suitors from whom to choose, a Knight, a Knave, and a Commoner. The king wants to avoid choosing the Commoner as the bridegroom, but he does not know which man is which. All the king knows is that the Knight always speaks the truth, the Knave always lies, and the Commoner can do either. The king will ask each man one yes/no question, and will then choose who gets to marry the princess. What question should the king ask and how should he choose the bridegroom?

[A follow-up question posed by Lyle Ramshaw.]

Suppose the three suitors know each other (an assumption that’s not needed in the original problem). Then find a new strategy for the king where the king only needs to ask a question of any two of the three suitors in order to pick the bridegroom.

[Another variation of the problem.]

Find a strategy for the king where the king can ask questions of only one suitor, but can ask two questions of that suitor.

[And another (at first sight incredible) follow-up question communicated to me by both Jim Saxe and Pierre Nallet.]

Find a strategy for the king where the king can ask only one yes/no question and only of one suitor.

IFIP WG 2.3

ifip-wg-2-3IFIP Working Group 2.3 Programming Methodology

IFIP WG 2.3 “Programming Methodology” is one of the working groups of IFIP Technical Committee 2 (Software: Theory and Practice).

Aim

To increase programmers’ ability to compose programs.

Scope

  1. Identification of sources of difficulties encountered in present day programming;
  2. the interdependence between the formulation of problems and the formulation of programs, and the mapping of relations existing in the world of problems into the relations among programs and their components;
  3. intellectual disciplines and problem-solving techniques that can aid programmers in the composition of programs;
  4. the problem of achieving program reliability;
  5. the consequences of requirements for program adaptability;
  6. the problem of provability of program correctness and its influence on the structure of programs and on the process of their composition;
  7. guidelines of partitioning large programming tasks and defining the interfaces between the parts;
  8. software for mechanized assistance to program composition.

News and Honors

News

  • Greg Nelson received the Herbrand Award, 2013.
  • Rustan Leino received the IFIP Silver Core award, 2010.
  • Tony Hoare received the IEEE Von Neumann medal, 2010.
  • Bertrand Meyer received the prestigious 2010 IEEE Computer Society Harlan Mills Award.
  • N. Shankar promoted to SRI Fellow. [2010]
  • Pamela Zave promoted to AT&T Fellow, “for groundbreaking use of formal methods in AT&T’s telecommunications and IP services and for enduring contributions to software theory.” [2009]
  • Bertrand Meyer elected IFIP Technical Committee 2 chair.  [April 2009]
  • Manfred Broy receives the Konrad Zuse Medal from the German Informatics Society, the most prestigious award in informatics in Germany.
  • IFIP WG 2.3 member Bertrand Meyer wins the prestigious ACM Software System Award for the development of the Eiffel.  With this award, ACM honors “an institution or individual(s) recognized for developing a software system that has had a lasting influence”, see the ACM Awards Program. Here is the ACM press release [March 2007].

(Sad) News

  • IFIP WG 2.3 founding member Doug T. Ross died on January 31, 2007.

Some remembrances of Doug Ross

Of Lexington, 77, January 31, from complications of a fall. Beloved husband of Patricia M. Ross.  Loving father of Jane L. Ross of Brookline, Kathryn R. Chow and her husband Henry R. Smedley of New York City, and Margaret R. Thrasher of Durham NH, and three grandchildren: Karen, Nicholas, and Bethany Thrasher.  Doug is survived by two sisters, Margaret J. Hastings and her husband James B. Hastings of Princeton NJ and Frances R. Grimm and her husband Robert J. Grimm of Portland OR.  As Head of the Computer Application Group at the MIT Electronic Systems Laboratory, Doug led the development of the Automatically Programmed Tool Language (APT), a special purpose programming language that became the world standard for programming computer-controlled machine tools.  He then turned his attention to the development of a software engineering methodology and supporting tools.  This led to the development while at MIT of the first software engineering language and supporting tools, the AED system.  In 1969 Doug founded SofTech, Inc. where he continued to work on software engineering standards.  While at SofTech, Doug conceived of SA, a graphic notation and methodology for system description.  SA has been successfully applied worldwide as SofTechs Structured Analysis and Design Technique (SADT) or as the U.S. government standard IDEF0.  Memorial Service with reception at Hancock United Church of Christ, Congregational, 1912 Massachusetts Ave., Lexington at 2:00 PM Sun., February 11.

–from Death Notices, the Boston Globe

Here some views about Doug.  For me, he has been an important pioneer in crucial areas throughout his career. Here are two examples:

  • In programming languages, the elaboration of new data structures, which became later known as records; cf. the plexes of the AED language in the fifties.
  • In large-scale system design, the systematic use of refinement into successive abstraction levels; cf. his well-known Structured Analysis and Design Technique (SADT) method in the sixties, and the company SofTech (a nice name) he founded.

Later, Doug became more and more interested in epistemological, philosophical and logic-related studies.  It is possible his work in that direction became too pioneering or too advanced for his colleagues, including us.  Who knows, the future may prove him right.  At any rate, his reflections regularly made me think.

Meetings

Meetings

IFIP Working Group 2.3 meets about once every 9 months.  Meetings often alternate between Europe and North America.

  • Meeting 55, Orlando, Florida, USA, 19-23 May 2014
  • Meeting 54, St. Petersburg, Russia, 3-7 June 2013
  • Meeting 53, Kirkland, WA, USA, 16-20 July 2012
  • Meeting 52, Winchester, UK, 19-23 September 2011
  • Meeting 51, Santa Barbara, CA, 17-21 January 2011
  • Meeting 50, Lachen, Switzerland, 1-5 March 2010
  • Meeting 49, MIT, Boston, MA, USA, 8-12 June 2009.
  • Meeting 48, Cambridge, England, 21-25 July 2008.
  • Meeting 47, Santa Fe, NM, USA, 8-12 October 2007.
  • Meeting 46, Sydney, Australia, 8-12 January 2007.
  • Meeting 45, Bruges, Belgium, 13-17 March 2006.
  • Meeting 44, Niagara Falls, 6-10 June 2005.
  • Meeting 43, Prato, Italy, 6-10 September 2004.
  • Meeting 42, Philadelphia, PA, USA, 5-9 January 2004.
  • Meeting 41, Biarritz, France, 24-28 March 2003.
  • Meeting 40, Turku, Finland, 12-16 August 2002.
  • Meeting 39, Hanover, NH, USA, 2-6 October 2001.
  • Meeting 38, Santa Cruz, CA, USA, 8-12 January 2001.
  • Meeting 37, Longhorseley, UK, 3-7 April 2000.
  • Meeting 36, Munich, Germany, 21-25 June 1999.
  • Meetting 35, Bloomington, IN, USA, 1-5 June 1998.
  • Meeting 34, Alsace, France, September 1997.
  • Meeting 33, Napa Valley, CA, January 1997.
  • Meeting 32, Han-sur-Lesse, Belgium, April 1996.
  • Meeting 31, Ithaca, NY, USA, July 1995.
  • Meeting 30, Ispra, Italy, June 1994.
  • Meeting 29, Lake Simcoe, ON, Canada, May 1993.
  • Meeting 28, New Forest, July 1992.
  • Meeting 27, Pouilly-en-Auxois, France, September 1991.
  • Meeting 26, Santa Catalina Island, CA, USA, December 1990.
  • Meeting 25, Munich, Germany, March 1990.
  • Meeting 24, Zaborów, Poland, June 1989.
  • Meeting 23, Pittsburg, PA, USA, August 1988.
  • Meeting 22, Habay-la-Neuve, Belgium, November 1987.
  • Meeting 21, Manchester, UK, April 1985.
  • Meeting 20, Victoria, BC, Canada, July 1984.
  • Meeting 19, Pont-à-Mousson, France, September 1983.
  • Meeting 18, New Paltz, NY, USA, September 1982.
  • Meeting 17, Sintra, Portugal, October 1981.
  • Meeting 16, Han-sur-Lesse, Belgium, January 1981.
  • Meeting 15, Kazimierz Dolny, Poland, April 1980.
  • Meeting 14, Santa Cruz, CA, USA, August 1979.
  • Meeting 13, Warwick, UK, April 1978.
  • Meeting 12, Niagara-on-the-Lake, ON, Canada, August 1977.
  • Meeting 11, St. Pierre de Chartruese, France, December 1976.
  • Meeting 10, Cazenovia, IL, USA, July 1976.
  • Meeting 9, Baden bei Wien, Austria, September 1975.
  • Meeting 8, Munich, Germany, December 1974.
  • Meeting 7, Boldern, Switzerland, April 1974.
  • Meeting 6, Blanchland, UK, October 1973.
  • Meeting 5, Munich, Germany, April 1973.
  • Meeting 4, Warsaw, Poland, September 1972.
  • Meeting 3, Bristol, UK, January 1972.
  • Meeting 2, Warwick, UK, April 1971.
  • Meeting 1, Copenhagen, Denmark, March 1970.
  • Meeting 0, Oslo, Norway, July 1969.

Members

Links

Links

CV

Research Interests

My research centers around tools for software engineers, including programming languages, programming systems, program verification, and program design technologies.

Research Projects

DafnyDafny is a programming language designed with verification in mind, and its compiler includes a state-of-the-art program verifier.  The language offers forms of both imperative and functional programming and can also be used to express some mathematics.  The verifier runs in the background of the development environment.  Dafny has been used to verify challenging algorithms, is used in teaching at several universities, and has been used by award-winning teams at program verification competitions.  Dafny excels at providing an accessible integrated verification experience. Joint work with Reza Ahmadi, Nada Amin, Chris Hawblitzel, Jason Koenig, Jay R. Lorch, Dan Matichuk, Michał Moskal, Peter Müller, Clément Pit–Claudel, Bryan Parno, Nadia Polikarpova, Tiark Rompf, Dan Rosén, Valentin Wüstholz, and others. 2008-present.
JennisysJennisys (“this is where programs begin”) is a program synthesizer. Joint work with Aleksandar Milicevic. 2011-2012.
ChaliceChalice is an experimental language for concurrency.  Its specifications are based on Implicit Dynamic Frames with fractional permissions. Joint work with Stefan Heule, Peter Müller, Jan Smans, Alex J. Summers, Kuat Yessenov, and others. 2009-present.
BoogieBoogie is an Intermediate Verification Language and a verification engine for that language.  It is used by more than a dozen verifiers for different languages. Joint work with Mike Barnett, Sascha Böhme, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, Michał Moskal, Shaz Qadeer, Philipp Rümmer, and others. 2003-present.
Spec#Spec# is a superset of the language C# 2.0, adding contracts and non-null types.  It includes a static verifier for the contracts. Joint work with Mike Barnett, Ádám Darvas, Manuel Fähndrich, Bart Jacobs, Ronald Middelkoop, Peter Müller, Wolfram Schulte, Herman Venter, Angela Wallenburg, and others. 2003-2009.
HoudiniHoudini is a specification wizard, originally for ESC/Java.  The technique infers specifications by guessing candidate specifications and then running an underlying checker to refute bad guesses. Joint work with Cormac Flanagan, Rajeev Joshi, Michael Y. Levin, and others. 1999-2001.
ESC/JavaESC/Java (which won the Most Influential 2002 PLDI Paper award) is a formal-methods based tool for statically finding software defects in Java programs. Joint work with Cormac Flanagan, Gary T. Leavens, Mark Lillibridge, Todd Millstein, Greg Nelson, James B. Saxe, Raymie Stata, and others. 1997-2001.
ESC/Modula-3ESC is the original Extended Static Checker for the Modula-3 language. Joint work with David L. Detlefs, Greg Nelson, and James B. Saxe. 1994-1996.
Modula-3DA variant of the Modula-3 language for programming multicomputers. 1992-1993.

Education

PhDComputer Science, California Institute of Technology, 1995. Advisor:  Prof. Dr. K. Mani Chandy
MSComputer Science, California Institute of Technology, 1993. Advisor:  Prof. Dr. Jan L. A. van de Snepscheut
BAwith Special Honors in Computer Science, The University of Texas at Austin, 1989. Honors research advisor:  Prof. Dr. Louis E. Rosier

Employment

Microsoft Redmond, WA, USAPrincipal Researcher (2007-present) Senior Researcher (2006-2007) Researcher (2001-2006) Software design engineer, technical lead (1989-1991)
Imperial College London London, UKVisiting Professor (honorary post, 2012-present)
DEC/Compaq Systems Research Center Palo Alto, CA, USAComputer science researcher (Jan 1995-Nov 2001) Research intern (summer 1994) Research intern (summer 1992)
Caltech Pasadena, CA, USACo-instructor, Mathematics of Program Construction (Fall 1994) Co-instructor, Mathematics of Program Construction (Spring 1994) Teaching assistant, Computation, Computers, Programs (Fall 1991-Spring 1994) Graduate research assistant (Fall 1991-Fall 1994)
CompuGuide Austin, TX, USAPresident, consultant (Feb 1988-May 1989)
UT Austin Informal Classes Austin, TX, USAInstructor of various computer classes (Sep 1987-May 1989)
One-Eleven, Inc. Austin, TX, USAProgrammer (Aug 1987-May 1989)

Publications

Quicksort Revisited—Verifying Alternative Versions of QuicksortTPFM 2016
Razvan Certezeanu, Sophia Drossopoulou, Benjamin Egelund-Muller, K. Rustan M. Leino, Sinduran Sivarajan, and Mark Wheelhouse
In Erika Ábrahám, Marcello M. Bonsangue, and Einar Broch Johnsen, editors, Theory and Practice of Formal Methods—Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday, pages 407-426.  Springer, 2016.
Trigger Selection Strategies to Stabilize Program VerifiersCAV 2016
K. Rustan M. Leino and Clément Pit-Claudel
In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification—28th International Conference, CAV 2016, volume 9779 of Lecture Notes in Computer Science, pages 361-381.  Springer, July 2016.
Integrated Environment for Diagnosing Verification ErrorsTACAS 2016
Maria Christakis, K. Rustan M. Leino, Peter Müller, and Valentin Wüstholz
In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems—22nd International Conference, TACAS 2016, volume 9636 of Lecture Notes in Computer Science, pages 424-441.  Springer, April 2016.
Verification, Model Checking, and Abstract Interpretation—17th International Conference, VMCAI 2016LNCS (VMCAI 2016)
Barbara Jobstmann and K. Rustan M. Leino
Volume 9583 of Lecture Notes in Computer Science.  Springer, January 2016.
An Assertional Proof of the Stability and Correctness of Natural MergesortACM Comp. Logic
K. Rustan M. Leino and Paqui Lucio
ACM Transactions on Computational Logic, 17(1): 6, December 2015. 
Fine-Grained Caching of Verification ResultsCAV 2015
K. Rustan M. Leino and Valentin Wüstholz
In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification—27th International Conference, CAV 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 380-397.  Springer, July 2015.
Automatic verification of Dafny programs with traitsFTfJP@ECOOP 2015
Reza Ahmadi, K. Rustan M. Leino, and Jyrki Nummenmaa
In Rosemary Monahan, editor, Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015, pages 4:1-4:5.  ACM, 2015.
Compiling Hilbert’s epsilon operatorLPAR short papers 2015
K. Rustan M. Leino
In Ansgar Fehnker, Annabelle McIver, Geoff Sutcliffe, and Andrei Voronkov, editors, 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning—Short Presentations, LPAR 2015, volume 35 of EPiC Series in Computing, pages 106-118.  EasyChair, 2015.
Programming Language Features for RefinementRefine@FM 2015
Jason Koenig and K. Rustan M. Leino
In John Derrick, Eerke A. Boiten, and Steve Reeves, editors, Proceedings 17th International Workshop on Refinement, Refine@FM 2015, volume 209 of Electronic Proceedings in Theoretical Computer Science, pages 87-106.  2016.
Co-induction simply—Automatic Co-inductive Proofs in a Program VerifierFM 2014
K. Rustan M. Leino and Michał Moskal
In Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: 19th International Symposium on Formal Methods, volume 8442 of Lecture Notes in Computer Science, pages 382-398.  Springer, May 2014.
Formalizing and Verifying a Modern Build LanguageFM 2014
Maria Christakis, K. Rustan M. Leino, and Wolfram Schulte
In Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: 19th International Symposium on Formal Methods, volume 8442 of Lecture Notes in Computer Science, pages 643-657.  Springer, May 2014.
Computing with an SMT SolverTAP 2014
Nada Amin, K. Rustan M. Leino, and Tiark Rompf
In Martina Seidl and Nikolai Tillmann, editors, Tests and Proofs—8th International Conference, TAP 2014, volume 8570 of Lecture Notes in Computer Science, pages 20-35.  Springer, July 2014.
The Dafny Integrated Development EnvironmentF-IDE 2014
K. Rustan M. Leino and Valentin Wüstholz
In Catherine Dubois, Dimitra Giannakopoulou, and Dominique Méry, editors, 1st Workshop on Formal-IDE, volume 149 of Electronic Proceedings in Theoretical Computer Science.  April 2014.
Automating Theorem Proving with SMTITP 2013
K. Rustan M. Leino
In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, 4th International Conference, ITP 2013, volume 7998 of Lecture Notes in Computer Science, pages 2-16.  Springer, July 2013.
Developing Verified Programs with DafnyICSE 2013
K. Rustan M. Leino
In David Notkin, Betty H. C. Cheng, and Klaus Pohl, editors, 35th International Conference on Software Engineering, ICSE ’13, pages 1488-1490.  ACM, May 2013.
Verified CalculationsVSTTE 2013
K. Rustan M. Leino and Nadia Polikarpova
In Ernie Cohen and Andrey Rybalchenko, editors, Verified Software: Theories, Tools, Experiments—5th International Conference, VSTTE 2013, Revised Selected Papers, volume 8164 of Lecture Notes in Computer Science, pages 170-190.  Springer, 2014.
Co-induction Simply:  Automatic Co-inductive Proofs in a Program VerifierMSR TR
K. Rustan M. Leino and Michal Moskal
Technical Report MSR-TR-2013-49, Microsoft Research, May 2013.
Tools for Software Verification:  special section from the Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of SystemsSTTT (from TACAS 2011)
Parosh Aziz Abdulla and K. Rustan M. Leino
Software Tools for Technology Transfer, 15(2).  April 2013. 
Abstract Read Permissions: Fractional Permissions without the FractionsVMCAI 2013
Stefan Heule, K. Rustan M. Leino, Peter Müller, and Alexander J. Summers
In Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni, editors, Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, volume 7737 of Lecture Notes in Computer Science, pages 315-334.  Springer, January 2013.
Using Dafny, an Automatic Program VerifierLASER 2011
Luke Herbert, K. Rustan M. Leino, and Jose Quaresma
In Bertrand Meyer and Martin Nordio, editors, Tools for Practical Software Verification, {LASER}, International Summer School 2011, volume 7682 of Lecture Notes in Computer Science, pages 156-181.  Springer, 2012.
Program extrapolation with JennisysOOPSLA 2012
K. Rustan M. Leino and Alexandar Milicevic
In Gary T. Leavens and Matthew B. Dwyer, editors, Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, pages 411-430.  ACM, October 2012.
Stepwise refinement of heap-manipulating code in ChaliceFAC
K. Rustan M. Leino and Kuat Yessenov
Formal Aspects of Computing, 24(4-6): 519-535, July 2012. Celebrating the 60th Birthday of Carroll Morgan. 
Endorsement blurb
K. Rustan M. Leino
On back cover of SPARK – The Proven Approach to High Integrity Software.  John Barnes with Altran Praxis.  Altran Praxis, 2012.
The EventB2Dafny Rodin plug-in TOPI 2012
Néstor Cataño, K. Rustan M. Leino, and Victor Rivera
In 2nd Workshop on Developing Tools as Plug-ins (TOPI), pages 49-54.  IEEE, June 2012.
Behavioral Interface Specification Languages Comp. Surv.
John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, and Matthew Parkinson
ACM Computing Surveys, 44(3): 16, June 2012. 
Special issue:  Selected Papers of the Confrence ‘Tools and Algorithms for the Construction and Analysis of Systems “TACAS” 2011’LMCS (from TACAS 2011)
Parosh Aziz Abdulla and K. Rustan M. Leino
Logical Methods in Computer Science.  DOI: 10.2168/LMCS-TACAS:2011.  2012. http://www.lmcs-online.org/ojs/specialIssues.php?id=40 
Getting Started with Dafny: A GuideMOD 2011
Jason Koenig and K. Rustan M. Leino
In Tobias Nipkow, Orna Grumberg, and Benedikt Hauptmann, editors, Software Safety and Security: Tools for Analysis and Verification.  NATO Science for Peace and Security Series D: Information and Communication Security.  IOS Press, 2012, volume 33, pages 152-181. Marktoberdorf International Summer School 2011 lecture notes.
Automating Induction with an SMT SolverVMCAI 2012
K. Rustan M. Leino
In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation – 13th International Conference, VMCAI 2012, volume 7148 of Lecture Notes in Computer Science, pages 315-331.  Springer, January 2012.
The Boogie Verification Debugger (Tool Paper)SEFM 2011
Claire Le Goues, K. Rustan M. Leino, and Michał Moskal
In Gilles Barthe, Alberto Pardo, and Gerardo Schneider, editors, Software Engineering and Formal Methods – 9th International Conference, SEFM 2011, volume 7041 of Lecture Notes in Computer Science, pages 407-414.  Springer, November 2011.
The 1st Verified Software Competition: Experience ReportFM 2011
Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, and Benjamin Weiβ
In Michael Butler and Wolfram Schulte, editors, FM 2011: Formal Methods – 17th International Symposium on Formal Methods, volume 6664 of Lecture Notes in Computer Science, pages 154-168.  Springer, June 2011. FM 2011 Best Paper Award.
Specification and verification: the Spec# experienceCACM
Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, and Herman Venter
Communications of the ACM, 54(6): 81-91, June 2011. 
Tools and Algorithms for the Construction and Analysis of Systems – 17th International Conference, TACAS 2011LNCS (TACAS 2011)
Parosh Aziz Abdulla and K. Rustan M. Leino
Volume 6605 of Lecture Notes in Computer Science.  Springer, March-April 2011.
Doomed program pointsFMSD
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, and Thomas Wies
Formal Methods in System Design, 37(2-3): 171-199, December 2010. 
Tools and Behavioral Abstraction: A Direction for Software EngineeringFOSE 2010
K. Rustan M. Leino
In Sebastian Nanz, editor, The Future of Software Engineering, pages 115-124.  Springer, November 2010. Festschrift for Bertrand Meyer on the Occasion of His 60th Birthday.
Usable Auto-Active VerificationUV 2010
K. Rustan M. Leino and Michał Moskal
In Tom Ball, Lenore Zuck, and N. Shankar, editors, UV10 (Usable Verification) workshop.  November 2010.  http://fm.csl.sri.com/UV10/
VACID-0: Verification of Ample Correctness of Invariants of Data-structures, Edition 0 VSTTE 2010 workshop
K. Rustan M. Leino and Michał Moskal
In Tools and Experiments workshop at VSTTE 2010.  August 2010.
Dafny Meets the Verification Benchmarks ChallengeVSTTE 2010
K. Rustan M. Leino and Rosemary Monahan
In Gary T. Leavens, Peter W. O’Hearn, and Sriram K. Rajamani, editors, Verified Software: Theories, Tools, Experiments, Third International Conference, VSTTE 2010, volume 6217 of Lecture Notes in Computer Science, pages 112-126.  Springer, August 2010.
To Goto Where No Statement Has Gone BeforeVSTTE 2010
Mike Barnett and K. Rustan M. Leino
In Gary T. Leavens, Peter W. O’Hearn, and Sriram K. Rajamani, editors, Verified Software: Theories, Tools, Experiments, Third International Conference, VSTTE 2010, volume 6217 of Lecture Notes in Computer Science, pages 157-168.  Springer, August 2010.
Learning to do program verificationCACM
K. Rustan M. Leino
Communications of the ACM, 53(6): 106, June 2010. Technical Perspective, introducing the article seL4: Formal Verification of an Operating-System Kernel by Gerwin Klein et al. 
Dafny: An Automatic Program Verifier for Functional Correctness LPAR-16
K. Rustan M. Leino
In Edmund M. Clarke and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning – 16th International Conference, LPAR-16, volume 6355 of Lecture Notes in Computer Science, pages 348-370.  Springer, April-May 2010.
Deadlock-Free Channels and LocksESOP 2010
K. Rustan M. Leino, Peter Müller, and Jan Smans
In Andrew D. Gordon, editor, Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, volume 6012 of Lecture Notes in Computer Science, pages 407-426.  Springer, March 2010.
A Polymorphic Intermediate Verification Language: Design and Logical EncodingTACAS 2010
K. Rustan M. Leino and Philipp Rümmer
In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, volume 6015 of Lecture Notes in Computer Science, pages 312-327.  Springer, March 2010.
Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs LASER 2007/2008
K. Rustan M. Leino and Peter Müller
In Peter Müller, editor, Advanced Lectures on Software Engineering, LASER Summer School 2007/2008, volume 6029 of Lecture Notes in Computer Science, pages 91-139.  Springer, 2010.
It’s Doomed; We Can Prove ItFM 2009
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, and Thomas Wies
In Ana Cavalcanti and Dennis Dams, editors, FM 2009: Formal Methods, Second World Congress, volume 5850 of Lecture Notes in Computer Science, pages 338-353.  Springer, November 2009.
A Basis for Verifying Multi-threaded ProgramsESOP 2009
K. Rustan M. Leino and Peter Müller
In Giuseppe Castagna, editor, Programming Languages and Systems, 18th European Symposium on programming, ESOP 2009, pages 378-393.  Springer, March 2009.
Proving Consistency of Pure Methods and Model FieldsFASE 2009
K. Rustan M. Leino and Ronald Middelkoop
In Marsha Chechik and Martin Wirsing, editors, Fundamental Approaches to Software Engineering, 12th International Conference, FASE 2009, pages 231-245.  Springer, March 2009.
Verification of Concurrent Programs with Chalice
K. Rustan M. Leino, Peter Müller, and Jan Smans
In Alessandro Aldini, Gilles Barthe, Roberto Gorrieri, editors, Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, volume 5705 of Lecture Notes in Computer Science, pages 195-222.  Springer, 2009.
Reasoning about Comprehensions with First-Order SMT SolversSAC 2009
K. Rustan M. Leino and Rosemary Monahan
In 2009 Symposium on Applied Computing, pages 615-622.  ACM, March 2009. A previous version of this article had the title Automatic verification of textbook programs that use comprehensions.
Specification and verification of object-oriented softwareMOD 2008
K. Rustan M. Leino
In Manfred Broy, Wassiou Sitou, and Tony Hoare, editors, Engineering Methods and Tools for Software Safety and Security.  NATO Science for Peace and Security Series D: Information and Communication Security.  IOS Press, 2009, volume 22, pages 231-266. Marktoberdorf International Summer School 2008 lecture notes.
A programming model for concurrent object-oriented programsTOPLAS
Bart Jacobs, K. Rustan M. Leino, Frank Piessens, Wolfram Schulte, and Jan Smans
ACM Transactions on Programming Languages and Systems, 31(1), December 2008.
Flexible immutability with frozen objectsVSTTE 2008
K. Rustan M. Leino, Peter Müller, and Angela Wallenburg
In Jim Woodcock and N. Shankar, editors, Verified Software: Theories, Tools, Experiments, VSTTE 2008, volume 5295 of Lecture Notes in Computer Science, pages 192-208.  Springer, October 2008.
Verification Condition SplittingMSR TR
K. Rustan M. Leino, Michał Moskal, and Wolfram Schulte
Technical Report, Microsoft Research, October 2008.
HOL-Boogie – An Interactive Prover for the Boogie Program-VerifierTPHOLs 2008
Sascha Böhme, K. Rustan M. Leino, and Burkhart Wolff
In Otmane Aït Mohamed, César A. Muñoz, Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, volume 5170 of Lecture Notes in Computer Science, pages 150-166.  Springer, August 2008.
Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software EngineeringCOMPAC 2008
K. Rustan M. Leino
In Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference, COMPSAC 2008, page 11.  IEEE Computer Society, August 2008.
This is Boogie 2MSR TR
K. Rustan M. Leino
Technical Report, Microsoft Research, June 2008.
Verification of equivalent-results methodsESOP 2008
K. Rustan M. Leino and Peter Müller
In Sophia Drossopoulou, editor, Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008, volume 4960 of Lecture Notes in Computer Science, pages 307-321.  Springer, March/April 2008.
Class-local object invariantsISEC 2008
K. Rustan M. Leino and Angela Wallenburg
In Proceedings of the 2008 First India Software Engineering Conference, pages 57-66.  ACM, February 2008.
Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domainWING 2007
K. Rustan M. Leino and Francesco Logozzo
In proceedings of Workshop on Invariant Generation (WING 2007), June 2007.
Specification and verification challenges for sequential object-oriented programsFAC
Gary T. Leavens, K. Rustan M. Leino, and Peter Müller
Formal Aspects of Computing, 19(2):159-189, June 2007.
Using history invariants to verify observersESOP 2007
K. Rustan M. Leino and Wolfram Schulte
In Rocco De Nicola, editor, Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, volume 4421 of Lecture Notes in Computer Science, pages 80-94.  Springer, March 2007.
Practical reasoning about invocations and implementations of pure methodsFASE 2007
Ádám Darvas and K. Rustan M. Leino
In Matthew B. Dwyer and Antónia Lopes, editors, Fundamental Approaches to Software Engineering, 10th International Conference, FASE 2007, volume 4422 of Lecture Notes in Computer Science, pages 336-351.  Springer, March 2007.
A verifying compiler for a multi-threaded object-oriented languageMOD 2006
K. Rustan M. Leino and Wolfram Schulte
In Manfred Broy, Johannes Grünbauer, and Tony Hoare, editors, Software Safety and Security.  NATO Science for Peace and Security Series D: Information and Communication Security.  IOS Press, 2007, volume 9, pages 351-416. Marktoberdorf International Summer School 2006 lecture notes.
Foreword
K. Rustan M. Leino
Verification of Object-Oriented Software: The KeY Approach.  Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt, editors.  Volume 4334 of Lecture Notes in Artificial Intelligence, pages VII-VIII.  Springer, 2007.
Boogie: A Modular Reusable Verifier for Object-Oriented ProgramsFMCO 2005
Mike Barnett, Robert DeLine, Bart Jacobs, Bor-Yuh Evan Chang, and K. Rustan M. Leino
In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, Formal Methods for Components and Objects:  4th International Symposium, FMCO 2005, volume 4111 of Lecture Notes in Computer Science, pages 364-387.  Springer, September 2006.
Verified Software: Theories, Tools, and Experiments, VSTTE 2006, Workshop proceedingsMSR TR (VSTTE 2006)
K. Rustan M. Leino and Wolfram Schulte, editors
Technical Report MSR-TR-2006-117, Microsoft Research, August 2006.
A verification methodology for model fieldsESOP 2006
K. Rustan M. Leino and Peter Müller
In Peter Sestoft, editor, Programming Languages and Systems: 15th European Symposium on Programming, ESOP 2006, volume 3924 of Lecture Notes in Computer Science, pages 115-130.  Springer, March 2006.
Loop invariants on demandAPLAS 2005
K. Rustan M. Leino and Francesco Logozzo
In Kwangkeun Yi, editor, Programming Languages and Systems, Third Asian Symposium, APLAS 2005, volume 3780 of Lecture Notes in Computer Science, pages 119-134.  Springer, November 2005.
The Spec# programming system: Challenges and directionsVSTTE 2005
Mike Barnett, Robert DeLine, Bart Jacobs, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte, and Herman Venter
Position paper, Verified Software: Theories, Tools, Experiments (VSTTE 2005), October 2005.
Weakest-precondition of unstructured programsPASTE 2005
Mike Barnett and K. Rustan M. Leino
In Michael D. Ernst and Thomas P. Jensen, editors, Proceedings of the 2005 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE’05, pages 82-87.  ACM, September 2005.
Safe Concurrency for Aggregate Objects with InvariantsSEFM 2005
Bart Jacobs, K. Rustan M. Leino, Frank Piessens, and Wolfram Schulte
In Bernhard K. Aichernig and Bernhard Beckert, editors, 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), pages137-146.  IEEE Computer Society, September 2005.
Modular verification of static class invariantsFM 2005
K. Rustan M. Leino and Peter Müller
In John Fitzgerald, Ian J. Hayes, and Andrzej Tarlecki, editors, FM 2005: Formal Methods, International Symposium of Formal Methods Europe, volume 3582 of Lecture Notes in Computer Science, pages 26-42.  Springer, July 2005.
BoogiePL: A typed procedural language for checking object-oriented programsMSR TR
Robert DeLine and K. Rustan M. Leino
Technical Report MSR-TR-2005-70, Microsoft Research, May 2005.
A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem ProverTACAS 2005
K. Rustan M. Leino, Madan Musuvathi, and Xinming Ou
In Nicolas Halbwachs and Lenore D. Zuck, editors, Tools and Algorithms for the Construction and Analysis of Software, 11th International Conference, TACAS 2005, volume 3440 of Lecture Notes in Computer Science, pages 334-348.  Springer, April 2005.
Efficient weakest preconditionsIPL
K. Rustan M. Leino
Information Processing Letters, 93(6):281-288, March 2005.
An overview of JML tools and applicationsSTTT
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll
International Journal on Software Tools for Technology Transfer, 7(3):212-232, 2005.
Generating error traces from verification-condition counterexamplesSCP
K. Rustan M. Leino, Todd Millstein, and James B. Saxe
Science of Computer Programming, 55(1-3):209-226, 2005.
Inferring object invariantsAIOOL 2005
Bor-Yuh Evan Chang and K. Rustan M. Leino
First international workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL), January 2005.
Abstract interpretation with alien expressions and heap structuresVMCAI 2005
Bor-Yuh Evan Chang and K. Rustan M. Leino
In Radhia Cousot, editor, Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, volume 3385 of Lecture Notes in Computer Science, pages 147-163.  Springer, January 2005.
Finding stale-value errors in concurrent programsC&C: P&E
Michael Burrows and K. Rustan M. Leino
Concurrency and Computation: Practice and Experience, 16(12):1161-1172, October 2004.
Modular verification of global module invariants in object-oriented programsETHZ TR
K. Rustan M. Leino and Peter Müller
Technical Report 459, ETH Zurich, Department of Computer Science, September 2004.
Exception safety for C#SEFM 2004
K. Rustan M. Leino and Wolfram Schulte
In Jorge R. Cuellar and Zhiming Liu, editors, SEFM 2004—Second International Conference on Software Engineering and Formal Methods, pages 218-227.  IEEE, September 2004.
Object invariants in dynamic contextsECOOP 2004
K. Rustan M. Leino and Peter Müller
In Martin Odersky, editor, ECOOP 2004—Object-oriented programming, 18th European Conference, Proceedings, volume 3086 of Lecture Notes in Computer Science, pages 491-516.  Springer, June 2004.
Verification of object-oriented programs with invariantsJOT
Mike Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte
Journal of Object Technology, 3(6):27-56, June 2004.
The Spec# Programming System: An overviewCASSIS 2004
Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte
In Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, Traian Muntean, editors, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, volume 3362 of Lecture Notes in Computer Science, pages 49-69.  Springer, March 2004.
On computing the fixpoint of a set of boolean equationsMSR TR
Viktor Kuncak and K. Rustan M. Leino
Technical Report MSR-TR-2003-08, Microsoft Research, December 2003. Also available as cs.PL/0408045, The Computing Research Repository (CoRR).
Declaring and checking non-null types in an object-oriented languageOOPSLA 2003
Manuel Fähndrich and K. Rustan M. Leino
In Proceedings of the 2003 ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’03), volume 38(11) of SIGPLAN Notices, pages 302-312.  ACM, November 2003.
Abstraction dependencies
K. Rustan M. Leino and Greg Nelson
In Annabelle McIver and Carroll Morgan, editors, Programming Methodology, Monographs in Computer Science, chapter 13, pages 269-289.  Springer, 2003.
Heap monotonic typestatesIWACO 2003
Manuel Fähndrich and K. Rustan M. Leino
In Proceedings of International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO), July 2003.
A SAT characterization of boolean-program correctnessSPIN 2003
K. Rustan M. Leino
In Thomas Ball and Sriram K. Rajamani, editors, Model Checking Software, volume 2648 of Lecture Notes in Computer Science, pages 104-120.  Springer, May 2003.
In-place refinement for effect checkingAVIS’03
Viktor Kuncak and K. Rustan M. Leino
Presented at Second International Workshop on Automated Verification of Infinite-State Systems (AVIS’03), Warsaw, Poland, April 2003.
A logic of object-oriented programs
Martín Abadi and K. Rustan M. Leino
In Nachum Dershowitz, editor, Verification: Theory and Practice, Essays dedicated to Zohar Manna on the occasion of his 64th birthday, volume 2772 of Lecture Notes in Computer Science, pages 11-41.  Springer, 2003.
Data abstraction and information hidingTOPLAS
K. Rustan M. Leino and Greg Nelson
ACM Transactions on Programming Languages and Systems, 24(5):491-553, September 2002.
Using data groups to specify and check side effectsPLDI 2002
K. Rustan M. Leino, Arnd Poetzsch-Heffter, and Yunhong Zhou
In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), volume 37(5) of SIGPLAN Notices, pages 246-257.  ACM, May 2002.
Extended static checking for JavaPLDI 2002
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata
In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), volume 37(5) of SIGPLAN Notices, pages 234-245.  ACM, May 2002. Most Influential PLDI 2012 Paper Award (awarded in 2012).
Applications of extended static checkingSAS’01
K. Rustan M. Leino
In Patrick Cousot, editor, Static Analysis: 8th International Symposium (SAS’01), volume 2126 of Lecture Notes in Computer Science, pages 185-193. Springer, July 2001.
Houdini, an annotation assistant for ESC/JavaFME 2001
Cormac Flanagan and K. Rustan M. Leino
In International Symposium of Formal Methods Europe 2001: Formal Methods for Increasing Software Productivity, volume 2021 of Lecture Notes in Computer Science, pages 500-517. Springer, March 2001.
Annotation inference for modular checkersIPL
Cormac Flanagan, Rajeev Joshi, and K. Rustan M. Leino
Information Processing Letters, 77(2-4):97-108, February 2001.
Real estate of namesIPL
K. Rustan M. Leino
Information Processing Letters, 77(2-4):169-171, February 2001.
Extended static checking: A ten-year perspectiveDagstuhl 10th anniversary
K. Rustan M. Leino
In Reinhard Wilhelm, editor, Informatics—10 Years Back, 10 Years Ahead, volume 2000 of Lecture Notes in Computer Science, pages 157-175. Springer, January 2001.
ESC/Java quick referenceSRC TN
Silvija Seres with K. Rustan M. Leino and James B. Saxe
Technical Note 2000-004, Compaq Systems Research Center, Palo Alto, CA, October 2000.
ESC/Java user’s manualSRC TN
K. Rustan M. Leino, Greg Nelson, and James B. Saxe
Technical Note 2000-002, Compaq Systems Research Center, Palo Alto, CA, October 2000.
JML: Notations and tools supporting detailed design in JavaOOPSLA’00 poster
Gary T. Leavens, K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs
In OOPSLA’00 Companion. ACM, 2000. Also available as Technical Report TR #00-15, Department of Computer Science, Iowa State University, August 2000.
A semantic approach to secure information flowSCP
Rajeev Joshi and K. Rustan M. Leino
Science of Computer Programming, 37(1-3):113-138, May 2000.
Checking Java programs via guarded commandsFTfJP 1999
K. Rustan M. Leino, James B. Saxe, and Raymie Stata
Technical Note 1999-002, Compaq Systems Research Center, Palo Alto, CA, May 1999. Also appeared in Formal Techniques for Java Programs, workshop proceedings. Bart Jacobs, Gary T. Leavens, Peter Muller, and Arnd Poetzsch-Heffter, editors. Technical Report 251, Fernuniversität Hagen, 1999.
Virginity: A contribution to the specification of object-oriented softwareIPL
K. Rustan M. Leino and Raymie Stata
Information Processing Letters, 70(2):99-105, April 1999.
Joining specification statementsTCS
K. Rustan M. Leino and Rajit Manohar
Theoretical Computer Science, 216(1-2):375-394, March 1999.
Computing permutation encodingsFAC
K. Rustan M. Leino
Formal Aspects of Computing, 11(1):56-74, 1999.
Extended static checkingSRC RR
David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe
Research Report 159, Compaq Systems Research Center, Palo Alto, CA, December 1998.
Data groups: Specifying the modification of extended stateOOPSLA ’98
K. Rustan M. Leino
In Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA ’98), volume 33(10) of ACM SIGPLAN Notices, pages 144-153.  ACM, October 1998.
Recursive object types in a logic of object-oriented programsNJC
K. Rustan M. Leino
Nordic Journal of Computing, 5(4):330-360, 1998.
Wrestling with rep exposureSRC RR
David L. Detlefs, K. Rustan M. Leino, and Greg Nelson
Research Report 156, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, July 1998.
A semantic approach to secure information flowMPC ’98
K. Rustan M. Leino and Rajeev Joshi
In Johan Jeuring, editor, Mathematics of Program Construction: 4th International Conference, MPC’98, volume 1422 of Lecture Notes in Computer Science, pages 254-271. Springer, June 1998.
Recursive object types in a logic of object-oriented programsESOP ’98
K. Rustan M. Leino
In Chris Hankin, editor, Programming Languages and Systems: 7th European Symposium on Programming, ESOP’98, volume 1381 of Lecture Notes in Computer Science, pages 170-184. Springer, April 1998.
Tool Demonstration:  An extended static checker for Modula-3CC’98 tool demo
K. Rustan M. Leino and Greg Nelson
In Kai Koskimies, editor, Compiler Construction: 7th International Conference, CC’98, volume 1383 of Lecture Notes in Computer Science, pages 302-305. Springer, April 1998.
A small dual-automorphic lattice with no involutory dual automorphismSRC TN
K. Rustan M. Leino and Lyle Ramshaw
Technical Note 1997-008, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, May 1997.
A logic of object-oriented programsTAPSOFT ’97
Martín Abadi and K. Rustan M. Leino
In Michel Bidoit and Max Dauchet, editors, Theory and Practice of Software Development: Proceedings / TAPSOFT ’97, 7th International Joint Conference CAAP/FASE, volume 1214 of Lecture Notes in Computer Science, pages 682-696. Springer, April 1997.
Checking object invariantsSRC TN
K. Rustan M. Leino and Raymie Stata
Technical Note 1997-007, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, January 1997.
Ecstatic: An object-oriented programming language with an axiomatic semanticsFOOL 4
K. Rustan M. Leino
In Proceedings of the Fourth International Workshop on Foundations of Object-Oriented Languages, January 1997.
Conditional compositionFAC
Rajit Manohar and K. Rustan M. Leino
Formal Aspects of Computing, 7(6):683-703, March 1995.
Constructing a program with exceptionsIPL
K. Rustan M. Leino
Information Processing Letters, 53(3):159-163, February 1995.
Toward reliable modular programsPhD thesis
K. Rustan M. Leino
PhD thesis, California Institute of Technology, January 1995.  Available as Technical Report Caltech CS-TR-95-03.
A method for showing progressFAC
K. Rustan M. Leino
Formal Aspects of Computing, 7(5):567-580, January 1995.
Semantics of exceptionsPROCOMET ’94
K. Rustan M. Leino and Jan L. A. van de Snepscheut
In E.-R. Olderog, editor, Programming concepts, methods, and calculi (PROCOMET’94), volume A-56 of IFIP Transactions, pages 447-466. North-Holland, June 1994.
Multicomputer programming with Modula-3DMS thesis
K. Rustan M. Leino
MS thesis, California Institute of Technology, June 1993.  Available as Technical Report Caltech CS-TR-93-15.
Extensions to an object-oriented programming language for programming fine-grain multicomputersCaltech CS TR
K. Rustan M. Leino
Technical Report Caltech-CS-TR-92-26, 1992.
K pinwheel schedulable numbers always have 3 friends, but need not have more
K. Rustan M. Leino
Undergraduate honors research, The University of Texas at Austin, May 1989.  Unpublished manuscript.

Presentations

(other than conference and workshop presentations of papers above)

  • Verification beyond programs
    • Invited talk, Workshop on Software Correctness and Reliability, Zurich, Switzerland (October 2016).
  • Certified intermediate verification language
    • IFIP WG 2.3 meeting 58, Villebrumier, France (October 2016).
  • Advanced Encodings into an Intermediate Verification Language
    • Invited talk, AutoProof workshop, Villebrumier, France (October 2016).
  • Global snapshots
    • Dr. TLA+ series lecture, Microsoft Research (and youtube), Redmond, WA, USA (September 2016).
  • Two-state lemmas
    • Lightening talk, UW PLSE Retreat 2016, Leavenworth, WA, USA (September 2016).
  • Dafny Autumn School
    • 2-day seminar, with Gudmund Grov, Edinburgh, Scotland, UK (September 2016).
  • Verification for the rest of us
    • Invited talk, MisraFest, Austin, TX, USA (April 2016).
  • Dafny tutorial
    • Invited tutorial, VerifyThis @ ETAPS 2016, Eindhoven, The Netherlands (April 2016).
  • Automated verification of functional programs
    • Dagstuhl seminar on Verification of Functional Languages, Dagstuhl, Germany (March 2016).
  • Modeling program semantics in an automated program verifier
    • Pacific Northwest PLSE 2016, Seattle, WA (March 2016).
  • Extreme predicates beyond continuity
    • IFIP WG 2.3 meeting 57, Pasadena, CA, USA (January 2016).
  • Software correctness: A personal journey
    • Invited talk, PAUSE, Villebrumier, France (December 2015).
  • The Dafny perspective on reasoning
    • Seminar, TU Darmstadt, Germany (March 2016)
    • CS Colloquium, Yale University, New Haven, CT, USA (November 2015).
  • Dafny: Programs and proofs
    • PLCLUB seminar, University of Pennsylvania, Philadelphia, PA, USA (October 2015).
  • Traits and dynamic frames
    • Semantics and Verification of Object-Oriented Languages, NII Shonan Meeting Seminar 063, Japan (September 2015).
  • Program semantics and machine-assisted proofs
    • 3-day mini-course, Imperial College London, London, UK (May 2015).
  • Programming with and implementing Hilbert’s ε operator
    • IFIP WG 2.3 meeting 56, Istanbul, Turkey (March 2015).
  • Induction, Synthesis, Inference
    • Invited talk, Induction workshop, Chalmers, Göteborg, Sweden (March 2015).
  • Making program verification work
    • Seminar, U. Bergen, Norway (June 2015).
    • Seminar, CEA LIST, Paris, France (March 2015).
    • PL Seminar, UC Berkeley, CA, USA (February 2015).
  • Higher-order functions in the verification-aware programming language Dafny
    • Seminar, Imperial College London, UK (January 2015).
  • Using Dafny for proofs
    • Guest presentation, C141, Imperial College London, UK (January 2015).
  • Early Verification
    • Keynote, VMCAI 2015, joint TIFR Colloquium, Mumbai, India (January 2015).
  • Preserving intent
    • New Directions In Software Technology (NDIST’14), St John, VI, USA (December 2014).
  • Thinking for a living
    • Invited talk, Renton Rotary, Renton, WA, USA (December 2014).
  • Program verification via an intermediate verification language
    • Guest lecture in Emina Torlak’s CSE 507, Computer-Aided Reasoning for Software, University of Washington, Seattle, WA (May 2016).
    • Guest lecture in Emina Torlak’s CSE 507, Computer-Aided Reasoning for Software, University of Washington, Seattle, WA (October 2014).
  • An interface to symbolic methods
    • Keynote, International Workshop on Algebraic Development Techniques (WADT 2014), Sinaia, Romania (September 2014)
  • Predicates that do more
    • IFIP WG 2.3 meeting 55, Orlando, FL, USA (May 2014).
  • Using Dafny for programs and proofs
    • Invited Tutorial, AI4FM workshop, Singapore (May 2014).
  • Verifying coroutines
    • Seminar, ETH Zurich, Switzerland (April 2014).
  • Dafny crash course
    • Tutorial, Dagstuhl seminar on Evaluating Software Verification Systems: Benchmarks and Competitions, Schloss Dagstuhl, Germany (April 2014).
  • Programming in Stages
    • Invited Talk, Third workshop on Validation Strategies for Software Evolution, Grenoble, France (April 2014).
  • Theorem Proving and Program Verification with Dafny
    • 3-day mini-course, Imperial College London, London, UK (March 2014).
  • Dafny induction demo
    • Induction workshop, Imperial College London, London, UK (November 2013).
  • Theorem proving using SMT
    • Keynote, ITP 2013, Rennes, France (July 2013).
  • More co-induction
    • IFIP WG 2.3 meeting 54, Saint Petersburg, Russia (June 2013).
  • Dafny: A programming system for functional correctness
    • CS Colloquium, UCLA, Los Angeles, CA (January 2014).
    • Northrop Grumman, Carson, CA (June 2013).
    • Microsoft Development Center Copenhagen, Copenhagen, Denmark (June 2013).
    • Oracle Labs, Redwood Shores, CA (May 2013).
  • For programs and proofs:  mo’ specs and mo’ math
    • JML seminar, Shonan Village, Japan (May 2013).
  • Verifying coroutines
    • Imperial College, London, UK (March 2013).
  • Program Proving using Intermediate Verification Languages (IVLs) like Boogie and Why3
    • Invited plenary talk, HILT 2012, Boston, MA (December 2012).
  • Developing verified programs with Dafny
    • Tutorial, SPLASH 2013, Indianapolis, IN (October 2013).
    • Tutorial, ICSE 2013, San Francisco, CA (May 2013).
    • Tutorial, HILT 2012, Boston, MA (December 2012).
  • Dafny and other tools in RiSE
    • NASA Ames, Moffett Field, CA (November 2012).
  • Induction, co-induction, calculations—what’s not to like about Dafny?
    • Chalmers Technical University, Göteborg, Sweden (May 2013).
    • Imperial College, London, UK (November 2012).
    • CMU, Pittsburgh, PA (November 2012).
  • Dafny, a programming system for functional correctness
    • Oracle Labs, Redwood Shores, CA (May 2013).
    • Ohio State University, Columbus, OH (November 2012).
    • NASA JPL LaRS, Pasadena, CA (November 2012).
  • Staged program development
    • Keynote, SPLASH 2012, Tucson, AZ (October 2012).
  • Coinduction in a language and verifier
    • IFIP WG 2.3 meeting 53, Kirkland, WA (July 2012).
  • Induction and coinduction in an automatic program verifier
    • Dagstuhl seminar on AI meets formal software development, Schloss Dagstuhl, Germany (July 2012).
  • Dafny: a tool for program correctness
    • PL seminar, MIT, Cambridge, MA (June 2012).
  • Languages and tools for supporting programmers at design time
    • Invited talk, New England Programming Languages and Systems Symposium (NEPLS), Portland, ME (June 2012).
  • Engineering Methods for Ensuring Program Correctness
    • Microsoft Research LATAM Faculty Summit, Riviera Maya, Mexico (May 2012).
  • Dafny: A Language and Program Verifier for Functional Correctness
    • Tutorial, Microsoft Research LATAM Faculty Summit, Riviera Maya, Mexico (May 2012).
  • Program verification using Dafny
    • ELLIIT Distinguished Lecture, Linköping University, Linköping, Sweden (March 2012).
  • Wasn’t that easy?! A tutorial on program verification with Dafny
    • Tutorial, KTH, Stockholm, Sweden (March 2012).
  • The increasing role of verification in software development
    • ACCESS Distinguished Lecture Series, KTH, Stockholm, Sweden (March 2012).
  • Induction in the program verifier Dafny
    • Imperial College, London, UK (February 2012).
  • Chalice, use and encoding
    • Philippa Gardner’s group meeting, Imperial College, London, UK (February 2012).
  • Developing verified programs with Dafny
    • Semantics lunch, Cambridge University, Cambridge, UK (February 2012).
    • Invited tutorial, VSTTE 2012, Philadelphia, PA (January 2012).
  • Using Chalice to reason about objects and concurrency
    • POPL TutorialFest 2012 (x2), Philadelphia, PA (January 2012).
  • Program verification
    • Guest lecture in Ethan Jackson’s CSE P 503, University of Washington, Seattle, WA (January 2012).
  • Program synthesis with Jennisys
    • IFIP WG 2.3 meeting 52, Winchester, UK (September 2011).
  • Using and Building an Automatic Program Verifier.  4 or 6 lectures.
    • LASER Summer School 2011, Elba, Italy (September 2011).
    • International Summer School Marktoberdorf, Bayrischzell, Germany (August 2011).
  • Using Program Verification Tools in Teaching
    • With Rajeev Joshi and Rosemary Monahan.  Session, Microsoft Research Faculty Summit, Redmond, WA (July 2011).
  • Harnessing SMT power using the verification engine Boogie
    • SAT/SMT Solver Summer School 2011, MIT, Cambridge, MA (June 2011).
  • Building an SMT-based program verifier using Boogie
    • Informatics@Edinburgh Distinguished Lecture – specialized lecture, Edinburgh, Scotland (May 2011).
  • Program verification Yesterday, today, tomorrow
    • Informatics@Edinburgh Distinguished Lecture, Edinburgh, Scotland (May 2011).
  • From Retrospective Verification to Forward-Looking Development
    • Invited talk, NFM 2011, Pasadena, CA (April 2011).
  • Dafny: A program verifier for functional correctness, and for students
    • University of Lugano, Lugano, Switzerland (February 2011).
    • UT Austin, Austin, TX (January 2011).
  • Refinement, reusable libraries, instantiable classes
    • IFIP WG 2.3 meeting 51, Santa Barbara, CA (January 2011).
  • Tools and Behavioral Abstraction: A Direction for Software Engineering
    • Invited talk, Future of Software Engineering symposium, Zurich, Switzerland (November 2010).
  • Using Boogie 2 in the verification of Spec# programs
    • With Rosemary Monahan.  Tutorial, SBMF 2010, Natal, Brazil (November 2010).
  • Dafny, a program verifier for functional correctness
    • Technical University Eindhoven, Eindhoven, The Netherlands (November 2011).
    • CMU, Pittsburg, PA (April 2011).
    • Seminar, Altran Praxis, Bath, UK (August 2010).
  • The Dafny program verifier
    • Victoria University of Wellington, Wellington, NZ (April 2010).
  • Contracts, tools, verification
    • Keynote, ASWEC 2010, Auckland, NZ (April 2010).
  • Two problems in the specification of termination
    • IFIP WG 2.3 meeting 50, Lachen, Switzerland (March 2010).
  • Verifying Concurrent Programs with Chalice
    • Invited talk, VMCAI 2010, Madrid, Spain (January 2010).
  • Fun with code, tests, and verification
    • Guest lecture in Mani Chandy’s CS 141, Caltech, Pasadena, CA (November 2009).
  • Understanding Program Verification
    • Invited talk, PROLE 2009, San Sebastian, Spain (September 2009).
  • Verification of concurrent object-oriented programs
    • EPFL, Lausanne, Switzerland (September 2009).
  • A Foundation for Verifying Concurrent Programs.  2 lectures.
    • 9th International School on Foundations of Security Analysis and Design (FOSAD 2009), Bertinoro, Italy (September 2009).
  • Comparing heap models: Ownership, Dynamic frames, Permissions
    • Dagstuhl seminar on Typing, Analysis and Verification of Heap-Manipulating Programs, Schloss Dagstuhl, Germany (July 2009).
  • Dynamic-frame specifications in Dafny
    • JML seminar, Schloss Dagstuhl, Germany (July 2009).
  • Locks, channels, deadlock freedom, progress
    • IFIP WG 2.3 meeting 49, Boston, MA (June 2009).
  • Correct Concurrency with Chalice
    • Seminar, MIT, Cambridge, MA (June 2009).
    • Seminar, INRIA-MSR joint lab, Orsay, France (January 2009).
  • Verification tools at Microsoft
    • Invited talk, Digiteo seminar, Orsay, France (January 2009).
  • How tool-based verification can be incorporated in teaching
    • Invited talk, Informatics Education Europe III, Venice, Italy (December 2008).
  • Specification techniques for verifying object-oriented software
    • University of Lugano, Lugano, Switzerland (December 2008).
  • Dynamic-frame specifications in Dafny
    • Invited talk, COST Action IC0701, Formal Verification of Object-Oriented Software, working group meeting, Madrid, Spain (December 2008).
  • Specification and Verification of Object-Oriented Software.  5 lectures.
    • International Summer School Marktoberdorf, Marktoberdorf, Germany (August 2008).
  • Ceaselessly-analyzing development environments
    • Panel presentation, COMPSAC 2008, Turku, Finland (July 2008).
  • Specification and Verification of Programs with Pointers.  2 lectures.
    • Summer School on Logic and Theorem-Proving in Programming Languages, Eugene, OR (July 2008).
  • Thread-local contributions
    • IFIP WG 2.3 meeting 48, Cambridge, UK (July 2008).
  • Spec#
    • Alt.NET, Redmond, WA (April 2008).
  • Boogie
    • Microsoft Research India, Bangalore, India (February 2008).
  • Program verification using the Spec# programming system
    • With Rosemary Monahan.  Tutorial, ETAPS 2008, Budapest, Hungary (March 2007).
  • Specifying and verifying software
    • KU Leuven, Leuven, Belgium (August 2008).
    • Chalmers, Göteborg, Sweden (November 2007).
    • Invited talk, ASE 2007, Atlanta, GA (November 2007).
  • Spec#
    • Invited talk, Øredev, Malmö, Sweden (November 2007).
  • Designing a type system for BoogiePL 2
    • IFIP WG 2.3 meeting 47, Santa Fe, NM (October 2007).
  • Designing verification conditions for software
    • Invited talk, CADE-21, Bremen, Germany (July 2007).
  • Program verification via an intermediate language
    • Seminar, National University of Ireland, Maynooth, Maynooth, Ireland (June 2007).
  • Verifying object-oriented software: Lessons and challenges
    • Invited talk, TACAS 2007, part of ETAPS in Braga, Portugal (March 2007).
  • Reasoning about object structures in Spec#
    • UNSW, Sydney, Australia (January 2007).
    • INRIA + Microsoft lab, Paris, France (November 2006).
  • Automatic verification of summations
    • IFIP WG 2.3 meeting 46, Sydney, Australia (January 2007).
  • Going beyond a simple ownership system in Spec#
    • European Science Foundation workshop on Java program verification, Nijmegen, The Netherlands (October 2006).
  • Object invariants in specification and verification
    • Invited talk, Brazilian Symposium on Formal Methods (SBMF 2006), Natal, Brazil (September 2006).
  • Spec#
    • Microsoft Research Faculty Summit 2006, Redmond, WA (July 2006).
  • Specifying and verifying programs in Spec#.
    • Invited talk, Sixth International Andrei Ershov Memorial Conference Perspectives of System Informatics (PSI 2006), Novosibirsk, Russia (June 2006).
  • Building a program verifier
    • Guest lecture in Shaz Qadeer’s CSE 599f, Formal Verification of Computer Systems, University of Washington, Seattle, Washington (May 2006).
  • Panel on Integrated Verification
    • The Challenge of Software Verification, Schloss Dagstuhl, Germany (Jul 2006).
    • IFIP WG 2.3 meeting 45, Bruges, Belgium (April 2006).
  • Invariants on demand
    • Invited talk, 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), Koblenz, Germany (September 2005).
  • Loop invariants on demand
    • IFIP WG 2.3 meeting 44, Niagara Falls, ON (June 2005).
  • The Spec# programming system
    • Distinguished Lecture, Max-Planck Institute for Software Systems, Kaiserslautern, Germany (March 2006).
    • Seminar, Åbo Akademi University, Turku, Finland (December 2005).
    • Lunch seminar, Praxis High Integrity Systems, Bath, UK (December 2005).
    • Short presentation and demo, Verified Software: Theories, Tools, Experiments (VSTTE 2005), Zurich, Switzerland (October 2005).
    • Software Quality Research Lab Distinguished Lecture, McMaster University, Hamilton, ON (May 2005).
    • Colloquium, University of Toronto, Toronto, ON (May 2005).
  • Advanced programming tools at Microsoft
    • Distinguished Lecture, York University, Toronto, ON (May 2005).
  • Demand-driven inference of loop invariants in a theorem prover.
    • Invited talk, Fourth International Workshop on Automated Verification of Infinite-State Systems (AVIS’05), Edinburgh, Scotland, UK (April 2005).
  • Program verification and programming methodology.
    • Invited talk, 12th International Workshop on Abstract State Machines (ASM 2005), Paris, France (March 2005).
  • Programming methodology.
    • Panel discussion, Workshop on the Verification Grand Challenge, Menlo Park, CA (February 2005).
  • Writing specifications for object-oriented programs.
    • Invited talk, First International Workshop on Abstract Interpretation of Object-Oriented Languages, Paris, France (January 2005).
  • Challenges in increasing tool support for programming.
    • Invited talk, First International Colloquium on Theoretical Aspects of Computing, Guiyang, Guizhou, China (September 2004).
  • On bounded model checking, induction, and interpolants
    • IFIP WG 2.3 meeting 43, Prato, Italy (September 2004).
  • Spec#: Writing and checking contracts in a .NET language.
    • Keynote, .NET Technologies 2004, 2nd International Workshop, Plzeň, Czech Republic (June 2004).
  • Hoare-style program verification.  3 lectures.
    • Guest lectures in Rob DeLine’s CSE 503, Software Engineering, University of Washington, Seattle, Washington (April/May 2004).
  • Toward enforceable contracts in .NET
    • Keynote, Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS 2004), Marseille, France (March 2004).
  • Abstract interpretation for heap structures
    • IFIP WG 2.3 meeting 42, Philadelphia, PA (January 2004).
  • Verifying invariants in object-oriented programs
    • Colloquium, Department of Computer Science, ETH Zurich, Switzerland (November 2003).
  • Technologies for finding errors in object-oriented software.  4 lectures.
    • UNU-IIST (United Nations University – International Institute for Software Technology) and IFIP WG 2.3 Summer School on Formal methods of Software, Tunis, Tunisia (September 2003).
  • Static program checking, module by module
    • Invited tutorial, Prato workshop on Trusted Components, Prato, Italy (January 2003).
  • A SAT characterization of boolean-program correctness.
    • IFIP WG 2.3 meeting 41, Biarritz, France (March 2003).
    • Department colloquium, Washington University in St. Louis, St. Louis, MO (February 2003).
    • IFIP WG 2.4 meeting, Schloss Dagstuhl, Germany (November 2002).
    • University of Eindhoven, Eindhoven, The Netherlands (November 2002).
  • ESC/Java or Light-weight formal methods: from objects to components.
    • Invited talk, First international symposium on Formal Methods for Components and Objects (FMCO 2002), Leiden, The Netherlands (November 2002).
  • Checking correctness properties of object-oriented programs.  5 lectures.
    • EEF Summer School on Specification, Refinement and Verification, Turku, Finland (August 2002).
  • Modular checking and side effects.
    • IFIP WG 2.3 meeting 40, Turku, Finland (August 2002).
  • Checking side effects in object-oriented programs.
    • Invited talk, Java Verification Workshop (JVW’02), Portland, OR (January 2001).
  • ESC/Java: The Greatest Thing Since Sliced Bread.
    • Distinguished Lecturer Series, Computing and Information Sciences, Kansas State University, Manhattan, KS (October 2001).
  • Applications of extended static checking.
    • Invited talk, Static Analysis Symposium (SAS’01), Paris, France (July 2001).
  • Challenging applications of extended static checking.
    • Panelist, Silver bullets for AI softwolves, AAAI 2001 Spring Symposium on Model-Based Validation of Intelligence, Stanford, CA (March 2001).
  • Houdini, an annotation assistant for ESC/Java.
    • Swedish Institute of Computer Science, Kista, Sweden (May 2001).
    • Uppsala University, Uppsala, Sweden (May 2001).
    • Chalmers University of Technology, Göteborg, Sweden (May 2001).
    • Computer science colloquium, University of Iowa, Iowa City, IA (May 2001).
    • Microsoft Research, Redmond, WA (April 2001).
    • Imperial College, London, England (January 2001).
    • Oxford University, Oxford, England (January 2001).
  • Benevolent side effects considered malevolent.
    • IFIP WG 2.3 meeting 38, Santa Cruz, CA (January 2001).
  • Program checking.
    • Invited talk, Schloss Dagstuhl’s Tenth Anniversary conference Informatics—10 years back, 10 years ahead, Saarbrucken, Germany (August 2000).
    • IFIP WG 2.3 workshop on program methodology, Tandil, Argentina (September 2000).
  • Real estate of names.
    • Invited talklet, In Pursuit of Simplicity, a symposium honoring Edsger W. Dijkstra, UT Austin, Austin, TX (May 2000).
  • Extended static checking for Java.
    • Automated Software Engineering Group seminar, NASA Ames, Mountain View, CA (November 2001).
    • Distinguished Lecture Series, Cornell University Computer Science Department, Ithaca, NY (Oct 2001).
    • University of Toronto, Toronto, ON, Canada (May 2001).
    • Computer Science Seminar, University of Cambridge, Cambridge, England (April 2000).
    • LFCS Theory Seminar, University of Edinburgh, Edinburgh, Scotland (April 2000).
    • University of Glasgow, Glasgow, Scotland (April 2000).
    • Programming Systems Seminar, UC Berkeley, Berkeley, CA (March 2000).
    • UC Davis, Davis, CA (February 2000).
  • Finding bugs in Java programs.
    • IFIP WG 2.3 meeting 37, Longhorsley, England (April 2000).
  • ESC/Java.
    • Stanford University, Stanford, CA (October 1999).
    • Invited talk, Larch Users’ Group Meeting at World Congress on Formal Methods (FM’99), Toulouse, France (September 1999).
    • UW/MSR Summer Institute on Technologies to Improve Software Development, Semi-ah-moo, WA (August 1999).
  • The essence of object-oriented program semantics.
    • Distinguished Lecturer Series – specialized lecture, Computing and Information Sciences, Kansas State University, Manhattan, KS (October 2001).
    • The University of Texas at Austin, Austin, TX (October 1999).
    • The semantic challenge of object-oriented programming (seminar), Schloss Dagstuhl, Germany (June 1998).
    • IFIP WG 2.3 meeting 35, Bloomington, IN (June 1998).
  • Extended static checking.
    • Invited talk, PROCOMET’98, Shelter Island, NY (June 1998).
  • A semantic approach to secure information flow.
    • California Institute of Technology, Pasadena, CA (March 1998).
    • IFIP WG 2.3 meeting 34, Alsace, France (September 1997).
  • Soundness and completeness considered harmful.
    • SRI computer science seminar, Menlo Park, CA (May 1998).
  • Object invariants in Java.
    • IFIP WG 2.3 meeting 34, Alsace, France (September 1997).
  • Generalized data abstraction.
    • IFIP WG 2.3 meeting 33, Napa Valley, CA (January 1997).
  • Extended static checking.
    • ETH Zurich, Zurich, Switzerland (September 1997).
    • The University of Texas at Austin, Austin, TX (August 1997).
    • Rice University, Houston, TX (July 1997).
    • IBM Austin Research Laboratory, Austin, TX (July 1997).
    • Seminar on semantics and abstract interpretation, Ecole Normale Superieure, Paris, France (April 1997).
    • California Institute of Technology, Pasadena, CA (December 1996).
    • Odyssey Research Associates, Inc., Ithaca, NY (November 1996).
    • NUPRL seminar, Cornell University, Ithaca, NY (November 1996).
  • Toward reliable modular programs.

Microsoft Research, Redmond, WA (January 1995).

Professional Distinctions

  • Tool Used by Most Teams Award (for Dafny), VerifyThis @ ETAPS 2015 program verification competition
  • ACM SIGPLAN Most Influential 2002 PLDI Paper Award, 2012.  For the paper “Extended Static Checking for Java” by Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata.
  • Shared Tool Used by Most Teams Award (for Dafny), VerifyThis @ FM 2012 program verification competition
  • Silver Medal (with Peter Müller), VSTTE 2012 Program Verification Competition
  • Best Paper Award, FM 2011 for the paper “Software Competition: Experience Report” by Vladimir Klebanov, et al.
  • IFIP Silver Core Award, 2010, awarded for outstanding service
  • Member, IFIP Working Group 2.3 “Programming Methodology”, 2000-present.  (Secretary, 2003-2012.)

Graduate school awards and distinctions

  • Research supported by Digital Equipment Corporation Systems Research Center, Palo Alto, CA, 1992-93 and 1994-95.
  • American Scandinavian Foundation of Los Angeles. Scholarship, 1994.
  • One of about 75 computer science students selected worldwide to attend the International Summer School on Program Design Calculi, Marktoberdorf, Germany, 1992.

Undergraduate awards and distinctions

  • Upsilon Pi Epsilon, Computer Science Honors Society (elected officer, UT Austin, 1988-89).
  • College of Natural Sciences, College Scholar, UT Austin, 1988 and 1989.
  • The Honor Society of Phi Kappa Phi.
  • Phi Beta Kappa.
  • Golden Key National Honor Society.
  • Angus G. and Erna H. Pearson Endowed Scholarship, UT Austin, 1988.
  • Alpha Lambda Delta, Freshman Honor Society.
  • Phi Eta Sigma, Freshman Honor Society.

High school awards and distinctions

  • Among numerous other academic high school awards, won 1st place Advanced Level, Kentucky Council Teachers of Mathematics High School Math Contest, 1985-86.
  • Among other high school programming contests first places, tied 5th place in the 1986 International Computer Program Solving Contest, in which 2500 teams from 13 countries participated. (With teammates Robert S. French and Dean Brooks.)

Among several other musical awards in high school, selected to play in the 1986 Kentucky All-State Symphonic Band. (Bass saxophone and baritone saxophone.)

Advisory Committees

Thesis committees

  • Habilitation thesis committees:
    • Jean-Christophe Filliâtre, Université Paris Sud 11 (December 2011).
    • Claude Marché, University Paris 11 (2005).
  • PhD thesis committees:
    • Tim Woods, Imperial College London (December 2016).  Internal reviewer.  Advisor: Sophia Drossopoulou.
    • Martin Hentschel, TU Darmstadt (March 2016).  External reviewer.  Advisor:  Reiner Hähnle.
    • Nadia Polikarpova, ETH Zurich (April 2014).  External reviewer.  Advisor:  Bertrand Meyer.
    • Nicholas Smallbone, Chalmers Technical University (May 2013).  Opponent.  Advisor:  Koen Claessen.
    • Ronald Middelkoop, Technical University Eindhoven (November 2011).  External reviewer.  Advisor: Ruurd Kuiper and Kees Huizing.  Professor:  Mark G. J. van den Brand.
    • Aliaksei Ttsitovich, University of Lugano (February 2011).  Advisor: Natasha Sharygina.
    • Radu Grigore, University College Dublin (August 2010).  External reviewer.  Advisor:  Joe Kiniry.
    • Yannick Moy, Université Paris 11 (2009).  External reviewer.  Advisor: Claude Marché.
    • Cristina Cerschi Seceleanu, Åbo Akademi University (2005).  External reviewer and Opponent.  Advisor:  Academy Prof. Dr. Ralph-Johan Back.
    • Rajeev Joshi, The University of Texas at Austin (1999).  Advisor:  Prof. Dr. Jayadev Misra.

Editorial boards

  • Editorial board, Journal of Automated Reasoning, 2007-present.

Project advice

  • Project evaluator, Research theme: Proof and Verification, INRIA, 2015.
  • Project evaluator, Research theme A: Symbolic systems, INRIA, 2006.
  • Scientific advisory board, Mobius project, 2005-2007.
  • Project retreat external visitor, Open Software Quality project, UC Berkeley, May 2001.

Steering committees

  • Programming Languages meet Program Verification (PLPV) workshop (2011-2015)
  • ETAPS steering committee (2011-2012)
  • BOOGIE workshop on intermediate verification languages (2011-2012)
  • Formal Techniques for Java-like Programs (FTfJP) workshop (2004-present)

Program committees

  • Formal Methods (FM 2016), Limassol, Cyprus (November 2016).
  • 3rd Workshop on Formal Integrated Development Environment (F-IDE 2016), at FM 2016, Limassol, Cyprus (November 2016).
  • 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), Toronto, ON, Canada (July 2016).
  • Co-chair, International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016), St Petersburg, FL, USA (January 2016).
  • 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-20), Suva, Fiji (November 2015).
  • Formal Methods (FM 2015), Oslo, Norway (June 2015).
  • 7th NASA Formal Methods Symposium (NFM 2015), Pasadena, CA, USA (April 2015).
  • 2nd Workshop on Formal Integrated Development Environment (F-IDE 2015), at FM 2015, Oslo, Norway (June 2015).
  • 1st Workshop on Formal Integrated Development Environment (F-IDE 2014), at ETAPS 2014, Grenoble, France (April 2014).
  • Workshop on Formal Techniques for Java-like Programs (FTfJP 2013), at ECOOP 2013, Montpellier, France (2013).
  • ESEC/FSE 2013 Tool Demos (ESEC/FSE Tools), Saint Petersburg, Russia (August 2013).
  • 24th International Conference on Automated Deduction (CADE-24), Lake Placid, NY (June 2013).
  • 27th European Conference on Object-Oriented Programming (ECOOP 2013), Montpellier, France (June 2013).
  • Formal Methods (FM 2012), Paris, France (August 2012).
  • 26th European Conference on Object-Oriented Programming (ECOOP 2012), Beijing, China (June 2012).
  • Eighteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), Tallinn, Estonia (March 2012).
  • Verified Software: Theories, Tools and Experiments (VSTTE 2012), Philadelphia, PA (January 2012).
  • Co-chair, First International Workshop on Intermediate Verification Languages (BOOGIE 2011), Wrocław, Poland (August 2011).
  • Workshop on Formal Techniques for Java-like Programs (FTfJP 2011), Lancaster UK (July 2011).
  • Co-chair, Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011), Saarbrücken, Germany (March-April 2011).
  • Verified Software: Theories, Tools and Experiments (VSTTE 2010), Edinburgh, Scotland (August 2010).
  • International Joint Conference on Automated Reasoning (IJCAR 2010), Edinburgh, Scotland (July 2010).
  • Programming Languages meets Program Verification (PLPV 2010), Madrid, Spain (January 2010).
  • Verification, Model Checking, and Abstract Interpretation (VMCAI 2010), Madrid, Spain (January 2010).
  • 11th International Conference on Formal Engineering Methods (ICFEM 2009), Rio de Janeiro, Brazil (December 2009).
  • International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO 2009) (July 2009).
  • Seventh International Andrei Ershov Memorial Conference, Perspectives of System Informatics (PSI 2009), Novosibirsk, Russia (June 2009).
  • Programming Languages meets Program Verification (PLPV 2009), Savannah, Georgia (January 2009).
  • 15th International Symposium on Formal Methods (FM 2008), Turku, Finland (May 2008).
  • Verification, Model Checking, and Abstract Interpretation (VMCAI 2008), San Francisco, CA (January 2008).
  • Ninth International Conference on Formal Engineering Methods (ICFEM 2007), Boca Raton, FL, USA (November 2007).
  • International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO 2007), at ECOOP 2007, Berlin, Germany (July 2007).
  • Workshop on Programming Languages and Analysis for Security (PLAS 2007), at PLDI 2007, San Diego, CA, USA (June 2007).
  • International Conference TOOLS EUROPE 2007 – Objects, Models, Components, Patterns, Zurich, Switzerland (June 2007).
  • Foundations and Developments of Object-Oriented Languages (FOOL/WOOD 2007), at POPL 2007, Nice, France (January 2007).
  • Co-chair, Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 2006), at FLoC 2006, Seattle, WA, USA (August 2006).
  • Formal Methods (FM 2006), Hamilton, Canada (August 2006).
  • 15th International Conference on Compiler Construction (CC 2006), Vienna, Austria (March 2006).
  • Workshop on Formal Techniques for Java-like Programs (FTfJP 2006), at ECOOP, Nantes, France (July 2006).
  • Fourth workshop on Specification and Verification of Component-Based Systems (SAVCBS 2005), at ESEC/FSE 2005, Lisbon, Portugal (September 2005).
  • 3rd International Conference on Software Engineering and Formal Methods (SEFM 2005), Koblenz, Germany (September 2005).
  • 1st International Workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL), at VMCAI 2005, Paris, France (January 2005).
  • 14th International Conference on Compiler Construction (CC 2005), Edinburgh, Scotland (April 2005).
  • Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2004), at ACM SIGSOFT 2004/FSE-12, Newport Beach, California (October/November 2004).
  • 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), Beijing, China (September 2004).
  • Mathematics of Program Construction (MPC 2004), Stirling, Scotland, UK (July 2004).
  • 2nd International Workshop on .NET Technologies’2004, University of West Bohemia, Campus-Bory Plzen, Czech Republic (31 May – 2 June 2004).
  • Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2003), at ESEC/FSE, Helsinki, Finland (September 2003).
  • Workshop on Formal Techniques for Java-like Programs (FTfJP 2003), at ECOOP, Darmstadt, Germany (July 2003).
  • Prato workshop on Trusted Components, Prato, Italy (January 2003).
  • Workshop on Formal Techniques for Java-like Programs (FTfJP 2002), at ECOOP, Málaga, Spain (June 2002).
  • Workshop on Foundations of Aspect-oriented Languages (FOAL), at AOSD, Enschede, The Netherlands (April 2002).
  • Mathematics of Program Construction (MPC 2002), Schloss Dagstuhl, Germany (July 2002).
  • ACM Symposium on Principles of Programming Languages (POPL’02), Portland, Oregon (January 2002).
  • Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2001), at OOPSLA, October 2001.
  • Workshop on Formal Techniques for Java Programs (FTfJP 2001), at ECOOP, Budapest, Hungary (June 2001).
  • The Second International Workshop on Automated Program Analysis, Testing and Verification (WAPATV), at ICSE, Toronto, Canada (May 2001).
  • Mathematics of Program Construction (MPC 2000), Ponte de Lima, Portugal, July 2000.
  • The First International Workshop on Automated Program Analysis, Testing and Verification (WAPATV), at ICSE, University of Limerick, Ireland, June 2000.
  • Intercontinental Workshop on Aliasing in Object-Oriented Systems (IWAOOS’99), in conjunction with ECOOP, Lisbon, Portugal, June 1999.
  • The Sixth International Workshop on Foundations of Object-Oriented Languages (FOOL 6), at POPL, San Antonio, TX, January 1999.

External Review Committees

40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), External Review Committee, Rome, Italy.

Mentoring

  • Research intern mentor, Microsoft Research:
    • Daniel Matichuk (Software Systems Research Group at Data61)
    • Kenny Foner (U. Penn), 2016.
    • Clément Pit–Claudel (MIT), 2015.
    • Dan Rosén (Chalmers), 2014.
    • Maria Christakis (ETH Zurich), 2013.
    • Valentin Wüstholz (ETH Zurich), 2013.
    • Jason Koenig (CMU), 2011, 2012.
    • Aleksandar Milicevic (MIT), 2011.
    • Kuat Yessenov (MIT), 2010.
    • Claire Le Goues (U. Virginia), 2009.
    • Philipp Rümmer (Chalmers), 2008, 2009
    • Ronald Middelkoop (TU Eindhoven), 2007.
    • Ralf Sasse (UI Urbana-Champaign), 2007.
    • Ádám Darvas (ETH Zurich), 2006.
    • Angela Wallenburg (Chalmers), 2006.
    • Bor-Yuh Evan Chang (UC Berkeley), 2004, 2005.
    • Xinming Ou (Princeton), 2004.
    • Rob Klapper (Washington University in St. Louis), 2003.
    • Viktor Kuncak (MIT), 2002.
  • Mentor, Compaq SRC:
    • Stephen N. Freund, 2000-2001.
    • Rajeev Joshi, 1999-2001.
    • Cormac Flanagan, 1997-2001.
    • Raymie Stata, 1996-2000.
  • Research intern host, Compaq SRC:
    • Todd Millstein (University of Washington), 1999.
    • Rajeev Joshi (The University of Texas at Austin), 1997.

Other Professional Activities

  • Microsoft Achievement Award (awarded 2011, used Aug-Oct 2013)
  • Delegate, National Academy of Engineering / UK Royal Academy of Engineering / Chinese Academy of Engineering Global Grand Challenges Summit, London, UK, 2013.
  • National Academy of Engineering Japan-America Frontiers of Engineering symposium, Irvine, CA, Nov 2009.
  • National Academy of Engineering Frontiers of Engineering symposium, Redmond, WA, 2007.
  • Summer intern czar (program coordinator), Compaq SRC, 1998.
  • Graduate Admissions Committee, Computer Science, Caltech, 1994.
  • Contributing editor to Cobb Journal on Microsoft Word for the PC, 1990-1991.
  • Contributor to the LAN Manager Programming Reference, Microsoft Press, 1990.
  • Member of the Association for Computing Machinery, 1989-present.

Patents

  • Raymond Paul Stata, Cormac Flanagan, K. Rustan M. Leino, Mark D. Lillibridge, and James Benjamin Saxe.  System and method for lexing and parsing program annotations.  U.S. Patent 6,353,925, March 2002.
  • Cormac Andrias Flanagan and K. Rustan M. Leino.  Method and apparatus for organizing warning messages.  U.S. Patent 6,978,443, December 2005.
  • K. Rustan M. Leino, Todd David Millstein, and James B. Saxe.  System and method for verifying computer program correctness and providing recoverable execution trace information.  U.S. Patent 7,024,661, April 2006.
  • Cormac Andrias Flanagan and K. Rustan M. Leino.  Method and apparatus for automatically inferring annotations.  U.S. Patent 7,120,902, October 2006.
  • Rustan M. Leino, Mark David Lillibridge, and Raymond Paul Stata. Method and apparatus for statically analyzing a computer program for data dependencies. U.S. Patent 5,987,252, November 1999.

Shareware Computer Games

Compact Discs

  • Caltech Jazz Bands. Exothermic Jazz. 1994.  Director:  Bill Bing. (Tenor and baritone saxophones.)

Videos and Soundtracks

  • PPRC Summer Intern Video, Episode 2002: Attack of the aliasing bug.  Microsoft Research, 2002.  (Production.  And with others, editing and soundtrack.)
  • PPRC Espresso Machine Tutorial.  Microsoft Research, 2003.  With Shaz Qadeer.
  • PPRC Summer Intern Video, The Incredible Race.  Microsoft Research, 2003.  (Production.  And with others, editing and soundtrack.)
  • Verification Corner (https://www.microsoft.com/en-us/research/project/the-verification-corner/)
  • Soundtrack for Emergency Response Procedures video, Compaq SRC, 2000.
  • Soundtrack for Compaq Research for Palo Alto Chamber of Commerce, 2000.
  • Soundtrack for SRC Summer Intern Video 1999. (With Todd Millstein.)
  • Soundtrack for research videos At the Gallery and In the Lab, describing the Bytes of Art project, 1998.
  • Soundtrack for research video describing VistaBar, 1997.
  • SRC Summer Intern Video 1994. (Script, soundtrack, and editing, joint with others.)
  • SRC Summer Intern Video 1992. (Soundtrack and editing, joint with others.)

Acknowledgment: Ken Beckman made the videos in the third group above possible and lots of fun.

Original Music

Some recordings, lyrics, and sheet music of original music is available at http://leino-online.com/music.

Some Musical Appearances

  • Principles of Jazz, POPL 2012 jazz band, Philadelphia, PA.  January 2012.  (Drums, piano.)
  • Jazz Open Jam, a monthly event, Luther’s Table, Renton, WA.  2012-2013.  (Drums, keyboards, tenor sax, vocals.)
  • Band member, Marktoberdorf International Summer School, Bayrischzell, Germany, 2011.  (Piano, vocals.)
  • Principles of Jazz, POPL 2011 jazz band, Austin, TX.  January 2011.  (Drums, tenor sax, piano.)
  • Sit-in with various bands, St. Matthew’s Lutheran Church, Renton, WA.  2012-present.  (Drums, bass, keyboards, tenor sax.)
  • The Assumptions, Marktoberdorf International Summer School, Marktoberdorf, Germany, 2008.  (Tenor sax, bass, keyboards, drums.)
  • God’s Garage band, every third Sunday at 9:30 and 11:00 services, St. Matthew’s Lutheran Church, Renton, WA.  2008-2011.  (Drums, fill-in on keyboards.)
  • Song of the day, monthly at 10:30 service, with Grace Ensemble.  Grace Lutheran Church, Bellevue, WA.  2002-2005.  (Drums, bass guitar, keyboards, sax.)
  • Weekly worship services, Immanuel Lutheran Church, Los Altos, CA. 1996-2001. (Drums, bass guitar, keyboards, vocals.)
  • Joseph and the technicolor dreamcoat. St. Lawrence Academy, March 2001. (Drums.)
  • They’re playing our song. West Valley Light Opera, Spring 1999. (Drums.)
  • Various concerts with the Caltech Thursday Jazz Band, 1992-95. Guest artists at concerts included: drummer Gregg Bissonette, guitarist Grant Geissman, trumpet player Chuck Findley, vocalist Angie Whitney, and composer and arranger Joe Curiale. (Tenor and baritone saxophones.)
  • Various concerts with the Caltech Monday Jazz Band, 1991-92. (Tenor saxophone.)
  • Special appearance with rock band Bob Popular, UT Austin, May 1989. (Tenor saxophone.)

Some Extracurricular Activities

  • Board member, Mending Wings, Yakama Nation. (September 2013-present)
  • Volunteer, Luther’s Table (a cafe and bar), Renton, WA. (September-October 2013)
  • Volunteer High School math teacher, Maths Camp, Sponsor an African Scholar (SAAS), Mombasa, Kenya. (August 2013)
  • Vice President, St. Matthew’s Lutheran Church, Renton, WA.  (2013-present)
  • Council member, St. Matthew’s Lutheran Church, Renton, WA.  (2012-present)
  • Group Exercise Volunteer (step aerobics instructor), Bellevue Family YMCA, Bellevue, WA.  2004-2012.  (Substitute instructor, 2012-present.)
  • Celebrity scientist, 2nd grade class, Somerset Elementary School, Bellevue, WA, January 2007.
  • Celebrity scientist, one 1st grade and one 4th grade class, Somerset Elementary School, Bellevue, WA, February 2006.
  • Fusion Jazz combo (drums), Ron Cole, instructor, Music Works Northwest, Spring 2005, Fall 2005, Winter 2006, Spring 2006.
  • Smooth Jazz combo (drums), Darren Motamedy, instructor, Music Works Northwest, Fall 2004, Winter 2005.
  • Chair, Evangelism committee, Grace Lutheran Church, Bellevue, WA.  2004-present.
  • Coach of a Somerset Elementary School team for Middle School Math Olympiad, Bellevue, WA, Spring 2004.
  • Music leader, Grace Ensemble, Grace Lutheran Church, Bellevue, WA.  2002-2005.
  • Worship and music committee, Grace Lutheran Church, Bellevue, WA.  2002-2004.
  • Co-coach of a Somerset Elementary School team for Middle School Math Olympiad, Bellevue, WA, Spring 2002.
  • Co-leader, small-group Bible studies (Genesis; Jeremiah; Romans; Revelation; Shadow of the Galilean; The inward pilgrimage: an introduction to Christian spiritual classics), Immanuel Lutheran Church, Los Altos, CA, 1999-2001.
  • Chair, Evangelism committee, Immanuel Lutheran Church, Los Altos, CA, 1999-2001.
  • Performed and recorded music for youth group musicals, Immanuel Lutheran Church, Los Altos, CA, 1999, 2000.
  • Visioning for the 21st Century committee, Immanuel Lutheran Church, Los Altos, CA, 1999.
  • Church Council, Immanuel Lutheran Church, Los Altos, CA, 1996-1999.
  • Chair, Youth director search committee, Immanuel Lutheran Church, Los Altos, CA, 1997.
  • Music leader, contemporary worship service, Immanuel Lutheran Church, Los Altos, CA, 1996-1997.
  • Representative at ELCA Sierra Pacific Synod convention, 1997.
  • Chair, Second Phase Building Fund Campaign, Immanuel Lutheran Church, Los Altos, CA, Summer 1996.
  • Helped start contemporary worship service, Immanuel Lutheran Church, Los Altos, CA, 1996.
  • Vision 2000 committee, Immanuel Lutheran Church, Los Altos, CA, 1995.
  • Organizer and co-founder, Caltech Swedish Club, Pasadena, CA, 1993-1994.
  • President, AAL Branch #6905 (a fraternal benefit society), San Gabriel, CA, 1993-1994.
  • Arranged, performed, and recorded music for youth group musicals, Trinity Lutheran Church, San Gabriel, CA, 1992, 1993.

Last updated November 2016.