[Om-announce] Call for Participation: ATVA 2010, 21st - 24th Singapore

[jun sun]

                  C A L L     F O R     P A R T I C I P A T I O N

8th International Symposium on Automated Technology for Verification
and Analysis
                                 (ATVA 2010)

      12th International Workshop on Verification of Infinite State Systems
                               (INFINITY 2010)

                        21st - 24th Sept 2010, SINGAPORE

        Registration and Hotel Details at : http://atva10.comp.nus.edu.sg
                 (Early Registration Deadline on 20th Aug 2010)


Day 1: 21th Sept 2010

 09:00 - 10:30 : ATVA Invited Tutorial (Igor Walukiewicz)
 10:30 - 11:00 : Coffee Break
 11:00 - 12:00 : INFINITY Invited Talk 1 (Ahmed Bouajjani)
 12:00 - 13:00 : Session 1 : Concurrency I
                           : INFINITY Session I
 13:00 - 14:00 : Lunch
 14:00 - 15:00 : INFINITY Invited Talk 2 (Tomas Vojnar)
 15:00 - 16:00 : Session 2 : Concurrency II
                           : INFINITY Session II
 16:00 - 16:30 : Coffee Break
 16:30 - 17:30 : INFINITY Invited Talk 3 (Parosh Abdulla)
 17:30 - 18:45 : Session 3 : Tools I
                           : INFINITY Session III
 19:00 - 20:30 : ATVA/INFINITY Reception

Day 2: 22th Sept 2010

 09:00 - 10:00 : Keynote Talk 1 (Igor Walukiewicz)
                  Synthesis : Words and Traces
 10:00 - 10:30 : Coffee Break
 10:30 - 12:00 : Session 4 : Verification Mechanisms
 12:00 - 13:30 : Lunch
 13:30 - 15:00 : Session 5 : Model Checking and Abstractions
 15:00 - 15:30 : Coffee Break
 15:30 - 17:30 : Session 6 : Tools II

Day 3: 23rd Sept 2010

 09:00 - 10:00 : Keynote Talk 2 (Joxan Jaffar)
                  Abstraction Learning
 10:00 - 10:30 : Coffee Break
 10:30 - 12:00 : Session 7 : Specification Formalisms
 12:00 - 13:30 : Lunch
 13:30 - 15:00 : ATVA Invited Tutorial 2 (Thomas Henzinger)
 15:00 - 15:30 : Coffee Break
 15:30 - 17:30 : Session 8 :  Automata & LTL
 18:00 - 20:00 : ATVA Banquet

Day 4: 24th Sept 2010

 09:00 - 10:00 : Keynote Talk 3 (Thomas Henzinger)
                  Probabilistic Automata on Infinte Words :
                   Decidability and Undecidability Results
 10:00 - 10:30 : Coffee Break
 10:30 - 12:30 : Session 9 : Timed and Hybrid Systems

-------------------
Sessions for 21Sept
-------------------

Concurrency Reasoning I (12:00-13:00)
======================================

Methods for Knowledge Based Controlling of Distributed Systems
Saddek Bensalem, Marius Bozga, Susanne Graf, Doron Peled, Sophie Quinton.

Non-Monotonic Refinement of Control Abstraction for Concurrent Programs
Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko.

INFINITY Session I (12:00 - 13:00)
==================================
On interleaving in {P,A}-Time Petri nets with strong semantics (Regular)
Hanifa Boucheneb and Kamel Barkaoui.

On Zone-Based Analysis of Duration Probabilistic Automata (Regular)
Oded Maler, Bruce Krogh, Kim G. Larsen.

Concurrency Reasoning II (15:00-16:00)
======================================

Symbolic Unfolding of Parametric Stopwatch Petri Nets
Louis-Marie Traonouez, Bartosz Grabiec, Claude Jard, Didier Lime,
Olivier H. Roux.

A Study of the Convergence of Steady State Probabilities in a Closed
Fork-Join Network
Guy Edward Gallasch and Jonathan Billington.

INFINITY Session II (15:00 - 16:00)
==================================

On Selective Unboundedness (Regular)
Stephane Demri.

