Preface

This volume contains the proceedings of the 13th International Workshop on Verification of Infinite-State Systems (INFINITY 2011). The workshop was held in Taipei, Taiwan on October 10, 2011, as a satellite event to the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA). The INFINITY workshop aims at providing a forum for researchers who are interested in the development of formal methods and algorithmic techniques for the analysis of systems with infinitely many states, and their application in automated verification of complex software and hardware systems.

The program committee of INFINITY 2011 consisted of

• Parosh Abdulla, Uppsala University, Sweden 

• Rajeev Alur, University of Pennsylvania, USA

• Mohamed Faouzi Atig, Uppsala University, Sweden

• Yu-Fang Chen, Academia Sinica, Taiwan

• Javier Esparza, TU Munich, Germany 

• Peter Habermehl, LIAFA, Universite Denis Diderot - Paris 7, CNRS, France

• Shuvendu Lahiri, Microsoft Research, USA

• Akash Lal, Microsoft Research, India

• Jerome Leroux, LaBRI, Domaine Universitaire, CNRS, France

• Rupak Majumdar, Max Plank Institute, Germany

• Robby, Kansas State University, USA

• Neha Rungta, NASA Ames Research Center, USA

• Tomas Vojnar, Brno University of Technology, Czech Republic 

Each workshop paper submission was reviewed by 3-4 committee members or external reviewers. We thank the external referees Torben Amtoft, Lukas Holik, Chih-Duo Hong, Ondrej Lengal, and Arnaud Sangnier for their help. 

We thank Lukas Holik and Anton Wijs for their presentations. We also want to thank the ATVA 2011 Organizing Committee for taking care of the local organization and accommodating our special requests.

The keynote speakers at the workshop were 

• Tevfik Bultan (University of California, Santa Barbara, USA) 

• Doron A. Peled (Bar Ilan University, Israel) 

The final proceedings will appear in the Electronic Proceedings in Theoretical Computer Science (EPTCS) series. We thank Rob Van Glabbeek and Rajeev Alur for their support.

October 2011, Fang Yu and Chao Wang

String Analysis

Most important Web application vulnerabilities, such as SQL Injection, Cross Site Scripting and Malicious File Execution, are due to inadequate manipulation of string variables. String analysis is a static analysis technique that determines the values that a string expression can take during program execution at a given program point. This information can be used to detect security vulnerabilities and program errors, and to verify that program inputs are sanitized properly. In this talk I will discuss my research group's work on automata-based symbolic string analysis techniques for automatic verification of string manipulating programs. Our approach consists of three phases: Given an attack pattern, we first conduct a vulnerability analysis to identify if strings that match the attack pattern can reach security-sensitive functions. Next, we compute the vulnerability signature which characterizes all input strings that can exploit the discovered vulnerability. Given the vulnerability signature, we then construct sanitization statements that 1) check if a given input matches the vulnerability signature and 2) modify the input in a minimal way so that the modified input does not match the vulnerability signature. We have developed a tool called Stranger that implements our automata-based symbolic string analysis approach. Stranger can be used to find and eliminate string-related security vulnerabilities in PHP applications.

Shape Analysis Based on Forest Automata

We consider verification of programs manipulating dynamic linked data structures such as various forms of singly and doubly-linked lists or trees. We come with a novel representation of sets of shape graphs based on tree automata which combines advantages of automata-based approaches (higher generality and flexibility of abstraction) with some advantages of separation-logic-based approaches (efficient local reasoning). In our approach, a heap is split into several separated parts such that each of them can be represented by a tree automaton. The automata can refer to each other allowing the different parts of the heaps to mutually refer to their boundaries. Moreover, we come with a hierarchical representation of heaps by allowing alphabets of the tree automata to contain other, nested tree automata. Program instructions can be easily encoded as operations on our representation. This makes it possible to use a method based on a symbolic state-space exploration together with refinable abstraction within the so-called abstract regular tree model checking, and verify efficiently properties like null-pointer dereferences, absence of garbage, shape properties, etc.

Informed Swarm Verification of Infinite-State Systems

Swarm verification and parallel randomised depth-first search are very effective parallel techniques to hunt bugs in large explicit state spaces. In case bugs are absent, however, scalability of the parallelisation is completely lost. Informed swarm verification is an extension, in which workers periodically communicate with a manager to perform bounded searches. The workers do not synchronise with each other, though. This scheme helps each worker to perform a finite search, even if the state space is infinitely large, while still benefitting from randomisation to find bugs quickly. Because the workers operate independently, this technique is very suitable for large-scale parallel explicit state space exploration on a computer cluster. A prototype of this technique has been implemented in the LTSmin toolset, developed at the University of Twente.