Get ready for for the beach...

Folks: two new SpaceInvader papers to read at the beach under a palm tree with a super-cold beer or lemonade and lots of ice!




Compositional Resource Invariant Synthesis.
This is a draft paper we just submitted. It describes an algorithm for automatically synthesizing resource invariants in a thread-modular way.
So you can prove concurrent programs compositionally. Sounds good isn'it?

The other one is an extended abstract for my invited talk at FMICS 2009.
I started by thinking to send just the usual boring abstract. Then talking to Peter in some bar in Baltimore he convinced me to add more stuff. Then I started to add stuff, and then more stuff... and the abstract blew-up to the current state. Fortunately I was two days late after the deadline so I really had to stop! Anyway, this is so easy that you can read it even with two or three super-cold beers and be so fast that the third beer is still cold! It's just a easy summary of bi-abduction and some practical experience in applying them to big program. Here it is:

Attacking Large Industrial Code with Bi-Abductive Inference


Enjoy!

Celebrating Richard!

The East London Massive and friends are gathering on the English coast (in Aldeburgh) to celabrate the 65th birthday of one of the historic pillars of the Massive: Richard Bornat!

It's gonna be all about proving programs and brainstorming on better way of proving programs... although I must admit that dreaming of coming up with a better proof for
in-place list reversal than Richard's one (check it out) it's realistically hopeless. That's definitely unbeatable!

More info here