Frama-C Perhaps you are looking for something to do pending the upcoming release of Frama-C (someone called it \Nitrozen" once by accident in a commit message. I would like the name to stick but I anticipate it won't)… Or you are already a serious user of the value analysis plug-in or...
Read MoreA 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 MoreMany OCaml programmers use it because it offers a reasonable (to them) compromise between expressivity and control over resources use. Serious OCaml users are often heard complaining about relatively simple optimizations that the compiler does not have. But this reveals as much of the kind of programmers that end up...
Read MoreA little while ago, I was commenting somewhere that Forth had the ultimate control structure, the BEGIN (1) WHILE (2) REPEAT construction. (1) and (2) are holes to be filled with programs. WHILE takes an evaluated condition from the stack, so that (1) can usually be divided into (1a): do...
Read MoreCsmith testing A typical Frama-C Csmith testing script repeats four actions in an infinite loop: getting a random program from Csmith; compiling and executing it; analyzing it with Frama-C; using the results from step 3, possibly together with those of step 2, to determine whether the program reveals something that...
Read More