Correctness Witness Validation by Abstract Interpretation

Explore a conference talk on validating correctness witnesses through abstract interpretation. Learn about the novel 'unassume' abstract operation for incorporating witness invariants into abstract program states. Discover how this approach can accelerate fixpoint convergence and improve precision in program analysis. Examine the implementation of unassume operators in an abstract interpreter and evaluate their impact on performance and precision. Understand how manually crafted witnesses can confirm verification results for multi-threaded programs, reducing CPU time by 7% to 47%. Investigate the potential of using witnesses from model checkers to guide analyzers in verifying previously unverifiable program properties.