TY - CONF AB - Separation logic (SL) has gained widespread popularity because of its ability to succinctly express complex invariants of a program’s heap configurations. Several specialized provers have been developed for decidable SL fragments. However, these provers cannot be easily extended or combined with solvers for other theories that are important in program verification, e.g., linear arithmetic. In this paper, we present a reduction of decidable SL fragments to a decidable first-order theory that fits well into the satisfiability modulo theories (SMT) framework. We show how to use this reduction to automate satisfiability, entailment, frame inference, and abduction problems for separation logic using SMT solvers. Our approach provides a simple method of integrating separation logic into existing verification tools that provide SMT backends, and an elegant way of combining SL fragments with other decidable first-order theories. We implemented this approach in a verification tool and applied it to heap-manipulating programs whose verification involves reasoning in theory combinations. AU - Piskac, Ruzica AU - Wies, Thomas AU - Zufferey, Damien ID - 2447 TI - Automating separation logic using SMT VL - 8044 ER - TY - CONF AB - Depth-Bounded Systems form an expressive class of well-structured transition systems. They can model a wide range of concurrent infinite-state systems including those with dynamic thread creation, dynamically changing communication topology, and complex shared heap structures. We present the first method to automatically prove fair termination of depth-bounded systems. Our method uses a numerical abstraction of the system, which we obtain by systematically augmenting an over-approximation of the system’s reachable states with a finite set of counters. This numerical abstraction can be analyzed with existing termination provers. What makes our approach unique is the way in which it exploits the well-structuredness of the analyzed system. We have implemented our work in a prototype tool and used it to automatically prove liveness properties of complex concurrent systems, including nonblocking algorithms such as Treiber’s stack and several distributed processes. Many of these examples are beyond the scope of termination analyses that are based on traditional counter abstractions. AU - Bansal, Kshitij AU - Koskinen, Eric AU - Wies, Thomas AU - Zufferey, Damien ED - Piterman, Nir ED - Smolka, Scott ID - 2847 TI - Structural Counter Abstraction VL - 7795 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 - TY - CONF AB - Cloud computing aims to give users virtually unlimited pay-per-use computing resources without the burden of managing the underlying infrastructure. We present a new job execution environment Flextic that exploits scal- able static scheduling techniques to provide the user with a flexible pricing model, such as a tradeoff between dif- ferent degrees of execution speed and execution price, and at the same time, reduce scheduling overhead for the cloud provider. We have evaluated a prototype of Flextic on Amazon EC2 and compared it against Hadoop. For various data parallel jobs from machine learning, im- age processing, and gene sequencing that we considered, Flextic has low scheduling overhead and reduces job du- ration by up to 15% compared to Hadoop, a dynamic cloud scheduler. AU - Henzinger, Thomas A AU - Singh, Anmol AU - Singh, Vasu AU - Wies, Thomas AU - Zufferey, Damien ID - 3302 TI - Static scheduling in clouds ER - TY - CONF AB - Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs. AU - Piskac, Ruzica AU - Wies, Thomas ED - Jhala, Ranjit ED - Schmidt, David ID - 3324 TI - Decision procedures for automating termination proofs VL - 6538 ER - TY - CONF AB - The static scheduling problem often arises as a fundamental problem in real-time systems and grid computing. We consider the problem of statically scheduling a large job expressed as a task graph on a large number of computing nodes, such as a data center. This paper solves the large-scale static scheduling problem using abstraction refinement, a technique commonly used in formal verification to efficiently solve computationally hard problems. A scheduler based on abstraction refinement first attempts to solve the scheduling problem with abstract representations of the job and the computing resources. As abstract representations are generally small, the scheduling can be done reasonably fast. If the obtained schedule does not meet specified quality conditions (like data center utilization or schedule makespan) then the scheduler refines the job and data center abstractions and, again solves the scheduling problem. We develop different schedulers based on abstraction refinement. We implemented these schedulers and used them to schedule task graphs from various computing domains on simulated data centers with realistic topologies. We compared the speed of scheduling and the quality of the produced schedules with our abstraction refinement schedulers against a baseline scheduler that does not use any abstraction. We conclude that abstraction refinement techniques give a significant speed-up compared to traditional static scheduling heuristics, at a reasonable cost in the quality of the produced schedules. We further used our static schedulers in an actual system that we deployed on Amazon EC2 and compared it against the Hadoop dynamic scheduler for large MapReduce jobs. Our experiments indicate that there is great potential for static scheduling techniques. AU - Henzinger, Thomas A AU - Singh, Vasu AU - Wies, Thomas AU - Zufferey, Damien ID - 3358 TI - Scheduling large jobs by abstraction refinement ER - TY - GEN AB - We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verification. We further show that satisfiability of formulas in TREX is decidable in NP. The low complexity makes it an attractive alternative to more expensive logics such as monadic second-order logic (MSOL) over trees, which have been traditionally used for reasoning about tree data structures. AU - Wies, Thomas AU - Muñiz, Marco AU - Kuncak, Viktor ID - 5383 SN - 2664-1690 TI - On an efficient decision procedure for imperative tree data structures ER - TY - CONF AB - We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verification. We further show that satisfiability of formulas in TREX is decidable in NP. The low complexity makes it an attractive alternative to more expensive logics such as monadic second-order logic (MSOL) over trees, which have been traditionally used for reasoning about tree data structures. AU - Wies, Thomas AU - Muñiz, Marco AU - Kuncak, Viktor ID - 3323 TI - An efficient decision procedure for imperative tree data structures VL - 6803 ER - TY - CONF AU - Podelski,Andreas AU - Thomas Wies ID - 4364 TI - Counterexample-guided focus ER - TY - CONF AB - Techniques such as verification condition generation, predicate abstraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Programs and their specifications often make use of data structures such as sets, multisets, algebraic data types, or graphs. Consequently, formulas generated from verification also involve such data structures. To automate the proofs of such formulas we propose a logic (a “calculus”) of such data structures. We build the calculus by starting from decidable logics of individual data structures, and connecting them through functions and sets, in ways that go beyond the frameworks such as Nelson-Oppen. The result are new decidable logics that can simultaneously specify properties of different kinds of data structures and overcome the limitations of the individual logics. Several of our decidable logics include abstraction functions that map a data structure into its more abstract view (a tree into a multiset, a multiset into a set), into a numerical quantity (the size or the height), or into the truth value of a candidate data structure invariant (sortedness, or the heap property). For algebraic data types, we identify an asymptotic many-to-one condition on the abstraction function that guarantees the existence of a decision procedure. In addition to the combination based on abstraction functions, we can combine multiple data structure theories if they all reduce to the same data structure logic. As an instance of this approach, we describe a decidable logic whose formulas are propositional combinations of formulas in: weak monadic second-order logic of two successors, two-variable logic with counting, multiset algebra with Presburger arithmetic, the Bernays-Schönfinkel-Ramsey class of first-order logic, and the logic of algebraic data types with the set content function. The subformulas in this combination can share common variables that refer to sets of objects along with the common set algebra operations. Such sound and complete combination is possible because the relations on sets definable in the component logics are all expressible in Boolean Algebra with Presburger Arithmetic. Presburger arithmetic and its new extensions play an important role in our decidability results. In several cases, when we combine logics that belong to NP, we can prove the satisfiability for the combined logic is still in NP. AU - Kuncak, Viktor AU - Piskac, Ruzica AU - Suter, Philippe AU - Wies, Thomas ED - Barthe, Gilles ED - Hermenegildo, Manuel ID - 4378 TI - Building a calculus of data structures VL - 5944 ER - TY - CONF AB - Cloud computing aims to give users virtually unlimited pay-per-use computing resources without the burden of managing the underlying infrastructure. We claim that, in order to realize the full potential of cloud computing, the user must be presented with a pricing model that offers flexibility at the requirements level, such as a choice between different degrees of execution speed and the cloud provider must be presented with a programming model that offers flexibility at the execution level, such as a choice between different scheduling policies. In such a flexible framework, with each job, the user purchases a virtual computer with the desired speed and cost characteristics, and the cloud provider can optimize the utilization of resources across a stream of jobs from different users. We designed a flexible framework to test our hypothesis, which is called FlexPRICE (Flexible Provisioning of Resources in a Cloud Environment) and works as follows. A user presents a job to the cloud. The cloud finds different schedules to execute the job and presents a set of quotes to the user in terms of price and duration for the execution. The user then chooses a particular quote and the cloud is obliged to execute the job according to the chosen quote. FlexPRICE thus hides the complexity of the actual scheduling decisions from the user, but still provides enough flexibility to meet the users actual demands. We implemented FlexPRICE in a simulator called PRICES that allows us to experiment with our framework. We observe that FlexPRICE provides a wide range of execution options-from fast and expensive to slow and cheap-- for the whole spectrum of data-intensive and computation-intensive jobs. We also observe that the set of quotes computed by FlexPRICE do not vary as the number of simultaneous jobs increases. AU - Henzinger, Thomas A AU - Tomar, Anmol AU - Singh, Vasu AU - Wies, Thomas AU - Zufferey, Damien ID - 4381 TI - FlexPRICE: Flexible provisioning of resources in a cloud environment ER - TY - CONF AB - Cloud computing is an emerging paradigm aimed to offer users pay-per-use computing resources, while leaving the burden of managing the computing infrastructure to the cloud provider. We present a new programming and pricing model that gives the cloud user the flexibility of trading execution speed and price on a per-job basis. We discuss the scheduling and resource management challenges for the cloud provider that arise in the implementation of this model. We argue that techniques from real-time and embedded software can be useful in this context. AU - Henzinger, Thomas A AU - Tomar, Anmol AU - Singh, Vasu AU - Wies, Thomas AU - Zufferey, Damien ID - 4380 TI - A marketplace for cloud resources ER - TY - JOUR AB - Any programming error that can be revealed before compiling a program saves precious time for the programmer. While integrated development environments already do a good job by detecting, e.g., data-flow abnormalities, current static analysis tools suffer from false positives ("noise") or require strong user interaction. We propose to avoid this deficiency by defining a new class of errors. A program fragment is doomed if its execution will inevitably fail, regardless of which state it is started in. We use a formal verification method to identify such errors fully automatically and, most significantly, without producing noise. We report on experiments with a prototype tool. AU - Hoenicke, Jochen AU - Leino, Kari AU - Podelski, Andreas AU - Schäf, Martin AU - Wies, Thomas ID - 533 IS - 2-3 JF - Formal Methods in System Design TI - Doomed program points VL - 37 ER - TY - CONF AB - Depth-bounded processes form the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. In this paper we develop an adequate domain of limits for the well-structured transition systems that are induced by depth-bounded processes. An immediate consequence of our result is that there exists a forward algorithm that decides the covering problem for this class. Unlike backward algorithms, the forward algorithm terminates even if the depth of the process is not known a priori. More importantly, our result suggests a whole spectrum of forward algorithms that enable the effective verification of a large class of mobile systems. AU - Wies, Thomas AU - Zufferey, Damien AU - Henzinger, Thomas A ED - Ong, Luke ID - 4361 TI - Forward analysis of depth-bounded processes VL - 6014 ER - TY - CONF AU - Seghir,Mohamed Nassim AU - Podelski,Andreas AU - Thomas Wies ID - 4365 TI - Abstraction Refinement for Quantified Array Assertions ER - TY - CONF AU - Thomas Wies AU - Piskac, Ruzica AU - Kuncak, Viktor ID - 4360 TI - Combining Theories with Shared Set Operations ER - TY - CONF AU - Lahiri,Shuvendu K. AU - Qadeer,Shaz AU - Galeotti,Juan P. AU - Voung,Jan W. AU - Thomas Wies ID - 4375 TI - Intra-module Inference ER - TY - CONF AU - Hoenicke,Jochen AU - Leino, K Rustan AU - Podelski,Andreas AU - Schäf,Martin AU - Thomas Wies ID - 4377 TI - It's Doomed; We Can Prove It ER - TY - CONF AB - Termination of a heap-manipulating program generally depends on preconditions that express heap assumptions (i.e., assertions describing reachability, aliasing, separation and sharing in the heap). We present an algorithm for the inference of such preconditions. The algorithm exploits a unique interplay between counterexample-producing abstract termination checker and shape analysis. The shape analysis produces heap assumptions on demand to eliminate counterexamples, i.e., non-terminating abstract computations. The experiments with our prototype implementation indicate its practical potential. AU - Podelski,Andreas AU - Rybalchenko, Andrey AU - Thomas Wies ID - 4366 TI - Heap Assumptions on Demand VL - 5123 ER - TY - CONF AU - Bouillaguet,Charles AU - Kuncak, Viktor AU - Thomas Wies AU - Zee,Karen AU - Rinard,Martin C. ID - 4394 TI - Using First-Order Theorem Provers in the Jahob Data Structure Verification System ER - TY - CONF AU - Berdine,Josh AU - Calcagno,Cristiano AU - Cook,Byron AU - Distefano,Dino AU - O'Hearn,Peter W. AU - Thomas Wies AU - Yang,Hongseok ID - 4398 TI - Shape Analysis for Composite Data Structures ER - TY - CONF AU - Thomas Wies AU - Kuncak, Viktor AU - Lam,Patrick AU - Podelski,Andreas AU - Rinard,Martin ID - 4359 TI - Field Constraint Analysis ER - TY - CONF AU - Podelski,Andreas AU - Thomas Wies ID - 4367 TI - Boolean Heaps ER -