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!