Towards Scalable Modular Checking of User-Defined Properties

Abstract. Theorem-prover based modular checkers have the potential to perform scalable and precise checking of user-defined properties by combining pathsensitive intraprocedural reasoning with user-defined procedure abstractions. However, such tools have seldom been deployed on large software applications of industrial relevance due to the annotation burden required to provide the procedure ions. In this work, we present two case studies of applying a modular checker HAVOC to check properties on large modules in the Microsoft Windows operating system. The first detailed case study describes checking the synchronization protocol of a core Microsoft Windows component with more than 300 thousand lines of code and 1500 procedures. The effort found 45 serious bugs in the component with modest annotation effort and low false alarms; most of these bugs have since been fixed by the developers of the module. The second case study reports preliminary user experience in using the tool for checkin...

• Type: Journal
• Year: 2010
• Where: VSTTE
• Authors: Thomas Ball, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer, Julien Vanegue
• Keywords: Annotation Burden, Modest Annotation, Modular Checker, Software Engineering, VSTTE 2010