TY - CONF AB - We propose a logic-based framework for automated reasoning about sequential programs manipulating singly-linked lists and arrays with unbounded data. We introduce the logic SLAD, which allows combining shape constraints, written in a fragment of Separation Logic, with data and size constraints. We address the problem of checking the entailment between SLAD formulas, which is crucial in performing pre-post condition reasoning. Although this problem is undecidable in general for SLAD, we propose a sound and powerful procedure that is able to solve this problem for a large class of formulas, beyond the capabilities of existing techniques and tools. We prove that this procedure is complete, i.e., it is actually a decision procedure for this problem, for an important fragment of SLAD including known decidable logics. We implemented this procedure and shown its preciseness and its efficiency on a significant benchmark of formulas. AU - Bouajjani, Ahmed AU - Dragoi, Cezara AU - Enea, Constantin AU - Sighireanu, Mihaela ID - 10903 SN - 0302-9743 T2 - Automated Technology for Verification and Analysis TI - Accurate invariant checking for programs manipulating lists and arrays with infinite data VL - 7561 ER - TY - CONF AB - Energy games belong to a class of turn-based two-player infinite-duration games played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in NP ∩ co−NP, but are not known to be in P. While the existence of polynomial-time algorithms has been a major open problem for decades, there is no algorithm that solves any non-trivial subclass in polynomial time. In this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several counter examples that show that many previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is developing the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting graph structures need not help. AU - Chatterjee, Krishnendu AU - Henzinger, Monika H AU - Krinninger, Sebastian AU - Nanongkai, Danupon ID - 10905 SN - 0302-9743 T2 - Algorithms – ESA 2012 TI - Polynomial-time algorithms for energy games with special weight structures VL - 7501 ER - TY - CONF AB - HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use the tool. AU - Grebenshchikov, Sergey AU - Gupta, Ashutosh AU - Lopes, Nuno P. AU - Popeea, Corneliu AU - Rybalchenko, Andrey ED - Flanagan, Cormac ED - König, Barbara ID - 10906 SN - 0302-9743 T2 - Tools and Algorithms for the Construction and Analysis of Systems TI - HSF(C): A software verifier based on Horn clauses VL - 7214 ER - TY - CHAP AU - Gupta, Ashutosh ID - 5745 SN - 0302-9743 T2 - Automated Technology for Verification and Analysis TI - Improved Single Pass Algorithms for Resolution Proof Reduction VL - 7561 ER - TY - CONF AB - Many infinite state systems can be seen as well-structured transition systems (WSTS), i.e., systems equipped with a well-quasi-ordering on states that is also a simulation relation. WSTS are an attractive target for formal analysis because there exist generic algorithms that decide interesting verification problems for this class. Among the most popular algorithms are acceleration-based forward analyses for computing the covering set. Termination of these algorithms can only be guaranteed for flattable WSTS. Yet, many WSTS of practical interest are not flattable and the question whether any given WSTS is flattable is itself undecidable. We therefore propose an analysis that computes the covering set and captures the essence of acceleration-based algorithms, but sacrifices precision for guaranteed termination. Our analysis is an abstract interpretation whose abstract domain builds on the ideal completion of the well-quasi-ordered state space, and a widening operator that mimics acceleration and controls the loss of precision of the analysis. We present instances of our framework for various classes of WSTS. Our experience with a prototype implementation indicates that, despite the inherent precision loss, our analysis often computes the precise covering set of the analyzed system. AU - Zufferey, Damien AU - Wies, Thomas AU - Henzinger, Thomas A ID - 3251 TI - Ideal abstractions for well structured transition systems VL - 7148 ER -