Looking for Missed Alarm Bugs in a Formal Verification Tool
Summary
The article analyzes missed alarm bugs in Alive2, a translation-validation tool for LLVM IR, and describes two strategies (randomized YARPGen mutations and Minotaur-driven synthesis) to uncover missed alarms. It reports that few missed alarms have been found so far, highlighting the challenges of rigorously testing formal verification tools and suggesting future areas to explore such as function attributes.