Whiley v0.5.3 Released!

And, finally, another release of Whiley is upon us after waiting! As usual, there are a range of known issues and limitations. But, the main improvements are:

Boogie Support.  Included within the distribution is a backend for verification using Boogie and Z3.  This significantly improves the verification capability with Whiley.

In addition, there have . . . → Read More: Whiley v0.5.3 Released!

Verifying Bubble Sort in Whiley

Bubble sort is a classic sorting algorithm with lots of well-known issues. It’s been a long time since I thought much about this algorithm. But, it turns out to be an interesting verification example for Whiley, as it has some interesting loop invariants. The algorithm is pretty simple: it loops through an array swapping . . . → Read More: Verifying Bubble Sort in Whiley

Whiley Demo @ Oracle Labs!!

Recently, I gave a demo of Whiley at Oracle Labs in Brisbane which they have kindly put up on YouTube:

The actual demo itself starts around 11:30s, so you might want to skip on to that.

The talk was part of a series of talks I did at various locations across . . . → Read More: Whiley Demo @ Oracle Labs!!

Property Syntax in Whiley

Recently, I gave a demo which showed off thew new “Property Syntax” in Whiley. Whilst this is still in the devel branch it will make its way, soon enough, into the next release. I thought it would be interesting to give a quick taste of the syntax.

To understand the purpose of properties, let’s . . . → Read More: Property Syntax in Whiley

Contractive and Uninhabited Types in Whiley

An interesting feature of Whiley is that it supports true recursive types.  These are surprisingly tricky to get right, and recently we came across some interesting examples that the Whiley compiler should (but doesn’t) check for.

Recursive Types

The following illustrates the syntax for recursive types in Whiley:

type Link is {any data, LinkedList . . . → Read More: Contractive and Uninhabited Types in Whiley

Eclipse Plugin v0.1.1 Released

After the recent release of Whiley v0.3.22 which updated the language syntax, I have now updated the Eclipse plugin accordingly.  See this page for more on installing the plugin from within Eclipse.

Whiley v0.3.21 Released!

This is a slightly quicker release than usual, with only a few relatively minor fixes and refactorings, etc:

Factored JVM Bytecode library into a separate project, called Jasm Various bug fixes mostly related to verification.  See here for the complete list.

I’ve also been working quite a lot on the Eclipse plugin, and will . . . → Read More: Whiley v0.3.21 Released!

Whiley Features in the Dominion Post!

Today’s edition of the Dominion Post (Wellington’s Local Newspaper) features a nice article on Whiley:

Obviously, I’m very excited to see Whiley being talked about in our local newspaper, and I think the article does a nice job of it.  There is also an electronic version as . . . → Read More: Whiley Features in the Dominion Post!

Profiling Field Initialisation in Java

Recently, I attended the annual Conference on Runtime Verification (RV2012) and gave a talk entitled “Profiling Field Initialisation in Java” (slides for the talk are here, and the paper itself is here). This is the work of my PhD student, Stephen Nelson, and he should take all the credit for the gory details. However, . . . → Read More: Profiling Field Initialisation in Java

Whiley Interview on VBC 88.3FM

Recently, I was on VBC 88.3FM (Victoria University’s Student Radio) giving a 60s “speed summary” of my research, and generally chatting about some tech stuff.  The station has been interviewing a whole range of people at the university to raise awareness of what research is going on.  Anyhow, I agreed to do the interview which . . . → Read More: Whiley Interview on VBC 88.3FM