Space Invader @ East London Massive

please welcome jStar

2010-03-30T09:19:00.000-07:00

Maybe it was the great weather in Cyprus last week at ETAPS, maybe something else. But yes, jStar is now out! Some great news come with this.

1st great news: it's finally out in the wild...

2nd great news: it's released on BSD license. So do whatever you like with it!

3rd great news: this is a first really basic release. Maybe alpha maybe beta. And what is great about it is that there is much room for improvement. So this is the great opportunity you were waiting for to jump into the community of people actively developing tools for separation logic. So have some fun with it and let us know of any good progress so that we can make them available to the world.

And btw you can download jStar from here

P.S.: we're keen on hear any feedback you may have!

Applying bi-abduction to Java memory leaks

2009-10-27T14:44:00.000-07:00

Ok guys, here there is a new idea. Well, new for you at least. Definitely not for Ivana and me that have been thinking this for quite some time now. But recently, we decided (finally!!) to write it down in a draft paper (currently submitted). It's yet another brand-new application of bi-abduction (these days is not surprising, isn't it?). This time is all about detecting objects which are allocated, not used anymore in the program, but which cannot be garbage collected (sometimes called Java memory leaks). I quite like the idea and I thought it was time to put it out there...

Here there is the draft, hope you enjoy it....

New funding for JStar!

2009-10-02T08:19:00.000-07:00

Great News! EPSRC is going to fund Dino and Matt research on jStar for the next three years. The recent grant has been announced also in the Times Higher Education magazine.
Have a look here.

Abduction in Seoul

2009-08-22T03:28:00.000-07:00

Abductor is going to Seoul in the winter. The paper

Compositional Resource Invariant Synthesis
Cristiano Calcagno, Dino Distefano, and Viktor Vafeiadis

as been accepted for APLAS 2009.

Bi-Abduction has opened his way to concurrency!

BTW, Abductor is also going to Italy and France and Germany in September. I'll give seminars on bi-abduction in Genova, Grenoble, and Saarbrücken.

Get ready for for the beach...

2009-06-17T17:03:00.000-07:00

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!

2009-06-01T13:34:00.000-07:00

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

jStar webpage

2009-05-11T07:34:00.000-07:00

jStar has a now a web-page. Soon it will feature also a distribution of the tool!

Check this out...

Looking at different kinds of reasoning

2009-03-15T16:23:00.000-07:00

Several members of the East London Massive (and of course Space Invader too) will go to Cambridge this week for this exciting workshop on reasoning: Frontiers of Computational Reasoning. What sounds cool is the mixture of all sorts of reasoning. I'm really looking forward to that.

Space Invader in Argentina

2009-02-11T07:54:00.000-08:00

After Savannah few weeks ago, Space Invader will be soon seen in Rio Cuarto (Argentina) for the first time. For this invasion he'll be supported by good part of the East London Massive.

Rumors say that Space Invader's cousin jStar may also show up...

I'm really looking forward for that, it looks like it's gonna be great fun!

Space Invader in Bangalore

2008-12-01T16:13:00.000-08:00

Space Invader is going back to Bangalore!!
Dino is gonna give an invited talk on Space Invader at APLAS 2008!

If you are in the neighborhood just try not to miss it...

Space Invader, high-speed and electro music...

2008-11-03T17:24:00.001-08:00

I heard my friend Dario has now a super racer car and drives too fast. My friend J. instead would just say: "you're out of your mind!" if - a year ago- I'd have told him what Space Invader would be up to nowadays. This is despite the fact that my friend L. claims that space invaders are smoking grass. Anyhow, no matter what, just gazing at the exciting brand new result we've just crafted in the last few months for Space Invader, it becomes apparent that it's definitely far beyond what we could have imagined a year ago, even when having endless pleasure in a limousine.

Wanna know more? Come to the rendez-vous at POPL 2009, read
Compositional Shape Analysis by means of Bi-Abduction and don't forget to wear your sunglasses at night.

Classical BI and the market crisis

2008-10-13T10:37:00.000-07:00

If you are a completely confused about the global crisis affecting the market (like myself) then
have a look at James's explanation written in his brand-new classical version of the logic BI (in the picture).

Obvious, isn'it?

Abducting the Awards night...

2008-09-25T03:19:00.000-07:00

Another breaking news folks.
Space Invader is gonna invade the Awards night on Oct 23th!
Space Invader is one of the finalists for the Times Higher Education Awards 2008 in the category Project of the Year.

Until then, cross your fingers.

And the winner is....

Space Invader 1.0 unleashed

2008-09-24T07:20:00.000-07:00

Breaking news folks!
Space Invader version described in the paper

Scalable Shape Analysis for Systems Code (CAV 2008)

has been finally released. Get it from www.eastlondonmassive.org

Enjoy it!

New funding for Space Invader

2008-08-10T17:04:00.000-07:00

Great news! EPSRC decided to provide funding for a new Space Invader's adventure. The project, called Adaptive Heap Analysis, is meant to bring to the next level the basic ideas described initially in Shape Analysis for Composite Data Structures (appeared in CAV 2007).

New exciting developments are coming! Stay tuned....

Abduction by Space Invader

2008-07-30T01:40:00.000-07:00

Alarming news has been reported yesterday by The Sun (citing a recent study carried out by scientists at University of London ): Space Invader has been reported as unexpectedly abducting vast quantities of open source code in East London. Authorities recommend high caution when walking at night in the capital, and in particular, in the popular Shoreditch area. The study cited by the tabloid has been submitted for publication and is currently being reviewed by world experts in the field.

P.S.: Drop me a line if you want to have a copy of the study.

Space Invader's Summer Tour 2008

2008-06-25T01:59:00.000-07:00

19 Jun - Microsoft, Cambridge, UK (Dino)
24 Jun - Bangalore, India (Hongseok)
30 Jun - Harvard, Cambridge, USA (Dino)
02 Jul - CMU, Pittsburgh, USA (Dino)
07 Jul - Paphos, Cyprus (Dino)
09 Jul - Princeton, USA (Peter)
12 Jul - Princeton, USA (Hongseok)
14 Jul - Princeton, USA (Hongseok)
17 Jul - Valencia, Spain (Peter)
02 Sep - Enschede, The Netherlands (Dino)
04 Sep - Eindhoven, The Nethrlands (Dino)

Don't miss it....

Just born jStar goes to the US

2008-05-06T02:41:00.000-07:00

Very exciting news. Very soon JStar will fly to the US. The paper

jStar: Towards practical verification for Java.
Dino Distefano and Matthew Parkinson.

has been accepted for publication at OOPSLA 2008.

Space Invader towards new remote frontiers

2008-03-31T15:22:00.001-07:00

Since last summer (I remember, shortly after CAV) we've been working to some new -quite radical and not yet announced- developments for Space Invader which really really excite me! In the last few weeks, we have improved this new technique. I feel it's getting closer and closer...

Be prepared.... stay tuned...

Space Invader in Princeton

2008-03-27T10:41:00.000-07:00

The new paper on join

Scalable Shape Analysis For Systems Code.
Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano and Peter O'Hearn.

has been accepted for publication in CAV 2008.

Space Invader is gonna invade Princeton!

jStar is born

2008-03-22T06:50:00.000-07:00

A Java cousin of Space Invader is just born. It's called jStar and it aims at the verification of tricky Java programs. Details in this paper:

jStar: Towards practical verification for Java.
Dino Distefano and Matthew Parkinson.
Submitted.

Invited talk on Space Invader

2008-02-01T09:14:00.000-08:00

Hongseok is going to give an invited talk on Space Invader at Systems Software Verification (SSV 08) in Sydney.

If you are in the Sydney area don't miss it!

Paper on join

2008-01-30T03:14:00.000-08:00

There is a new paper giving the details on the join operator which allows high scalability in shape analysis.

Scalable Shape Analysis For Systems Code.
Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano and Peter O'Hearn.
To appear in CAV 2008.

Breaking barriers: 10000 line of code and beyond

2007-11-26T16:03:00.000-08:00

Space Invader has climbed and conquered the peak of 10000 line of code! Only a year ago breaking this barrier was considered to be no more than a dream for deep heap analyses. Today it's reality.

Find out more (how/where/when) in this new technical report!

Next barrier to break? Fifty-thousand line....

Wanna join the Terminator/Slayer team?

2007-10-14T13:05:00.000-07:00

If you are interested in a position as a developer for the Terminator/SLAyer project, there is an exiting opening at Microsoft Research Cambridge. Have a look at this

Space invading Sicily

2007-09-28T03:20:00.000-07:00

For few days the East London Massive and friends have been exploring the buzzing streets of Catania (east coast of Sicily). Lots of fish, wine and sun helped us with our brainstorming about new directions in separation logic, space invader, small foot, semantics,...

Invited talks

2007-09-12T02:21:00.000-07:00

After giving an invited talk on new advances in concurrent separation logic at Concur 2007 in Lisbon (Portugal), Peter is going to give a Space Invader/Smallfoot related invited talk at The 2007 International Symposium on Memory Management, in Montrel (Canada).

2007-07-26T06:36:00.000-07:00

Dino giving his Space Invader talk at CAV 2007 in Berlin.

SeparationFest

2007-06-27T16:46:00.000-07:00

John Reynolds is receiving an honorary degree from Queen Mary on 17 July for his signal contributions to programming languages.
The day after, John's celebration will continue with SeparationFest, a one-day workshop on Separation Logic (again at Queen Mary).
Tony Hoare will give a keynote talk on Separation Logic and Declarative Semantics.

SeparationFeest is open to everybody. Don't miss it! Come and join us...

New funding for Space Invader

2007-06-05T18:11:00.000-07:00

EPSRC and Royal Academy of Engineering have decided to sponsor further development of Space Invader!
Hongseok has been awarded the Advanced Fellowship from EPSRC and Dino has been awarded the Royal Academy of Engineering Research Fellowship!

New exciting time is coming for Space Invader!

Next July it's Berlin time

2007-05-12T16:27:00.000-07:00

