Frama-C A number of colleagues and I have been tasked with writing a summary of an article they published in 2010. Each of us has to do this for an article of theirs, that is. I chose the article whose long version title is \A Mergeable Interval Map" (link PDF available...
Read MoreThere won't be many changes in the value analysis' documentation in Nitrogen. For lack of time, the new options, some of which were alluded to in this blog, will remain in their \to be documented" state. But documenting them more fully can always be done here too once they are...
Read MoreDo two jobs, and do them well In the previous post, I used the command: $ cat log? | grep \N " | sort | uniq This may be an inefficient way to get a list of unique lines containing "N ". The command sort does not know that it...
Read MoreIntroduction In the first post in the obfuscated animated donut series my colleague Anne pointed out that: The alarm about : assert \valid(". -~:;=!*#$@"+tmp_7); seems strange because the analysis tells us that tmp_7 ∈ [0..40] at this point... How can this be valid ? It is only safe to use...
Read MoreThis post documents the steps I followed in order to finish verifying function compute(), picking up from there. Previously on this blog In last episode we had found that some sub-cubes in the search space appeared to lead to dangerous value sets for variable N. These sets were: N ∈...
Read More