Software bugs // why should you care
There are still open challenges in automated code verification
The summary of a talk given by Elizabeth Paul Green, a lecturer in computer science at the University of Edinburgh. The main points covered in the talk are:
1. Green expresses her distrust in computers and software systems due to historical software failures that have resulted in disasters, injuries, and loss of lives.
2. She explains how software is becoming increasingly complex, making it difficult for humans to reason about and verify its correctness.
3. Green draws an analogy between Sherlock Holmes’s logical reasoning skills and the way SAT solvers work, using a combination of proof-theoretic and model-theoretic reasoning to verify software properties.
4. She discusses the field of automated verification, where tools are built to translate questions about software behavior into logical statements that can be checked by SAT solvers.
5. Green highlights examples of successful applications of automated verification tools in industry, such as Microsoft’s SLAM tool for detecting crashes and Amazon’s zelCo tool for checking data access permissions.
6. However, she acknowledges that there are still open challenges in automated verification, such as scaling to larger systems, asking the right questions, making correct assumptions, and gaining wider adoption from software developers.
7. In the end, Green loosens her distrust in computers, but only if their desired behavior is fully specified and mathematically proven to satisfy that specification under reasonable assumptions.
