Looking for students and postdocs

Work on exciting projects! Change the world!

Unfortunately, computing in Germany isn’t what it used to be in the 80’s. It can still be fun, though.

Rant

I saw the following (redacted, numbers modified) section in a recent paper doing a long proof in an interactive theorem prover:

Statistics

My proof, excluding standard libraries and the library for foobaring bazes, consists of 33 source files, 9 136 lines of specifications, 37 101 lines of proof, and 1 255 709 total characters. The size of the gzipped tarball (gzip -9) of all the source files is 135 009 bytes, which is an estimate of the information content of my proof.

 

 Call me a stat-hater, but I found the last line somewhat ridiculous. What next? Every paper must have a section

 

The size of the gzipped (gzip -9) pdf file for this paper is XXX bytes, which is an estimate of the information content of this paper.

 

A nice fixpoint problem to find XXX, though!

Advertisement

Schooling in Germany

My child’s kindergarten has three groups of children: the mouse group, the mole group, and the eagle group. I often wonder about the phase transition between the first two and the third groups, and what makes a kid an eagle versus a mole. “The little kids go to mouse group, the talented ones to eagle group, the stinky ones to mole group,” I’d imagine. But it turns out, rather uninterestingly, that the sorting is based on age. And I’m not saying this because my kid’s in the mole group.

But schools in Germany do quite an early selection into different streams. By the 5th grade, kids are sorted into “academic”, “vocational”, and “sporty” (I broadly paraphrase here, and might be missing a few other classifications: “artsy”, “jailbird”). The teachers have a strong, sometimes absolute, influence on the categorization. And it is quite tricky to shift from one sort to another down the line.

Which leads to interesting problems, as a recent conversation with a colleague revealed. Turns out, my colleague spent a sabbatical year outside of Germany when his daughter was in the 4th grade. When he comes back, his kid is uncategorized, because she wasn’t observed in the 4th grade. Moreover, this is in a state where the teachers’ categorization is absolute. So without the categorization there is no school ready to accept the kid! Suggested solution: have the child repeat fourth grade. Ouch. Ain’t he glad he wasn’t away for 5 years?

A loophole exists. Move to a state where the parents can decide on the sorting, get the kid in school, and move back. (Transfers between schools of the same sort are allowed.) But curricula vary widely across states. So for example in Bavaria, the kids learn German and Latin (!) in school, in other states, they learn German and English, German and French, German and Russian. So moving across states effectively involves “repeating” a grade.

It turned out ok for my friend, because the teachers decided to accept the kid with only a preliminary evaluation. But I think it is a bad thing overall to make moving such a hassle. There must be an economic theory correlating fluidity of the workforce to the output of the economy. Intuitively, it seems an economy should do better if the workforce can move, in zero time, where labor is most required. Specifically, for highly skilled people such as researchers, the hassle or impossibility of a move due to external constraints such as schooling can mean sub-optimal allocations of resources across the country.

ACM TECS now has page limits

I recently found out that ACM Transactions on Embedded Computing Systems now mandates that every submission must be at most 25 pages. I think it is not a good step. In the conference-centric worldview of computer science, we already have a tendency to omit details in order to fit ideas “perfectly” into somewhat arbitrarily imposed page limits. However, the argument always is that a more detailed version can be presented in an archival journal. By setting a somewhat arbitrary page limit, TECS is going to encourage a slew of papers that somehow all “just fit” into 25 pages, with some parts omitted “for lack of space.” I am not sure this is good for the field, or for the journal. I cannot come up with a convincing argument that every idea in embedded computing systems worth writing about can be written in 25 pages. 🙂

In the particular case, I asked my postdoc to look for a different journal, one that does not impose page limits.

Misconfigurations

I am in California for a week, visiting Berkeley and Los Angeles, and also catching up with friends and family in the area.

In talking to my friends in Silicon Valley, I was repeatedly struck by the dissonance between “academic” verification research I do, and the “real world” software engineering grunge that becomes as important, if not more important, than the pure functionality of the code.

For example, there is the issue of system configuration. When you deploy a software stack, say on the cloud, you not only have “your” code, but an entire ecosystem of servers, load balancers, database backends, etc. that must all work together. The magic glue that makes this happen is configuration options written in lengthy files, in somewhat ad hoc languages. Getting the configurations right at deployment, and maintaining their correctness through system and component upgrades is an art. And a nightmare.

It’s a nightmare because your entire system can crash because you have misconfigured your system, even though individual components (your application, the server) are individually perfect. In fact, misconfigurations are a significant reason for system downtimes.

The problem is old and important, but I am not sure it has ever been a hot area in academic research. I recall there was a nice paper by Nick Feamster and Hari Balakrishnan on BGP misconfigurations some years back, and more recently, I read a paper by Mona Attariyan and Jason Flinn on dynamic dependency tracking for debugging misconfigurations. Are there other projects I am missing?

