Blog

Tag Archives: benchmarks

SATE VI Workshop: Frama-C satisfies the Ockham Criteria
André Maroneze on 2 October 2019

During the SATE VI Workshop, organized by the NIST SAMATE project, Frama-C was confirmed as having satisfied the Ockham criteria for sound analysis tools. Frama-C previously satisfied the SATE V Ockham criteria (2013-2016) and found hundreds of errors in the test material. We reported in this blog about our analysis...

Read More

Finding unexpected bugs in the DARPA CGC corpus
André Maroneze on 26 February 2019

Recently, we’ve been running Frama-C/Eva on the DARPA challenges from the SATE VI Classic track tool evaluation, organized by NIST. The C programs come from a Linux-compatible port of the DARPA Cyber Grand Challenge. The port was made by Trail of Bits and used as one of the evaluation sets...

Read More

Frama-C/Eva in SATE VI with Juliet 1.3
André Maroneze on 15 November 2018

Frama-C chose to participate in the SATE VI Ockham Sound Analysis Criteria. With the upcoming Frama-C 18 (Argon) release, results can be reproduced using the open source version of the Eva plug-in. This post briefly presents SATE, the Juliet test suite, and the results obtained with Frama-C 18. We then...

Read More

Short, difficult programs
Pascal Cuoq on 2 November 2012

When researchers start claiming that they have a sound and complete analyzer for predicting whether a program statement is reachable, it is time to build a database of interesting programs. Goldbach's conjecture My long-time favorite is a C program that verifies Goldbach's conjecture (actual program left as an exercise to...

Read More

Exact Gap Computation for Code Coverage Metrics in ISO-C
Pascal Cuoq on 16 October 2012

Comparing static analysis tools is (still) difficult Earlier this year of 2012, some of my colleagues and I took the opportunity to point out that, as a research community, we are not doing a satisfactory job of comparing static analysis tools. This article and blog post were concerned with independent...

Read More