Scalable Software Model Checking for Finding Bugs in the Large
Event details
| Date | 21.06.2011 |
| Hour | 14:15 |
| Speaker | Dr Aarti Gupta, NEC Laboratories America |
| Location | |
| Category | Conferences - Seminars |
Software model checking has become popular due to the success of predicate abstraction and refinement techniques in finding API usage bugs in programs. In this talk, I will describe an alternate approach we have taken for finding memory safety bugs (such as null pointer dereferences, array buffer overflows, string errors, memory leaks), and
violations of API usage and user-specified assertions in C programs.
The highlights of our approach are:
- accurate memory modeling, including an analysis-friendly
representation
- powerful static analyses based on abstract
interpretation, to simplify models and find relatively
easy proofs of correctness
- efficient symbolic model checking, to verify the
unresolved properties and generate concrete error
traces.
To improve scalability on large software projects, we utilize a DC2 (Depth Cutoff with Design Constraints) framework. DC2 creates manageable partitions based on scope bounding, and uses automated specification inference techniques to derive environment constraints for partitions and stubs for missing code. Furthermore, it can automatically suggest refinements of the environment contraints based on counterexamples generated by a model checker, if a user deems a reported witness to be a false positive. We have implemented these
ideas in the F-Soft verification platform, which has been used successfully to find bugs in many large open source as well as industry software projects. Dr Gupta's homepage
Practical information
- General public
- Free