David J. Pearce (Blog)

Language Designers ... who wait?

Thursday, July 22nd, 2010

Someone recently pointed me to the Rust programming language which has some very nice features, although it’s still in early stage development. In particular, the system statically prevents null pointer errors, and does not permit dangling pointers.

On Object-Oriented Programming

Thursday, July 15th, 2010

There’s an interesting interview with Ralph Johnson and Joe Armstrong over at QCon. They’re talking generally about whether OOP has been successful, and reflecting on the last few decades. A few things from the interview caught my eye.

Finding Bugs in the Real World

Thursday, July 8th, 2010

There’s a really interesting article over on CACM about static analysis in the real world. Here’s the Link. The article is a report from experiences gained in the commercialisation of a tool by Coverity which uses static code analysis to find bugs.

Kiwi Language Creator Acknowledged!

Monday, July 5th, 2010

The Dom Post ran a short article over the weekend on kiwi Ross Ihaka, about the R programming language which he created along with Robert Gentleman at the University of Auckland.

Example: Sum Over a Positive List

Wednesday, June 30th, 2010

So, here’s the first Whiley programming example. Obviously, it’s pretty simple as Whiley is not quite ready for big code just yet. The idea is to compute the sum of a positive list which, of course, will give you a positive number.

What is Extended Static Checking?

Saturday, June 26th, 2010

Extended Static Checking (ESC) is the main technique used in Whiley. *But, what is it? *Since there isn’t a huge amount of information available on the web, I thought some discussion about this would be useful.

Rich Hickey on Clojure (SE Radio)

Wednesday, June 23rd, 2010

I’ve just been listening to an interesting interview with Rich Hickery on Clojure over at SE Radio. I’m a big fan of Clojure, since it shares a lot of similar ideas with Whiley (really, it does … trust me :).

The Trouble with Quantifier Instantiation in an SMT Solver? Triggers.

Tuesday, June 22nd, 2010

So, i’ve been recently working through the quantifier instantiation mechanism in wyone. This is a tricky, yet important topic. There’s been a lot of interesting research in this area as well (see further reading below for some examples), although I found the papers often hard work at times.

Experimental Security Analysis of a Modern Automobile

Tuesday, June 15th, 2010

Another good paper I found recently was the following: “Experimental Security Analysis of a Modern Automobile”, Hoscher, Czeskis, et al. In Proceedings of IEEE Symposium on Security and Privacy, 2010. [PDF]

Formal Methods: To the Moon and Back!

Thursday, June 10th, 2010

I recently came across a rather interesting presentation by Gerard Holzmann (author of the SPIN model checker) who’s currently working for NASA’s Jet Propulsion Lab, and previously worked at Bell Labs: