Session 1: Verification, Session chair: Uday Khedker
3:30pm – 4:00pm Verification of Math Libraries, Rahul Sharma, Microsoft Research India
Math libraries provide heavily optimized implementations of transcendental functions like exp, log, sin, etc. Since the typical implementations found in math.h/libm operate over a finite number of bits, they are necessarily approximate. Moreover, humans and superoptimizers generate even faster math library functions that tradeoff precision for performance. We describe an automated technique that bounds the deviation between a given math library implementation from the ideal result.
4:00pm – 4:30pm Verifying Band Convergence for Sampled Control Systems, Ezudheen P, IISc Bangalore
We present a method to verify transient and settling time properties, called band convergence properties, of digitally controlled continuous systems, wherein we consider a linear dynamical system model for a plant and a PID controller. We consider the discrete-time sampled behaviour of the closed loop system, and verify band convergence for the discrete-time behavior. The basic idea is to look for a box-shaped invariant for the system which is adequate to ensure that the system stays within the given band. We first give a technique to handle a general discrete-time system, but with determinate matrix entries. We then give a technique to handle discrete-time systems with matrices that lie in a range which over-approximate the matrix exponential (which arise when we consider the discrete-time version of a continuous system), using the notion of an abstract discrete-time system. We have implemented the verification approach, and evaluate its efficacy on some popular Simulink models.
4:30pm – 5:00pm A Simulator for State Chart Based Language, Advait Lonkar, IIIT Bangalore
Specification models provide the benefit of automatic verification, where the defects in the software can be detected early in the development cycle. Statechart is a visual formalism for such specification models with complex life-cycles. Statechart formalism ensures expressivity while maintaining simplicity, making it widely accepted in the industry. Statechart Based Language (StaBL) is a specification language which allows modeling of statecharts. The statecharts modeled by StaBL are an extension of Harel Statecharts, with local variables and action language. Similar to other state-based formalisms, StaBL based statecharts are also susceptible to various specification issues. Early identification of such specification issues would not only be desirable but would also aid effective debugging. As statecharts can often evolve to be large (contain hundreds of states, variables, with multiple levels of hierarchy, etc), the task of manual identification of specification issues would be tedious and error-prone. We have built a simulator that captures the configuration of a statechart (modeled in StaBL) for each step, with the ability to maintain the value environments for the three types of variables provided by StaBL(local, parameter, and static). The implementation follows the work by Chakrabarti et. al. The simulation can proceed in three different modes: pre-event in steps, pre-event one-shot, and user-event in steps. The tool can run automated-tests that will identify points of various specification issues. This is especially useful in cases where a smaller sub-set of input (from an otherwise very large set) is responsible for inducing the issue. In this talk, we discuss the main design and architectural details of our tool, and our results on test specifications involving the different modes of execution. We also illustrate how the simulator can be used in the identification of the particular specification issue of non-determinism in a multi-level hierarchical configuration.
Session 2: Static Analysis, Session chair: K.V. Raghavan
5:15pm – 5:45pm New Results in May Happen in Parallel (MHP) Analysis, V. Krishna Nandivada, IIT Madras
May-Happen-in-Parallel (MHP) analysis is becoming the backbone of many of the parallel analyses and optimizations. In this talk, we present new approaches to do MHP analysis for X10-like languages that support async-finish-atomic parallelism. We present a fast incremental MHP algorithm to derive all the statements that may run in parallel with a given statement. We extend the MHP algorithm of Agarwal et al. (answers if two given X10 statements may run in parallel, and under what condition) to improve the computational complexity, without compromising on the precision. We also present algorithms to efficiently compute MHP analysis on the fly, when the program is changing, say in the context of IDEs.
5:45pm – 6:15pm Generalized Points-to Graphs: A Precise and Scalable Abstraction for Points-to Analysis, Pritam Gharat, Imperial College UK
Computing precise (fully flow- and context-sensitive) and exhaustive (as against demand-driven) points- to information is known to be expensive. Top-down approaches require repeated analysis of a procedure for separate contexts. Bottom-up approaches need to model unknown pointees accessed indirectly through pointers that may be defined in the callers and hence do not scale while preserving precision. Therefore, most approaches to precise points-to analysis begin with a scalable but imprecise method and then seek to increase its precision. In contrast, we begin with a precise method and increase its scalability. We create naive but possibly non-scalable procedure summaries and then use novel optimizations to compact them while retaining their soundness and precision. We propose a novel abstraction called the generalized points-to graph (GPG), which views points-to relations as memory updates and generalizes them using the counts of indirection levels leaving the unknown pointees implicit. This allows us to construct GPGs as compact representations of bottom- up procedure summaries in terms of memory updates and control flow between them. Their compactness is ensured by strength reduction (reducing the indirection levels), control flow minimization (eliminating control flow edges while preserving soundness and precision), and call inlining (enhancing the opportunities of these optimizations). The effectiveness of GPGs lies in the fact that they discard as much control flow as possible without losing precision. As a result GPGs are very small even for main procedures that contain the effect of the entire program. This allows our implementation to scale to 158 kLoC for C programs. At a more general level, GPGs provide a convenient abstraction to represent and transform memory in the presence of pointers.
6:15pm – 6:45pm Bidirectionality in flow-sensitive demand-driven analysis, Swati Jaiswal, VNIT Nagpur
Demand-driven methods for program analysis have primarily been viewed as efficient algorithms for computing the same information as the corresponding exhaustive methods, but for a given set of demands. We found this counter intuitive. Hence we tried to connect a known fact (“demand-driven methods compute less information”) with a self-evident intuition (“imprecision caused by abstraction should increase with the amount of data abstracted”). This investigation led to our contribution of designing demand-driven flow-sensitive alias analysis (which we call PDFSA). PDFSA is not only efficient but also more precise as compared to exhaustive flow-sensitive alias analysis (EFSA). We formalize PDFSA using an inherent property of a demand-driven flow-sensitive alias analysis: demands are propagated against the control flow and aliases are propagated along the control flow. Traditionally, this has been seen as a collection of two separate analyses whose interaction is controlled by an algorithm that drives the two analyses. We formalize this algorithmic view as a bidirectional data flow analysis to define PDFSA declaratively. Further, we define Meet Over Paths (MoP) solution for bidirectional flows for reasoning about the soundness of PDFSA. Our definition generalizes the classical definition of MoP which is restricted to unidirectional flows. We have implemented PDFSA, existing demand-driven alias analysis (which we call ADFSA), and EFSA for static resolution of virtual function calls in C++ for constructing more precise call graphs. Our measurements show that the call graphs computed using PDFSA are indeed more precise than those that are computed using ADFSA or EFSA.
6:45pm – 7:15pm Efficient Fixpoint Computation for Abstract Interpretation, Aditya Thakur, UC Davis, USA
Abstract interpretation is a general framework for expressing static program analyses. It reduces the problem of extracting properties of a program to computing an approximation of the least fixpoint of a system of equations. The de facto approach for computing this approximation uses a Bourdoncle’s algorithm based on weak topological order (WTO). This talk describes recent work on improving the time and memory performance of abstract interpretation without sacrificing precision. First, we present a deterministic parallel algorithm for fixpoint computation by introducing the notion of weak partial order (WPO), which generalizes the notion of WTO. We present an almost-linear time algorithm for computing a WPO. Second, we present a technique for memory-efficient fixpoint computation. Both techniques are proved to be optimal while computing the same result as Bourdoncle’s approach. The talk will also describe the implementation and evaluation of these techniques in the NASA IKOS and Facebook SPARTA abstract interpreters.