David J. Pearce (Blog)

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:

Dafny: An Automatic Program Verifier for Functional Correctness

Monday, June 7th, 2010

So, last week the pl reading group chose to read this paper by Rustan Leino. Ignoring the fact that a number of people in our group are interested in this area, Rustan had recently given a presentation on Dafny here (his slides are here) and this was reason we chose this paper.