I've been in Berlin just few times in my life but it has been always amazingly good. It's definetely a great city. Especially during summer.
Next July there are several reasons why you really wanna be there. Here some suggestions in random order

1. A Space Invader paper has been accepted for publication in CAV 2007:

Shape analysis for composite data structures.
Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies and Hongseok Yang.

2. There is a great Symposium associated with CAV which you cannot miss: AHA 2007

3. Byron's invited talk at CAV 2007

Unfortunately not everything is perfect. There is a problem....
what I considered to be the greatest event in July turned out to be actually a disappointment!
The Love Parade! It was really a must, but unfortunately the latest news says that, this year for the first time, it's not gonna happen in Berlin!!!!! How unfortunate is that? Is CAV involved in this???? Too bad...

Footprint analysis gets to Copenhagen

2007-05-07T15:40:00.000-07:00

Beside Berlin, it seems that this summer Space Invader and the East London Massive will visit Copenhagen as well! Our Footprint analysis paper:

Footprint Analysis: A Shape Analysis that Discovers Preconditions.
C Calcagno, D Distefano, PW O'Hearn and H Yang.

has been accepted for publication in the International Static Analysis Symposium. The tech report version can be found here

Queen Mary Tech Report RR-07-02, April 2007.

A new paper!

2007-03-29T10:50:00.000-07:00

A new Space Invader paper has been accepted in the 19th International Conference on Computer Aided Verification (CAV):

Shape analysis for composite data structures.
Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies and Hongseok Yang.

See below for the tech report version.

Space Inveder looks at Apache

2007-02-24T13:42:00.000-08:00

This is Apache seen with Space Invader's eyes...

Teaching Space Invader to adapt

2007-02-01T13:29:00.000-08:00

Hongseok and Josh friendly fighting for the best strategy to teach Space Invader to adapt to many unpredictable and dangerous data structures it will encounter in his mission to invade the galaxy of device drivers....

Results? Two new papers describing what Space Invader has learned during his training across Europe (London, Cambridge, Venice and Nice):

Footprint Analysis: A Shape Analysis that Discovers Preconditions.
Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn and Hongseok Yang.

Shape analysis for composite data structures.
Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies and Hongseok Yang.
Microsoft Research Tech Report TR-2007-13

le Massive et la Cote D'Azur

2007-01-20T12:13:00.000-08:00

Most of the Massive invaded Nice last week for POPL and VMCAI.
Hongseok impressed VMCAI's audience with a wicked keynote invited talk on very recent Space Invader developments.
An unforgettable talk...
look here for Hongseok's slides...

Bee has some nice snapshots/stiries of the long nights the Massive spent in a bar in the small streets of the old city centre...

Commercial tavern

2006-12-09T04:56:00.000-08:00

the Space Invaders after few beers at the Commercial Tavern one of our favorite pubs in Shoreditch (East London)

Space Invader in Freiburg

2006-12-06T12:39:00.000-08:00

This week Dino went to Freiburg visiting Andreas Podelski. He gave a talk on Space Invader's latest exiting developments.
After that, two intense days of Space Invader brainstorming at the whiteboard followed...

Human Space Invader

2006-11-21T10:27:00.000-08:00

Look at this very cool video I discovered by chance.
Made by Guillaume Reymond who used 67 people as pixel and moved them around for 4 hours and
collecting 390 images.

Human Space Invader

More info here

Slayer

2006-11-20T16:15:00.000-08:00

Space Invader's cousin Slayer has now a web-site...

the East London Massive goes to Venice

2006-10-29T14:14:00.000-08:00

Space Invader and Terminator met in Venice last week.
everyday on the agenda: brainstorming, coffee, hacking, beer, messing around, more coffee, more beer, more hacking, more brainstorming....
wanna know more? check this out...

Smallfoot's celebration

2006-10-22T07:17:00.000-07:00

the east london massive celebrating new support for Smallfoot in a little bar somewhere
in the small streets of Genova. Tequila!

Space Invader's papers

2006-10-20T19:44:00.000-07:00

and of course you are desperately looking for the Space Invader papers.... here you go

Space Invader comes from outer space to join us and have some fun. This is the
original Space Invader paper:
A Local Shape Analysis Based on Separation Logic...
(aka TACAS 2006 paper).

then, one night in September 2005, in a pub in Cambridge, Space Invader met Terminator and.... Mutant was born
(aka Mutant paper or CAV 2006 paper). Some pictures while making Mutant in Peter's house

without warning Space Invader decided to leap beyond the reachable galaxy and we got the space invader for pointer arithmetic
(aka malloc paper or SAS 2006 paper)

and then several other papers have followed:

Scalable Shape Analysis for System Code (CAV 2008)

Shape Analysis for Composite Data Structures (CAV 2007)

Footprint Analysis: A Shape Analysis that Discovers Preconditions (SAS 2007)

Space Invader goes mobile clubbing

2006-10-13T13:08:00.000-07:00

jumping, shaking, bumping altogether.... in silence... totally space madness... 10 points!

check Peter's videos of that night...

who are these crazy people?
crazy Space Invader

prelude

2006-10-13T12:39:00.000-07:00

east london massive the invasion starts from here

attack!