08:30-11:00 |
Registration |
11:00-13:00 |
Tutorial 1: Testing, Optimization, and Games (by
Mihalis Yannakakis) |
|
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. |
13:00-14:00 | Lunch Break |
14:00-16:00 |
Tutorial 2: Introduction to Generalized Symbolic Trajectory Evaluation (by Jin Yang) |
|
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. |
16:00-16:15 | Coffee Break |
16:15-18:15 |
Tutorial 3: Secrets of SLAM (by Thomas Ball) |
|
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. |
18:45-20:30 |
Reception |
08:30-08:50 |
Registration |
08:50-09:00 |
Opening by Huimin Lin, Susanne Graf, Farn Wang
|
09:00-10:00 |
Keynote Speech by Mihalis Yannakakis
(Session Chair: Susanne Graf)
|
|
Analysis of Recursive Probabilistic Models |
10:00-11:30 |
Session 1: Probablilitic Analysis
(Session Chair: Susanne Graf)
|
|
Symmetry Reduction for Probabilistic Model Checking Using Generic
Representatives.
(by Alastair F. Donaldson, Alice Miller , UK) |
|
Eager Markov Chains.
(by Parosh Aziz Abdulla, Noomene Ben Henda, Richard Mayr, Sven Sandberg
, SE) |
|
A Probabilistic Learning Approach for Counterexample Guided Abstraction
Refinement.
(by Fei He, Xiaoyu Song, Ming Gu, Jiaguang Sun
, CN) |
11:30-12:00 | Coffee Break |
12:00-13:30 |
Session 2: Model Checking
(Session Chair: Jin Yang)
|
|
A Fine-Grained Fullness-Guided Chaining Heuristic for Symbolic Reachability
Analysis.
(by Ming-Ying Chung, Gianfranco Ciardo, Andy Jinqing Yu
, US) |
|
Model Checking Timed Systems with Urgencies.
(by 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.
(by Chao Wang,
Zijiang Yang,
Franjo Ivancic,
Aarti Gupta
, US) |
13:30-14:30 | Lunch Break |
14:30-16:30 |
Session 3: Computation and Complexity
(Session Chair: Michael Yannakakis)
|
|
On the Membership Problem for Visibly Pushdown Languages.
(by Salvatore La Torre, Margherita Napoli, Mimmo Parente , IT) |
|
On the Construction of Fine Automata for Safety Properties.
(by Orna Kupferman, Robby Lampert , IL) |
|
On the Succinctness of Nondeterminizm.
(by Benjamin Aminof, Orna Kupferman , IL) |
|
Efficient Algorithms for Alternating Pushdown Systems with an
Application to the Computation of Certificate Chains.
(by Dejvuth Suwimonteerabuth, Stefan Schwoon, Javier Esparza
, DE) |
16:30-16:45 | Coffee Break |
16:45-18:45 |
Session 4: Satisfiability and Reasoning
(Session Chair: Wenhui Zhang)
|
|
Compositional Reasoning for Hardware/Software Co-Verification.
(by Fei Xie, Guowu Yang, Xiaoyu Song, US) |
|
Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition.
(by Wonhong Nam, Rajeev Alur, US) |
|
On the Satisfiability of Modular Arithmetic Formulae.
(by Bow-Yaw Wang , TW) |
|
Selective Approaches for Solving Weak Games.
(by Malte Helmert, Robert Mattmüller, Sven Schewe
, DE) |
19:00-21:00 |
Dinner (sponsored by
Laboratory of Computer Science, Institute of Software,
Chinese Academy of Sciences)
|
08:30-09:30 |
Keynote Speech by Jin Yang
(Session Chair: Farn Wang)
|
|
Verification Challenges and Opportunities
in the New Era of Microprocessor Design
|
09:30-11:00 |
Session 5: Synthesis
(Session Chair: Farn Wang)
|
|
Controller synthesis and Ordinal Automata.
(by Thierry Cachat , FR) |
|
Effective Contraction of Timed STGs for Decomposition Based Timed Circuit
Synthesis.
(by Tomohiro Yoneda, Chris J. Myers, JP) |
|
Synthesis for Probabilistic Environments.
(by Sven Schewe , DE) |
11:00-11:30 | Coffee Break |
11:30-13:30 |
Session 6: Realtime and Hybrid Systems
(Session Chair: Hsu-Chun Yen)
|
|
Branching-Time Property Preservation Real-time Systems.
(by Jinfeng Huang, Marc Geilen, Jeroen Voeten, Henk Corporaal
, NL) |
|
Automatic Verification of Hybrid Systems with Large Discrete State Space.
(by Werner Damm,
Stefan Disch,
Hardi Hungar,
Jun Pang,
Florian Pigorsch,
Christoph Scholl,
Uwe Waldmann,
Boris Wirtz
, DE) |
|
Timed Unfoldings for Networks of Timed Automata.
(by Patricia Bouyer, Serge Haddad, Pierre-Alain Reynier
, FR) |
|
Symbolic Unfoldings For Networks of Timed Automata.
(by Franck Cassez, Thomas Chatain, Claude Jard
, FR) |
13:30-14:10 | Business Meeting & Lunch Break |
14:10-18:30 |
Social Event: Sightseeing to the Great Wall (Ba Da Ling) |
19:00-21:30 |
Banquet |
08:30-09:30 |
Keynote Speech by Thomas Ball
(Session Chair: Susanne Graf)
|
|
Automated Abstraction of Software
|
09:30-11:00 |
Session 7: Abstraction
(Session Chair: Susanne Graf)
|
|
Ranked Predicate Abstraction for Branching Time: Complete, Incremental,
and Precise.
(by Harald Fecher, Michael Huth
, DE) |
|
Timed Temporal Logics for Abstracting Transient States.
(by Houda Bel Mokadem, Béatrice Bérard, Patricia Bouyer, François Laroussinie
, FR) |
|
Predicate Abstraction of Programs Containing Non-linear Computation.
(by Songtao Xia, Ben Di Vito, Cesar Munoz
, US) |
11:00-11:30 | Coffee Break |
11:30-13:00 |
Session 8: Communicating Systems and Testing
(Session Chair: Thomas Ball)
|
|
A Fresh Look at Testing for Asynchronous Communication.
(by Puneet Bhateja, Paul Gastin, Madhavan Mukund
, IN) |
|
Proactive Leader Election in Asynchronous Shared Memory Systems.
(by M. C. Dharmadeep, K. Gopinath
, IN) |
|
A Semantic Framework for Test Coverage.
(by Laura Brandán Briones, Ed Brinksma, Mariëlle Stoelinga
, NL) |
13:00-14:00 | Lunch Break and PC meeting |
14:00-16:00 |
Session 9: Protocols and Security
(Session Chair: Bow-Yaw Wang)
|
|
Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols.
(by Giorgio Delzanno, Javier Esparza, Jiri Srba
, DK) |
|
Analyzing Security Protocols in Hierarchical Networks.
(by Ye Zhang, Hanne Riis Nielson
, DK) |
|
Functional Analysis of a Real-Time Protocol for Networked Control Systems.
(by Colin Fidge, Yu-Chu Tian
, AU) |
|
Symbolic Semantics for the Verification of Security Properties of Mobile
Petri Nets.
(by Fernando Rosa-Velardo, David de Frutos-Escrig
, ES) |
16:00-16:15 | Coffee Break |
16:15-18:15 |
Session 10: Bisimulation and Model Checking
(Session Chair: Huimin Lin)
|
|
Sigref - A Symbolic Bisimulation Tool Box.
(by Ralf Wimmer, Marc Herbstritt, Holger Hermanns, Kelley Strampp, Bernd Becker
, DE) |
|
Towards a Model-Checker for Counter Systems.
(by Stephane Demri, Alain Finkel, Valentin Goranko, Govert van Drimmelen
, FR) |
|
The Implementation of Mazurkievicz Traces in POEM.
(by Peter Niebert, Hongyang Qu
, FR) |
|
Model-Based Tool-Chain Infrastructure for Automated Analysis of Embedded
Systems.
(by Hang Su, Graham Hemingway, Kai Chen, T. John Koo
, US) |
18:15-18:30 |
Closing |