Analyzing Data Structure Properties of Large Object-Oriented Programs
Final Report Abstract
This project concerns with usability of static program analysis using logical constraint solvers. Such approaches are very promising because unlike dynamic approaches that only analyze particular executions of programs, static approaches analyze the whole state space of programs with no need to actually execute the code. However, static techniques have always been criticized because they are expensive and do not scale to larger programs. The cost comes from various aspects: (1) the underlying constraint solvers cannot solve large, complex formulas, (2) specification languages used in such analysis are unintuitive and error-prone for complex properties, and (3) several existing tools require a lot of annotations or manual interventions from users. In this project, we alleviated the problem by introducing three automated techniques that help users apply static program analysis approaches in a more cost-efficient way. In particular, we have developed: A fully automatic translation of code and specifications to SMT logic. The resulting constraints are easy-to-read and can be efficiently solved by state-of-the-art SMT solvers. This approach made our static bounded program verification tool scale much more than other existing tools. - A fully automatic transformation from Alloy to JML specification languages. This allows users to specify data-structure rich properties succinctly in the more expressive, abstract, and readable Alloy language without worrying about the underlying analyses which use the lower-level JML language. - A full evaluation of various approaches for using constraint solving in automatic generation of test cases. Such approaches will exploit the strengths of logical constraints in producing test cases that are structurally complex and possibly steer programs into corner cases and less-executed paths.
Publications
- “Bounded Program Verification using an SMT Solver: A Case Study”, Proc. of the 5th International Conference on Software Testing, Verification, and Validation (ICST), pages 101-110, IEEE, Montreal, April 2012
T. Liu, M. Nagel, and M. Taghdiri
- “A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution”, 10th Haifa Verification Conference (HVC), 2014
T. Liu, M. Araujo, M. D’Amorim, and M. Taghdiri
(See online at https://doi.org/10.1007/978-3-319-13338-6_21) - “Generating JML Specifications from Alloy Expressions”, 10th Haifa Verification Conference (HVC), 2014
D. Grunwald, C. Gladisch, T. Liu, M. Taghdiri, and S. Tyszberowicz
(See online at https://doi.org/10.1007/978-3-319-13338-6_9)