A somewhat naive view is to consider the content of the configuration file as symbolic inputs and to apply symbolic execution techniques, generating a symbolic description of all configurations causing a failure (and by negation, the space of “safe” configurations). I doubt though if symbolic execution can be scaled to the system level. An alternative is to compute the forward dynamic slice of an error trace, projecting to the set of configuration variables. Both techniques are “low level”. It is not clear to me how semantic constraints can be captured in this way.

Finally, why isn’t there a lot more academic interest in the problem? Is it that deployment issues affecting large scale deployments don’t “show up” in most projects in an academic setting?

Adventures in Paperwork

Opening a bank account is not easy when you are jetlagged.

So we are in KL, running around getting all the paperwork in order. (You need one document registering your, and your families’, address with the city. A second document to state that the children claimed to reside in the address in the first document do indeed reside in the address stated in the first document. There is an entire section in the form dealing with illegitimate children… You take these two documents to a different office where you apply for a “Child allowance” from the state. A further different office takes that money back as part of income taxes.) Like most countries’ immigration laws, German rules are inconsistently circular. You need the document from the city office to get bank accounts. But no landlord will rent you a place without the paperwork and a bank account.

We got through the paperwork smoothly enough, thanks to the MPI admins who shepherded us around (“Coming through! Idiot foreigners!”). The only magical trick I got to show off was the use of an IPhone app to convert our heights and weights to the metric system at diverse offices.

Picture this: it’s our first week in Germany, we are all extremely jetlagged. The kids have been up all night. It’s noon = 3 am Los Angeles time, and we have just spent an hour in a government office. But I see a shiny bank building and decide to open an account.

I walk in. I explain this in broken German. Really broken German. I use “gelb” (= yellow) for “geld” (=money), explainging my need to store many, many, yellow things in the bank to a confused receptionist. Nevertheless, we are ushered into a small office, waiting for the bigger financial muscles to show up. We decide to release the kids in the room. At least, the damage will be contained. Tandra lies back for a catnap.

Soon a banker comes in. The room is a sea of crawling infant, loud running boy, sleepy wife, and documents. He looks at the state of affairs, tries to find the cat that brought all this in, and gives a sorry nod.

“What can I do for you?”

I explain my need for a bank account. He looks me over, disbelieving that I could ever have Actual Coins I would want to vaultize. But an epsilon money received is an epsilon money earned for the bank, so he decides, against all better judgment, to continue.

“What do you do?”

I start talking about Petri nets. Tandra gives me a withering look. I hand the man my Very First Visiting Card made in the excellent German tradition pointing out (a) professorship, (b) a doctoral degree. Me, I would have preferred the Wile E. Coyote simple style:

Wile E. Coyote

Genius

Have brain. Will travel.

But that template ist verboten. Little did I know the bureaucracy I unleashed.

You see, there are 700 different categories of professorships, and about double that of Ph.D. degrees. And the bank requires the exact classification to be stored with my account information. So we patiently start going over the list. “Informatik” is, of course, absent (or in hiding). I try to convince the guy that “Electronische Zauberer” should do. Nope. We get into semantic arguments about Mathematics, Platonism, and Naturwissenschaft. There is a simple “Doctor of Philosophy” but that, apparently, requires knowledge of, umm, philosophy. I can hear Tandra groaning in the background. I lose track of time, descending into a vortex of academic categorization.

I must have dozed off. When I wake up, I see Ritwik madly stamping the office wall with an official-looking bank stamp. And Rajit thoughtfully chewing on the banker’s trousers. The Germans hide their emotions well. Instead of suing me for irreparable sartorial damages, the financial magnate gives me a painful smile of understanding.

“Children,” he pronounced ruefully, “are better outside.”

Outside, yes. I could see what he meant. For these two, for sure outside of Germany, preferably outside the solar system. We looked at each other, men of the world. Understanding. Tandra’s snores filled the background.

We finally settle on “technische wissenschaft” as my exact expertise. Forms are filled out, signed. The banker mops his brow, exhausted. We walk out into the bright sunlight.

I realize, a few days later, that the large “S” sign for the bank is a generic sign for a whole set of banks. There is the Kreissparkasse, the Stadtsparkasse, the Foosparkasse. All they have in common is the “S” (presumably, for Sparkasse). I am reminded of the section from Monty Python’s Life of Brian:

Brian	Are you the Judean People's Front?
Reg	Fuck off.
Brian	What?
Reg	Judean People's Front. We're the People's Front of Judea. Judean
	People's front, caw.
Francis Wankers.
Brian	Can I join your group?
Reg	No. Piss off.
Brian	I didn't want to sell this stuff. It's only a job. I hate the Romans
	as much as anybody.