Implicit Real Vector Automata (Regular)
Bernard Boigelot, Julien Brusten, Jean-Francois Degbomont.

Tools I (17:30-18:30)
=====================

Model-checking Web Applications with Web-TLR
Mara Alpuente, Demis Ballis, Javier Espert, Daniel Romero.

Developing Model Checkers Using PAT
Yang Liu, Jun Sun, Jinsong Dong.

MCGP: A Software Synthesis Tool Based on Model Checking and Genetic Programming
Gal Katz and Doron Peled.

INFINITY Session III (17:30 - 18:45)
==================================

Probabilistic Regular Graphs (Regular)
Nathalie Bertrand and Christophe Morvan.

A Decidable Characterization of a Graphical Pi-calculus with Iterators (Regular)
Frederic Peschanski, Hanna Klaudel, Raymond Devillers.

IMITATOR II: A Tool for Solving the Good Parameters Problem in Timed
Automata (Tool)
Etienne Andre.

-------------------
Sessions for 22Sept
-------------------

Verification Mechanisms (10:30-12:00)
=====================================

What's Decidable About Sequences?
Carlo Alberto Furia.

A Specification Logic for Exceptions and Beyond
Cristian Gherghina and Cristina David.

Reachability as deducibility, finite countermodels and verification
Alexei Lisitsa.

Model Checking and Abstractions (13:30-15:00)
=============================================

Lattice-Valued Binary Decision Diagrams
Gilles Geeraerts, Gabriel Kalyon, Tristan Le Gall, Nicolas Maquet,
Jean-Francois Raskin.

Auxiliary Constructs for Proving Liveness in Compassion Discrete Systems
Long Teng and Zhang Wenhui.

On Scenario Synchronization
Duc-Hanh Dang, Anh-Hoang Truong, Martin Gogolla.

Tools II (15:30-17:30)
======================
Ecdar: An Environment for Compositional Design and Analysis of Real Time Systems
Axel Legay, Alexandre David, Kim G. Larsen, Ulrik Nyman, Andrzej Wasowski.

GAVS: Game Arena Visualization and Synthesis
Chih-Hong Cheng, Christian Buckl, Michael Ruttenberger, Alois Knoll

YAGA: Automated Analysis of Quantitative Safety Specifications in
Probabilistic B
Ukachukwu Ndukwu and Annabelle McIver.

Rbminer: A tool for discovering Petri nets from transition  systems
Marc Sol and Josep Carmona.

CRI: Symbolic Debugger for MCAPI Applications
Mohamed Elwakil, Zijiang Yang, Liqiang Wang

COMBINE: A Tool on Combined Formal Methods for Bindingly Verification
An N. Nguyen, Tho T. Quan, Phung H. Nguyen, Thang H. Bui.

-------------------
Sessions for 23Sept
-------------------

Specification Formalism (10:30-12:00)
=====================================

Probabilistic Contracts for Component-based Design
Dana N. Xu, Gregor Goessler, Alain Girault.

Automatic generation of history-based access control from information
flow specification
Yoshiaki Takata and Hiroyuki Seki.

An Approach for Class Testing from Class Contracts
Atul Gupta

Automata and LTL (10:30-12:30)
==============================

Promptness in Omega-regular Automata
Shaull Almagor, Yoram Hirshfeld, Orna Kupferman

Efficient On-The-Fly Emptiness Check for Timed Buchi Automata
Frdric Herbreteau and B Srivathsan.

Compositional Algorithms for LTL Synthesis
Emmanuel Filiot, Naiyong Jin, Jean-Francois Raskin.

LTL can be more succinct
Kamal Lodaya and Sreejith A V.

------------------
Session for 24Sept
------------------

Timed and Hybrid Systems (15:30-17:30)
======================================

Composing Reachability Analyses of Hybrid Systesm for Safety and Stability
Sergiy Bogomolov, Corina Mitrohin, Andreas Podelski

Using Redundant Constraints for Refinement
Eugene Asarin, Thao Dang, Oded Maler, Romain Testylier.

Recursive Timed Automata
Ashutosh Trivedi and Dominik Wojtczak.

The Complexity of Codiagnosability for Discrete Event and Timed Systems
Franck Cassez.



-- 
yours,
Sun Jun