Advertisement
Published in:
2008 | OriginalPaper | Chapter
Software Verification: Roles and Challenges for Automatic Decision Procedures
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Software model checking has become popular with the successful use of predicate abstraction and refinement techniques to find real bugs in low-level C programs. At the same time, verification approaches based on abstract interpretation and symbolic execution are also making headway in real practice. Much of the recent progress is fueled by advancements in automatic decision procedures and constraint solvers, which lie at the computational heart of these approaches. In this talk, I will describe our experience with several of these verification approaches, highlighting the roles played by automatic decision procedures and their interplay with the applications. Specifically, I will focus on SAT- and SMT-based model checking, combined with abstract domain analysis based on polyhedra representations. I will also describe some challenges from software verification that can motivate interesting research problems in this area.