ATVA China 2006

October 23-26, 2006       Beijing, China organised and funded by ARTIST 

Programme & Slides


- National Natural Science Foundation of China
- Institute of Software of the Chinese Academy of Sciences
- Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Keynote speakers

Mihalis Yannakakis
Columbia University
New York, NY 10027

Jin Yang
Strategic CAD Labs
Intel Corporation

Thomas Ball
Microsoft Research
Redmond, WA 98052

Day 1 (23 OCT 2006)

Tutorial 1: Mihalis Yannakakis Columbia University
Testing, Optimization, and Games
We will discuss algorithmic problems arising in the testing of reactive systems (i.e. systems that interact with their environment), modeled by various types of state machines. The goal is to design test sequences so that we can deduce desired information about the given system under test, such as whether it conforms to a given specification model, or whether it satisfies given requirement properties. Test generation can be approached from different points of view - as an optimization problem of minimizing cost and maximizing the effectiveness of the tests; as a game between tester and system under test; or as a learning problem. We touch on some of these aspects and related algorithmic questions.

Tutorial 2: Jin Yang, Intel Corporation
Introduction to Generalized Symbolic Trajectory Evaluation
Generalized Symbolic Trajectory Evaluation (GSTE) is a symbolic model checking approach that combines the high capacity of STE with the expressive power of traditional symbolic model checking. It has been successfully applied to the formal verification of complex Intel micro-processor designs with tens of thousands of state elements. GSTE uses an operational style specification for describing a functional property of a hardware circuit. Model checking in GSTE is based on a form of symbolic simulation with a tightly integrated dynamic quaternary abstraction mechanism that explores the shape of the specification to achieve high verification capacity. As such, the complexity of model checking in GSTE mostly depends on the complexity of the specification rather than the complexity of the circuit under verification. A brief introduction to some of the key aspects of GSTE is to be given.

Tutorial 3: Thomas Ball, Microsoft Research
Secrets of SLAM
Model checking is a technique to find bugs in systems by systematically exploring their state spaces. Due to state space explosion, model checkers typically operate on a manually constructed finite-state abstraction of the system. The goal of the SLAM project is to model check software written in common programming languages directly. SLAM has been successfully used to find and fix errors in Windows device drivers written in the C language. SLAM operates by automatically constructing and refining model-checkable abstractions (called Boolean Programs) of a C program. The first part of this tutorial will describe how the SLAM project has combined and extended results from the areas of program analysis, model checking and theorem proving to analyze critical properties of systems software written in the C language. The second half of the tutorial will present some of the engineering "secrets" we applied to the basic SLAM process to improve its performance on Windows device drivers.

Day 2 (24 OCT 2006)

Opening (Huimin Lin, Susanne Graf, Farn Wang)
Keynote Speech Mihalis Yannakakis (Session Chair: Susanne Graf)
Analysis of Recursive Probabilistic Models
  • Session 1: Probablilitic Analysis(Session Chair: Susanne Graf)
    - Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives. ( Alastair F. Donaldson, Alice Miller , UK)
    - Eager Markov Chains. (Parosh Aziz Abdulla, Noomene Ben Henda, Richard Mayr, Sven Sandberg , SE)
    - A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement. (Fei He, Xiaoyu Song, Ming Gu, Jiaguang Sun , CN)
  • Session 2: Model Checking (Session Chair: Jin Yang)
    - A Fine-Grained Fullness-Guided Chaining Heuristic for Symbolic Reachability Analysis. ( Ming-Ying Chung, Gianfranco Ciardo, Andy Jinqing Yu , US)
    - Model Checking Timed Systems with Urgencies.(Pao-Ann Hsiung, Shang-Wei Lin, Yean-Ru Chen, Chun-Hsian Huang, Jia-Jen Yeh, Hong-Yu Sun, Chao-Sheng Lin, Hsiao-Win Liao , TW)
    - Whodunit? Causal Analysis for Counterexamples. (Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta , US)
  • Session 3: Computation and Complexity (Session Chair: Michael Yannakakis)
    - On the Membership Problem for Visibly Pushdown Languages. (Salvatore La Torre, Margherita Napoli, Mimmo Parente , IT)
    - On the Construction of Fine Automata for Safety Properties. (Orna Kupferman, Robby Lampert , IL)
    - On the Succinctness of Nondeterminizm. ( Benjamin Aminof, Orna Kupferman , IL)
    - Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains. (Dejvuth Suwimonteerabuth, Stefan Schwoon, Javier Esparza , DE)
  • Session 4: Satisfiability and Reasoning (Session Chair: Wenhui Zhang)
    - Compositional Reasoning for Hardware/Software Co-Verification. (Fei Xie, Guowu Yang, Xiaoyu Song, US)
    - Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition. (Wonhong Nam, Rajeev Alur, US)
    - On the Satisfiability of Modular Arithmetic Formulae. (Bow-Yaw Wang , TW)
    - Selective Approaches for Solving Weak Games. (Malte Helmert, Robert Mattmüller, Sven Schewe , DE)

