please welcome jStar

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

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!

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

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...

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

jStar webpage

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

Check this out...