Reading
Is correctness relevant for systems? Somewhat! We’re reading two papers today. First is one of the most successful academic software correctness projects of the last 20 years; the KLEE project is still going strong, and 250+ published papers have used or extended it. Second is an example of how formal verification ideas make it into production at Amazon.
-
“KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs”, Cristian Cadar, Daniel Dunbar, Dawson Engler (OSDI 2008)
-
“Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3”, James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, Andrew Warfield (SOSP 2021)
Also, before class, refresh your memory on Kangaroo—we may discuss it for a couple minutes.
Reading questions
KLEE is a single symbolic execution tool, whereas the Amazon paper describes multiple tools, each fit for a single purpose. Which of these general approaches more attracts you?