-
Why Isn’t C Memory Safe Yet?
Memory safety errors in C/C++ code include null pointer dereferences, out-of-bounds array accesses, use after free, double free, etc. Taken together, these bugs are extremely costly since they are at the root of a substantial fraction of all security vulnerabilities. At the same time, lots of nice research has been done on memory safety solutions…
-
The Last Mile for a Verification Problem
A few weeks ago my student Lu Zhao defended his PhD thesis and we were lucky to get his external committee member, Magnus Myreen, to attend in person since he was in the USA anyway for a meeting. While he was out here, Magnus gave a talk on some not-yet-published work that is really cool.…
-
When Will Software Verification Matter?
When will average people start to use formally verified software? Let me be clear right from the start that I’m not talking about software that has been subjected to static analysis or about software that implements proved-correct algorithms, but rather about software whose functional correctness has been verified at the implementation level in a way…
-
Software Testing Using Function/Inverse Pairs
One of the hardest problems in software testing is finding convenient, strong oracles—programs that can tell us whether the software under test worked correctly. Weak oracles, such as checking to make sure a program doesn’t crash, are always available, but not always of much use. An example of a strong oracle would be a reference…
-
Udacity Visit
Yesterday I took a day trip to Palo Alto to visit Udacity where I’m getting ready to teach a course on software testing. The goal was to become familiar with the recording setup, hash out any infrastructure issues, and try to refine my course content–which right now is just a collection of rough notes. Originally I had…
-
Harris Wash, Zebra and Tunnel Slot Canyons
[nggallery id=52]
-
Does Portable Byte-Order Code Optimize?
When reading data whose byte-ordering may differ from the host computer’s, Rob Pike advocates writing portable code as opposed to using #ifdefs to optimize the case where the encoded data’s byte ordering matches the host. His arguments seem reasonable and it’s definitely a win if the compiler can transparently recognize the useless data extraction operations…
-
57 Small Programs that Crash Compilers
It’s not clear how many people enjoy looking at programs that make compilers crash — but this post is for them (and me). Our paper on producing reduced test cases for compiler bugs contained a large table of results for crash bugs. Below are all of C-Reduce’s reduced programs for those bugs. Can we conclude…
-
New Paper on Test-Case Reduction
For about the last four years my group has struggled with the problem of taking a large program that makes a compiler do something bad (crash, run forever, generate incorrect code) and turning it into a minimum-sized program that elicits the same bad behavior. Delta is a great tool but it does not entirely solve…
-
Happy Canyon
[nggallery id=51] Although Happy Canyon is a giant drainage occupying something like 90 square miles of southern Utah, it doesn’t get a lot of visitors. First, Happy is fairly remote and not in any of the national parks or recreation areas. Second, it is well-protected by cliffs, with only about five ways in or out.…