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. We want Whiley to realise this and correct us if there’s a . . . → Read More: Example: Sum Over a Positive List
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.
The term “static” implies that ESC is applied at Compile-Time — that is, when a program is constructed, . . . → Read More: What is Extended Static Checking?
The abstracts from the Dagstuhl seminar I recently attended are now available on the seminar site — there’s even a photo! The seminar was a lot of fun, and I encourage everyone who gets the chance to go along. The idea is that you get a bunch of people together, and then brainstorm for . . . → Read More: Whiley at Dagstuhl
Well, finally, after a lot of effort I have a new release of the Whiley Development Kit. To get it, follow the download links on the left.
The major difference over the previous version is that the theorem prover has been almost completely rewritten. So, while on the surface it might not appear much . . . → Read More: Whiley v0.2.7 Released!
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 :). Anyway, Clojure provides the notion of pure functions and values, as Whiley does. The . . . → Read More: Rich Hickey on Clojure (SE Radio)
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.
Anyway, the basic idea is pretty . . . → Read More: The Trouble with Quantifier Instantiation in an SMT Solver? Triggers.
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]
What I found particularly interesting was the discussion of the computing setup on a modern car. Here’s some info:
Most modern cars feature . . . → Read More: Experimental Security Analysis of a Modern Automobile
Testing that the Whiley-to-Java Compiler (wyjc) functions correctly is something of a challenge. We must, as usual, check that the correct (JVM) code is generated, and that the type checker is accepting/rejecting the right programs. However, we must also test that the theorem prover wyone is accepting / rejecting the right programs as well. . . . → Read More: An Overview of Whiley’s Testing Framework
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:
One of the things he talks about his is a possible moon-landing in 2019, and the software required compared with that of . . . → Read More: Formal Methods: To the Moon and Back!
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. Unfortunately, I . . . → Read More: Dafny: An Automatic Program Verifier for Functional Correctness