Published on: 12-Dec-2016
The award was presented to Assistant Professor Liu Yang (3rd from left) at the Award Ceremony in FSE 2016.
SCSE cybersecurity research team won the ACM SIGSOFT Distinguished Paper Award at the 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2016) held in Seattle, Washington on November 13-18, 2016. The award winning paper, entitled 'Proteus: Computing Disjunctive Loop Summary via Path Dependency Analysis' is co-authored by Xie Xiaofei, Dr Chen Bihuan and Assistant Professor Liu Yang in SCSE, Assistant Professor Le Wei from Iowa State University, USA and Professor Li Xiaohong from Tianjin University, China. This paper proposes an approach to analysis and summarize loop. The loop summarization technique can be applied in many program analysis tasks, e.g., program verification, symbolic execution and testing.
FSE 2016 is an internationally renowned forum for researchers, practitioners, and educators to present and discuss the most recent innovations, trends, experiences, and challenges in the field of software engineering. FSE brings together experts from academia and industry to exchange the latest research results and trends, as well as their practical application in all areas of software engineering. Topics of interest include, but are not limited to: Architecture and design; Aspect-orientation; Autonomic computing and (self-)adaptive systems; Big data; Cloud computing; Components, services, and middleware; Computer supported cooperative work; Configuration management and deployment; Crowdsourcing; Debugging; Dependability, safety, and reliability; Development tools and environments; Distributed, parallel, and concurrent software; Education; Embedded and real-time software; Empirical software engineering; End-user software engineering; Formal methods; Green computing; Human and social factors in software engineering; Human-computer interaction; Knowledge based software engineering; Mobile, ubiquitous, and pervasive software; Model-driven software engineering; Patterns and frameworks; Policy and ethics; Processes and workflows; Program analysis; Program comprehension and visualization; Program synthesis; Programming languages; Refactoring; Requirements engineering; Reverse engineering; Safety-critical systems; Scientific computing; Search-based software engineering; Security and privacy; Software economics and metrics; Software evolution and maintenance; Software product lines; Software reuse; Software services; Specification and verification; Testing; Traceability; Web-based software.
Title: Proteus: Computing Disjunctive Loop Summary via Path Dependency Analysis
Authors: Xiaofei Xie, Bihuan Chen, Yang Liu, Wei Le, Xiaohong Li
Background: Analyzing loops is very important for successful program optimizations, bug findings, and test input generation. However, loop analysis is one of the most challenging tasks in program analysis. It is described as the “Achilles’ heel” of program verification and a key bottleneck for scaling symbolic execution. Generally, there are three kinds of techniques for analyzing loops, namely loop unwinding, loop invariant inference and loop summarization. The most intuitive method is loop unwinding, where we unroll the loop with a fixed number of iterations (a.k.a. the bound). This technique is unsound and cannot reason about the program behaviors beyond the loop bound. Loop invariant is a property that holds before and after each loop iteration. It is mostly used to verify the correctness of a loop. The limitation is that typically only strong invariants are useful to prove the property; while commonly-used fixpoint-based invariant inferencing is iterative and sometimes time-consuming. It may fail to generate strong invariants, especially for complex loops. In addition, loop invariants often cannot sufficiently describe the effect after the loop and hence are limited to check the property after the loop. Compared with loop invariants, loop summarization provides a more accurate and complete comprehension for loops. It summarizes the relationship between the inputs and outputs of a loop as a set of symbolic constraints. We therefore can replace the loop fragments with such “symbolic transformers” during program analysis.
This paper accomplishes two tasks to advance the state-of-the-art loop analysis. First, we proposed a classification for multi-path, single loops (un-nested loops) based on a deep analysis on challenging loops found in real-world software. The classification defines what types of multi-path loops we can handle precisely, what types of multi-path loops we can handle with approximation, and what types of multi-path loops we cannot handle. Second, we developed a loop analysis framework, named Proteus, to summarize the effect of the loops for each type. Proteus takes a loop code fragment and a set of variables of interest as inputs to compute the disjunctive loop summary (DLS). The DLS represents a disjunction of a set of path-sensitive loop effects on the variables of interest.
Back to listing