Tag Archives: position

The case for formal verification of existing software
Pascal Cuoq on 2 September 2013

Perry E. Metzger takes a look at formal verification [removed dead link]. This is good stuff; there is a lot to agree with here. However agreeing with Perry's post alone would not make a very interesting counterpoint. If agreeing was the only thing I intended to do I might even...

Read More

Arithmetic overflows in Fluorine
Pascal Cuoq on 9 July 2013

There is a C quiz in the middle of this post, lost in the middle of all the reminiscing. A history of arithmetic overflows in Frama-C From the very beginnings in 2005, until after the first Open Source release in 2008, Frama-C's value analysis was assuming that all arithmetic overflows...

Read More

On writing a dedicated model-checker for the RERS competition
Pascal Cuoq on 24 August 2012

In recent posts I have shown that Frama-C's value analysis could answer many reachability questions and some questions that weren't originally phrased as reachability questions about the programs in the RERS competition. If you are vaguely familiar with the internals of Frama-C's value analysis and if you tried analyzing some...

Read More

assume and assert
Pascal Cuoq on 3 August 2012

The previous post links to a message [removed dead link] from Michał Moskal highlighting ACSL constructs that the VCC developers at Microsoft Research had either regretted the absence of or found superfluous while re-designing their own annotation language for VCC. In that e-mail the third item in the “missing” list...

Read More

Oxygen is stricter about types and why you should get used to it
Pascal Cuoq on 27 July 2012

I have just sent a list of changewishes (1 2) to a static analysis competition mailing-list and that reminded me of a blog post I had to write on the strictness of the type-checker in upcoming Frama-C release Oxygen. This is the blog post. This post is not about uninitialized...

Read More