Frama-C I would use a social network where the discussions are about the near future's zeitgeist. As they are, people just use them to discuss what is happening now (\what are you doing?") which does not have the same usefulness. Case in point: Christmas just came and went; presents given and...
Read MoreThis page where Microsoft Research's Z3 theorem prover is on sale for for just a bit less than $15 000 has come to my attention. This is interesting because Z3 is at the same time a free download. Note that the free download is covered by this license (executive summary:...
Read MoreI was previously complaining about the use of the word \prove" when describing either what Frama-C or another tool does to mean something other than what it means. But it seems we have come to the point over-confidence is actually expected lest readers get confused. In a submitted article one...
Read MoreMy colleagues are formidable. Over the last few days, three of them fixed four bugs in my code. And one of the fixes was a simple, obviously correct fix for the bug previously discussed here. In celebration of these terrific colleagues here is a new patchset for Nitrogen 20111001 patchlevel...
Read MoreCsmith as a static analyzer fuzzer A new version of Csmith, the generator of random defined C programs, was released a few days ago. This is the version that many functions in Frama-C Nitrogen were debugged against. Conversely a few bugs in the development versions of Csmith characterized by programs...
Read More