Day 3 (25 OCT 2006)

- Keynote Speech by Jin Yang (Session Chair: Farn Wang)
- Verification Challenges and Opportunities in the New Era of Microprocessor Design
  • Session 5: Synthesis (Session Chair: Farn Wang)
    - Controller synthesis and Ordinal Automata. (Thierry Cachat , FR)
    - Effective Contraction of Timed STGs for Decomposition Based Timed Circuit Synthesis. (Tomohiro Yoneda, Chris J. Myers, JP)
    - Synthesis for Probabilistic Environments. (Sven Schewe , DE)
  • Session 6: Realtime and Hybrid Systems (Session Chair: Hsu-Chun Yen)
    - Branching-Time Property Preservation Real-time Systems. (Jinfeng Huang, Marc Geilen, Jeroen Voeten, Henk Corporaal , NL)
    - Automatic Verification of Hybrid Systems with Large Discrete State Space. (Werner Damm, Stefan Disch, Hardi Hungar, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz , DE)
    - Timed Unfoldings for Networks of Timed Automata. (Patricia Bouyer, Serge Haddad, Pierre-Alain Reynier , FR)
    - Symbolic Unfoldings For Networks of Timed Automata. (by Franck Cassez, Thomas Chatain, Claude Jard , FR)

Day 4 (26 OCT 2006)

- Keynote Speech by Thomas Ball (Session Chair: Susanne Graf)
- Automated Abstraction of Software
  • Session 7: Abstraction (Session Chair: Susanne Graf)
    - Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise. (Harald Fecher, Michael Huth , DE)
    - Timed Temporal Logics for Abstracting Transient States. (Houda Bel Mokadem, Béatrice Bérard, Patricia Bouyer, François Laroussinie , FR)
    - Predicate Abstraction of Programs Containing Non-linear Computation. (Songtao Xia, Ben Di Vito, Cesar Munoz , US)
  • Session 8: Communicating Systems and Testing (Session Chair: Thomas Ball)
    - A Fresh Look at Testing for Asynchronous Communication. (Puneet Bhateja, Paul Gastin, Madhavan Mukund , IN)
    - Proactive Leader Election in Asynchronous Shared Memory Systems. (M. C. Dharmadeep, K. Gopinath , IN)
    - A Semantic Framework for Test Coverage. (Laura Brandán Briones, Ed Brinksma, Mariëlle Stoelinga , NL)
  • Session 9: Protocols and Security (Session Chair: Bow-Yaw Wang)
    - Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols. (Giorgio Delzanno, Javier Esparza, Jiri Srba , DK)
    - Analyzing Security Protocols in Hierarchical Networks. (Ye Zhang, Hanne Riis Nielson , DK)
    - Functional Analysis of a Real-Time Protocol for Networked Control Systems. (Colin Fidge, Yu-Chu Tian , AU)
    - Symbolic Semantics for the Verification of Security Properties of Mobile Petri Nets. ( Fernando Rosa-Velardo, David de Frutos-Escrig , ES)
  • Session 10: Bisimulation and Model Checking (Session Chair: Huimin Lin)
    - Sigref - A Symbolic Bisimulation Tool Box. (Ralf Wimmer, Marc Herbstritt, Holger Hermanns, Kelley Strampp, Bernd Becker , DE)
    - Towards a Model-Checker for Counter Systems. (Stephane Demri, Alain Finkel, Valentin Goranko, Govert van Drimmelen , FR)
    - The Implementation of Mazurkievicz Traces in POEM. (Peter Niebert, Hongyang Qu , FR)
    - Model-Based Tool-Chain Infrastructure for Automated Analysis of Embedded Systems. (Hang Su, Graham Hemingway, Kai Chen, T. John Koo , US)

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009

Réalisation Axome - Création de sites Internet