Papers

Compositional May-Must Program Analysis

Program analysis tools typically compute two types of information: (1) may information that is true of all program executions and is used to prove the absence of bugs in the program, and (2) must information that is true of some program executions and is used to prove the existence of bugs in the program. In this paper, we propose a new algorithm, dubbed SMASH, which computes both may and must information compositionally. At each procedure boundary, may and must information is represented and stored as may and must summaries, respectively. Those summaries are computed in a demand-driven manner and possibly using summaries of the opposite type. We have implemented S MAS H using predicate abstraction (as in S L AM) for the may part and using dynamic test generation (as in DART) for the must part. Results of experiments with 69 Microsoft Windows Vista device drivers show that SMAS H can signiﬁcantly outperform may-only, must-only and non-compositional may-must algorithms. Indeed, our empirical results indicate that most complex code fragments in large programs are actually often either easy to prove irrelevant to the speciﬁc property of interest using may analysis or easy to traverse using directed testing. The ﬁne-grained coupling and alternation of may (universal) and must (existential) summaries allows SMAS H to easily navigate through these code fragments while traditional may-only, must-only or noncompositional may-must algorithms are stuck in their speciﬁc analyses.

DART: Directed Automated Random Testing

We present a new tool, named DART, for automatically testing soft- ware that combines three main techniques: (1) automated extraction of the interface of a program with its external environment using static source-code parsing; (2) automatic generation of a test driver for this interface that performs random testing to simulate the most general environment the program can operate in; and (3) dynamic analysis of how the program behaves under random testing and automatic generation of new test inputs to direct systematically the execution along alternative program paths. Together, these three techniques constitute Directed Automated Random Testing, or DART for short. The main strength of DART is thus that testing can be performed completely automatically on any program that com- piles – there is no need to write any test driver or harness code. During testing, DART detects standard errors such as program crashes, assertion violations, and non-termination. Preliminary experiments to unit test several examples of C programs are very encouraging.

From Tests to Proofs

We describe the design and implementation of an automatic invariant generator for imperative programs. While automatic invariant generation through constraint solving has been extensively studied from a theoretical viewpoint as a classical means of program veriﬁcation, in practice existing tools do not scale even to moderately sized programs. This is because the constraints that need to be solved even for small programs are already too difﬁcult for the underlying (non-linear) constraint solving engines. To overcome this obstacle, we propose to strengthen static constraint generation with information obtained from static abstract interpretation and dynamic execution of the program. The strengthening comes in the form of additional linear constraints that trigger a series of simpliﬁcations in the solver, and make solving more scalable. We demonstrate the practical applicability of the approach by an experimental evaluation on a collection of challenging benchmark programs and comparisons with related tools based on abstract interpretation and software model checking.

Liquid Types

We present Logically Qualiﬁed Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the beneﬁts of dependent types, namely static veriﬁcation of critical properties and the elimination of expensive run-time checks, without the heavy price of manual annotation. We have implemented liquid type inference in DS OLVE, which takes as input an OC AML program and a set of log- ical qualiﬁers and infers dependent types for the expressions in the OC AML program. To demonstrate the utility of our approach, we describe experiments using DS OLVE to statically verify the safety of array accesses on a set of OC AML benchmarks that were previously annotated with dependent types as part of the DML project. We show that when used in conjunction with a ﬁxed set of array bounds checking qualiﬁers, DS OLVE reduces the amount of manual annotation required for proving safety from 31% of program text to under 1%.

Proofs from Tests

We present an algorithm Dash to check if a program P satisﬁes a safety property ϕ. The unique feature of the algorithm is that it uses only test generation operations, and it reﬁnes and maintains a sound program abstraction as a consequence of failed test generation operations. Thus, each iteration of the algorithm is inexpensive, and can be implemented without any global may-alias information. In particular, we introduce a new reﬁnement operator WPα that uses only the alias information obtained by executing a test to reﬁne abstractions in a sound manner. We present a full exposition of the "Dash" algorithm, its theoretical properties, and its implementation.

SYNERGY: A New Algorithm for Property Checking

We consider the problem if a given program satisﬁes a speciﬁed safety property. Interesting programs have inﬁnite state spaces, with inputs ranging over inﬁnite domains, and for these programs the property checking problem is undecidable. Two broad approaches to property checking are testing and veriﬁcation. Testing tries to ﬁnd inputs and executions which demonstrate violations of the property. Veriﬁcation tries to construct a formal proof which shows that all executions of the program satisfy the property. Testing works best when errors are easy to ﬁnd, but it is often diﬃcult to achieve suﬃcient coverage for correct programs. On the other hand, veriﬁcation methods are most successful when proofs are easy to ﬁnd, but they are often ineﬃcient at discovering errors. We propose a new algorithm, Synergy, which combines testing and veriﬁcation. Synergy uniﬁes several ideas from the literature, including counterexample-guided model checking, directed testing, and partition reﬁnement. This paper presents a description of the Synergy algorithm, its theoretical properties, a comparison with related algorithms, and a prototype implementation called Yogi.

Type-based Data Structure Veriﬁcation

We present a reﬁnement type-based approach for the static veriﬁcation of complex data structure invariants. Our approach is based on the observation that complex data structures are typically fashioned from two elements: recursion (e.g., lists and trees), and maps (e.g., arrays and hash tables). We introduce two novel type-based mechanisms targeted towards these elements: recursive reﬁnements and polymorphic reﬁnements. These mechanisms automate the challenging work of generalizing and instantiating rich universal invariants by piggybacking simple reﬁnement predicates on top of types, and carefully dividing the labor of analysis between the type system and an SMT solver [6]. Further, the mechanisms permit the use of the abstract interpretation framework of liquid type inference [22] to automatically synthesize complex invariants from simple logical qualiﬁers, thereby almost completely automating the veriﬁcation. We have implemented our approach in DS OLVE, which uses liquid types to verify OC AML programs. We present experiments that show that our type-based approach reduces the manual annotation required to verify complex properties like sortedness, balancedness, binary-search-ordering, and acyclicity by more than an order of magnitude.

Yogi Project: Software Property Checking via Static Analysis and Testing

We present Yogi, a tool that checks properties of C programs by combining static analysis and testing. Yogi implements the Dash algorithm which performs veriﬁcation by combining directed testing and abstraction. We have engineered Yogi in such a way that it plugs into Microsoft’s Static Driver Veriﬁer framework. We have used this framework to run Yogi on 69 Windows Vista drivers with 85 properties. We ﬁnd that the new algorithm enables Yogi to scale much better than Slam, which is the current engine driving Microsoft’s Static Driver Veriﬁer.

Document Actions