Menu
TrustInSoft’s Pascal Cuoq wins the prestigious honor of being an author of an influential paper that has stood the test of time
TrustInSoft’s very own Chief Scientist and co-founder Pascal Cuoq was recently awarded the Most Influential Paper of PLDI 2012 at the Programming Language Design and Implementation (PLDI) 2022 conference. The award is given to the authors of a research paper, submitted 10 years before, that has stood the test of time and continued to have an impact in the 10 years following its submission. TrustInSoft is very proud of this achievement and the award highlights the continued influence of this innovation on TrustInSoft Analyzer’s key functionalities. Read the story of how TrustInSoft Analyzer’s automated verification came to be thanks to this paper and the impact it continues to have on customers today in Pascal’s blog entry below.
Blog written by Pascal Cuoq
In 2011, Xuejun and John had published an article about automatically finding bugs in C compilers, using a tool they had named Csmith (incidentally, this article was published at PLDI 2011 and was itself judged “Most Influential” of that year at PLDI 2021). Csmith generates random C programs. Any particular generated C program is supposed to be deterministic, but it combines the operations allowed by C in a random manner that differs each time Csmith is invoked. A bug is found when one of the generated C programs produces a different result, when compiled with the target C compiler, than the result of the same program compiled by other C compilers used as reference.
After the publication of Xuejun and John’s PLDI 2011 article on Csmith, I myself had used Csmith to find bugs in the C value analysis that would evolve to be at the center of TrustInSoft’s product. As my own publication on this novel use of Csmith said at the time, “new functionality had to be implemented in the value analysis… to make it testable as a plain C interpreter” (See ‘Testing static analyzers with randomly generated programs’ in NFM 2012). Indeed, this research work had involved adding the initial prototype of an “interpreter” mode to the existing value analysis. The resulting C interpreter was able to print the result of the C program in a way that could be directly compared to the result of the execution of a binary produced by a reference C compiler for the same C program.
John approached me as he was preparing the PLDI 2012 article that would describe a complementary tool to be named C-reduce. C-Reduce takes a large C (or now C++) file that has a property of interest (such as triggering a compiler bug) and automatically produces a much smaller C/C++ file that has the same property. One missing piece for the puzzle was the problem of automatically verifying that the reduced C program does not exhibit undefined behavior. I was glad to tell him that the functionality was ready, and, if I am allowed to anthropomorphize it a bit, eager to prove useful in contexts other than the one for which it had been specially developed. In this first application beyond the original motivation, the “C interpreter” functionality would check that a C program, that indicates a compiler bug because it is defined, continues to be defined when bits of the program are removed in an automated process.
C-reduce itself has grown beyond the “minimum viable research prototype” that was necessary for a scientific publication and has become a widely-used full-featured open-source tool for anyone who works on programs that process C or C++ programs as inputs. The engineering team at TrustInSoft regularly uses it in the context of the development of TrustInSoft Analyzer.
In the ten years that have elapsed, the “C interpreter” functionality has been greatly expanded at TrustInSoft, becoming seamlessly applicable to programs that call C or POSIX standard functions. This functionality has proved its general usefulness by helping numerous customers to get immediate results with very little human investment, by providing a way to take advantage of existing tests in order to get analysis results without false positives. Today, engineers at TrustInSoft’s customer companies apply this functionality to their existing test drivers, and without any analysis tuning, detect undefined behavior in the executions defined by the test drivers without false negatives or false positives.
Learn more about TrustInSoft Analyzer by visiting our product page.
