Static Analysis of Memory Models for SMT Encodings

Explore a conference talk presenting innovative research on improving the efficiency of bounded model checkers through static analysis of memory models. Learn about a novel approach that reduces encoding size by computing bounds on relations used to determine execution consistency. Discover how the analysis derives both upper and lower bounds relativized to event execution, and incorporates external information to enhance precision. Examine new optimizations for SMT encoding, including simplified acyclicity constraint encoding. Understand the implementation and evaluation of these techniques within a bounded model checker, demonstrating significant reductions in verification time. Gain insights into the application of these optimizations for efficiently checking safety, liveness, and data race freedom in Linux kernel code.

[OOPSLA23] Static Analysis of Memory Models for SMT Encodings