PFJ	Sssh. Ssssh, sssh, sssh, ssssh
Judith	Are you sure?
Brian	Oh. Dead sure... I hate the Romans already.
Reg	Listen. If you really wanted to join the PFJ, you'd have to really
	hate the Romans.
Brian	I do.
Reg	Oh yeah? How much?
Brian	A lot!
Reg	Right. You're in. Listen. The only people we hate more than the
	Romans are the fucking Judean People's Front.
PFJ	Yeah
Judith	Splitters.
Francis And the Judean Popular Peoples Front.
PFJ	Oh yeah. Splitters.
Loretta And the peoples Front of Judea.
PFJ	Splitters.
Reg	What?
Loretta The Peoples front of Judea. Splitters.
Reg	We're the Peoples front of Judea.
Loretta Oh. I thought we were the Popular Front.
Reg	Peoples Front.
Francis Whatever happened to the Popular Front, Reg?
Reg	He's over there.

Version 3.0: Debugging Deutschland

So we finally moved to Kaiserslautern, Germany.

Not an easy feat with a garage. A garage is an excellent device to make stuff disappear. Don’t know what to do with that huge carpet vacuum? Put it in the garage. How about the kitschy cakestand-bong combo from your hippie days? Garage. Drill bits? Ditto. Paint cans from 2005? You get the picture. It is very satisfying existentially. If a box is in the garage and nobody is there to see it, is it really there?

Except: it all bites back when you have to move. Unopened boxes from our 2004 move came marching out. Unused snorkeling gear. Enough Costco stuff to feed a family of 4 for a year (well, assuming the family survives the toxic brew the expired foodstuff has slowly transformed into over the years). Rajit’s “oh-so-cute” duck-shaped onesie (“he came home wearing that”). Ketchup-splattered tablecloth from Ritwik’s first birthday (“remember how he poured juice over his head?”).

Lesson: If you want to move, ever, don’t own a garage! You know the “dark matter” cosmologists keep looking for? Offer God a new home, make him move, and the stuff’ll pop out of his garage.

Anyhoo, we show up at the airport. Six large-ish suitcases. A car seat. A crib. Two clueless kids (“Yay, we’re going to Germany. Mommy, after we go to Germany, can we go to Chuck-e-Cheese?” and “Drool”, respectively). A wife. Me. A disbelieving Supershuttle driver. And our flight is late and we miss the connecting flight to Frankfurt.

Panic. But for once, the airline customer support comes in to the rescue. We get put on a direct LosAngeles Frankfurt flight. (The same flight I cheaply did not buy, since the tickets were more expensive than our LosAngeles-Boise-Iowa City-Rejkjavik-ferry-Bremerhaven-Frankfurt itinerary. Sweet, sweet, victory.)

The plane ride was usual and uneventful: screaming babies (Rajit won the “screamiest baby” contest), cramped spaces, strangely gelatinous food. Lost luggage. Yeah, we did lose our bags. I used to think that’s a Bad Thing. But it’s really an Airline-managed Door-to-Door Delivery Service. Saved me the hassle of moving a bunch of heavy things by myself. I’m surprised the airlines don’t already charge for lost luggage!

But it could be worse. The first email I checked was from my travel insurance company:

UPDATE 1: Health authorities recall another 152 million eggs linked to Salmonella infections in the US.

This on top, apparently, of the 228 million eggs already recalled. Oh http://www.eggsafety.org, you have done it again! Scooped the liberal mainstream media! So yeah, it could be worse! I could be eating buggy eggs!

Amir Pnueli

I was saddened to hear that Amir Pnueli passed away on November 2. The news came by email right as I was discussing one of his papers with my students. Amir was one of the intellectual giants in our community, and will be missed.

v2.0, and MPI

Various things, including the arrival of our second baby, kept me from the blog the past two months. But now that the baby is sleeping through the night, let me take a stab again. v2.0.

In the meantime, I have accepted an offer from the Max Planck Institute for Software Systems, and plan to move to Germany next year. MPI-SWS has an excellent group, and they’re going to grow over the next several years! If you work in the area of software systems, and are looking for a faculty position, please apply! If you want to work in the area of software systems, please apply to the graduate program at MPI!

What’s more, MPI is not the only place which is hiring: IST Austria, with Tom Henzinger as President, is hiring (“40-50 research groups by 2016”), and so is IMDEA, Madrid. IST has already hired Krishnendu Chatterjee. IMDEA hired a bunch of very capable PL/verification folks (including my postdoc Pierre Ganty), and will grow more. It is an exciting time to be in Europe, especially for verification/systems types.

Hello world!

Welcome to Unverified!

I am an associate professor of computer science at UCLA working in formal verification of systems (and the associated theory and engineering aspects).

I am starting this blog in a moment of madness (or a moment of clarity after one too many glass of wine), as a meeting place for the verification community. Please send me feedback, comments, flames, etc.