The 4 Horsemen of Unsoundness in Object-Oriented Languages

Explore the unique challenges of object-oriented (OO) verification in this 49-minute conference talk presented at ACM SIGPLAN. Delve into four subtle yet significant issues that complicate OO verification: termination problems, leaky partial verification, ill-founded contracts, and the inevitable reduction to primitive operations. Examine concrete code examples that can be adapted for various OO verifiers, serving as benchmarks to identify well-known forms of unsoundness. Gain insights into the "4 horsemen of unsoundness" in OO languages and their implications for software development and verification processes.