Search

In this article, we present a new shape analysis algorithm. The key distinguishing aspect of our algorithm is that it is completely compositional, bottom-up and noniterative. We present our algorithm as an inference system for computing Hoare triples summarizing heap manipulating programs. Our inference rules are compositional: Hoare triples for a compound statement are computed from the Hoare triples of its component statements. These inference rules are used as the basis for bottom-up shape analysis of programs. Specifically, we present a Logic of Iterated Separation Formulae (LISF), which uses the iterated separating conjunct of Reynolds [2002] to represent program states. A key ingredient of our inference rules is a strong bi-abduction operation between two logical formulas. We describe sound strong bi-abduction and satisfiability procedures for LISF. We have built a tool called SpInE that implements these inference rules and have evaluated it on standard shape analysis benchmark programs. Our experiments show that SpInE can generate expressive summaries, which are complete functional specifications in many cases. [ABSTRACT FROM AUTHOR]

We present an algorithm DASH to check if a program P satisfies a safety property φ. The unique feature of this algorithm is that it uses only test generation operations, and it refines 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 refinement operator WPα that uses only the alias information obtained by symbolically executing a test to refine abstractions in a sound manner. We present a full exposition of the DASH algorithm and its theoretical properties. We have implemented DASH in a tool called YOGI that plugs into Microsoft's Static Driver Verifier framework. We have used this framework to run YOGI on 69 Windows Vista drivers with 85 properties and find that YOGI scales much better than SLAM, the current engine driving Microsoft's Static Driver Verifier. [ABSTRACT FROM AUTHOR]

In this paper, we present new ways of describing and constructing linear tail-biting trellises for block codes. We extend the well-known Bahl-Cocke-Jelinek--Raviv (BCJR) construction for conventional trellises to tail-biting trellises. The BCJR-like labeling scheme yields a simple specification for the tail-biting trellis for the dual code, with the dual trellis having the same state-complexity profile as that of the primal code. Finally, we show that the algebraic specification of Forney for state spaces of conventional trellises has a natural extension to tail-biting trellises. [ABSTRACT FROM AUTHOR]