Tag Archives: obviously-terminates

Participating in the RERS 2012 competition: liveness questions
Pascal Cuoq on 20 August 2012

This third installment discusses the diagnosis of liveness properties of particular C programs, using Frama-C's value analysis, for the RERS 2012 competition. [Note added in September 2012: the diagnostic found for the example in this post disagrees with the diagnostic found later and sent to the competition organizers. I am...

Read More

To finish on termination
Pascal Cuoq on 8 June 2012

Enthusiastic reactions to the previous post about verifying the termination of a C program with Frama-C's value analysis lead me to write this post-scriptum. On detecting both termination and non-termination The scheme I outlined in the previous post can only confirm the termination of the program. If the program does...

Read More

Minimizing the number of alarms emitted by the value analysis
Pascal Cuoq on 12 March 2012

This blog post describes for the first time some options that became available in Nitrogen, continuing this series. This post also offers a benchmark but the results of this benchmark cannot be reproduced with Nitrogen. They should be reproducible with the next version of Frama-C. Alarms false alarms and redundant...

Read More