Published: 11th November 2011
DOI: 10.4204/EPTCS.73
ISSN: 2075-2180

EPTCS 73

Proceedings 13th International Workshop on
Verification of Infinite-State Systems
Taipei, Taiwan, 10th October 2011

Edited by: Fang Yu and Chao Wang

Preface
Fang Yu and Chao Wang
Keynote: String Analysis
Tevfik Bultan
1
Invited Paper: Practical Distributed Control Synthesis
Doron Peled and Sven Schewe
2
Invited Presentation: Shape Analysis Based on Forest Automata
Lukas Holik
18
Invited Presentation: Informed Swarm Verification of Infinite-State Systems
Anton Wijs
19
Trees over Infinite Structures and Path Logics with Synchronization
Alex Spelten, Wolfgang Thomas and Sarah Winter
20
Synthesis of Switching Rules for Ensuring Reachability Properties of Sampled Linear Systems
Laurent Fribourg, Bertrand Revol and Romain Soulat
35
A coinductive semantics of the Unlimited Register Machine
Alberto Ciaffaglione
49
Model Checking Probabilistic Real-Time Properties for Service-Oriented Systems with Service Level Agreements
Christian Krause and Holger Giese
64
A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking
Takashi Tomita, Shigeki Hagihara and Naoki Yonezaki
79

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

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 

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

Tevfik Bultan (University of California, Santa Barbara)

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

Lukas Holik (Uppsala University, Sweden)

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

Anton Wijs (Eindhoven University of Technology, Netherlands)

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.