ATVA 2008

International Symposium on

Automated Technology for Verification and Analysis

October 20-23, 2008

Korea University, Seoul Korea

Day 1: October 20 (Monday)

09 : 00 - 10 : 00	Registration
10 : 00 - 12 : 00	Tutorial 1 : Logic in Specification and Verification (abstract) Natarajan Shankar (SRI) Session Chair : Sungdeok Cha
12 : 00 - 13 : 00	Lunch
13 : 00 - 15 : 00	Tutorial 2 : Boolean Modeling of Cell Biology (abstract) David Dill (Stanford) Session Chair : Dolon Peled
15 : 00 - 15 : 30	Coffee Break
15 : 30 - 17 : 30	Tutorial 3 : Checking Object Invariants by Combining Static and Dynamic Analysis (abstract) Sriram Rajamani (Microsoft Research India) Session Chair : Moonzoo Kim
17 : 30 - 20 : 00	Reception

Day 2: October 21 (Tuesday)

08 : 45 - 09 : 00	Opening
09 : 00 - 10 : 00	Keynote 1 : Tests, Proofs and Refinements Sriram Rajamani (Microsoft Research India)
10 : 00 - 10 : 30	Coffee Break
10 : 30 - 13 : 00	Session 1 : Model Checking Session Chair : Yunja Choi CTL Model-Checking with Graded Quantifiers Alessandro Ferrante, Margherita Napoli, Mimmo Parente Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms Gal Katz, Doron Peled Computation Tree Regular Logic for Genetic Regulatory Networks Radu Mateescu, Pedro T. Monteiro, Estelle Dumas, Hidde de Jong Compositional Verification for Component-based Systems and Application Saddek Bensalem, Marius Bozga, Joseph Sifakis, Thanh-Hung Nguyen A Direct Algorithm for Multi-Valued Bounded Model Checking Jefferson Andrade, Yukiyoshi Kameyama
13 : 00 - 14 : 00	Lunch
14 : 00 - 15 : 50	Session 2 : Software Verification Session Chair : Bow-Yaw Wang Model Checking Recursive Programs with Exact Predicate Abstraction Arie Gurfinkel, Ou Wei, Marsha Chechik Loop Summarization using Abstract Transformers Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph Wintersteiger Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions Chao Wang, Yu Yang, Aarti Gupta, Ganesh Gopalakrishnan Authentication Revisited : Flaw or Not, the Recursive Authentication Protocol(short) Guoqiang Li, Mizuhito Ogawa
15 : 50 - 16 : 00	Coffee Break
16 : 00 - 17 : 00	Local Keynote : Software Quality in Consumer Electronics: Issues and Challenges In-Kyung Ryu (LG Electronics Software Center)
17 : 00 - 19 : 00	Session 3 : Decision Procedures Session Chair : Mizuhito Ogawa Automating Algebraic Specifications of Non-freely Generated Data Types Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif Interpolants for linear arithmetic in SMT Yuefeng Tang, Christopher Lynch SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems Andreas Eggers, Martin Frazle, Christian Herde SMELS: Satisfiability Modulo Equality with Lazy Superposition Christopher Lynch, Duc-Khanh Tran

Day 3: October 22 (Wednesday)

09 : 00 - 10 : 00	Keynote 2 : Formal Verification and Biology David Dill (Stanford)
10 : 00 - 10 : 30	Coffee Break
10 : 30 - 12 : 00	Session 4 : Linear Time Analysis Session Chair : Saddek Bensalem Controllable Test Cases for the Distributed Test Architecture Rob Hierons, Mercedes Merayo, Manuel Nunez Impartial Anticipation in Runtime-Verification (short) Wei Dong, Martin Leucker, Christian Schallhart Run-time Monitoring of Electronic Contracts (short) Marcel Kyas, Cristian Prisacariu, Gerardo Schneider Practical Efficient Modular Linear-Time Model-Checking (short) Carlo Alberto Furia, Paola Spoletini
12 : 00 - 13 : 00	Lunch
13 : 00 - 18 : 00	Excursion (Kyoung-Bok Palace + Korean Folk Museum/ Biwon)
18 : 00 - 20 : 00	Banquet

Day 4: October 23 (Thursday)

09 : 00 - 10 : 00	Keynote 3 : Trust and Automation in Verification Tools Natarajan Shankar (SRI)
10 : 00 - 10 : 15	Coffee Break
10 : 15 - 12 : 00	Session 5 : Tool Demonstration Papers Session Chair : Martin Leucker Goanna: Syntactic Software Model Checking Ralf Huuck, Ansgar Fehnker, Sean Seefried, Joerg Brauer A Dynamic Assertion-based Verification Platform for Validation of UML designs Ansuman Banerjee, Sayak Ray, Pallab Dasgupta, Partha Pratim Chakrabarti, S. Ramesh, P Vignesh Ganesan CheckSpec: A Tool for Consistency and Coverage analysis of Assertion Specifications Ansuman Banerjee, Kausik Datta, Pallab Dasgupta DiVinE Multi-Core - A Parallel LTL Model-Checker Jiri Barnat, Lubos Brim, Petr Rockai Alaska: Antichains of Logic, Automata and Symbolic Kripke structures Analysis Martin De Wulf, Laurent Doyen, Jean-Francois Raskin, Nicolas Maquet NetQi: A Model checker for Anticipation Game Elie Bursztein Component-Based Design and Analysis of Embedded Systems with UPPAAL PORT John Hakansson, Jan Carlson, Aurelien Monot, Paul Pettersson, Davor Slutej
12 : 00 - 13 : 30	Lunch
13 : 30 - 15 : 50	Session 6 : Timed & Stochastic Systems Session Chair : Gihwon Kwon Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions Farn Wang Decidable Compositions of O-minimal Automata Alberto Casagrande, Pietro Corvaja, Carla Piazza, Bud Mishra On the Applicability of Stochastic Petri Nets for Analysis of Multiserver Retrial Systems with Different Vacation Policies Nawel Gharbi Model Based Importance Analysis for Minimal Cut Sets Eckard Bode, Thomas Peikenkamp, Jan-Hendrik Rakow, Samuel Wischmeyer Passive Testing of Timed Systems(short) Cesar Andres, Mercedes Merayo, Manuel Nunez	Tool Demonstrations
15 : 50 - 16 : 30	Coffee Break
16 : 30 - 18 : 30	Session 7 : Theory Session Chair : Manuel Nunez Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic Hiroaki Shimizu, Kiyoharu Hamaguchi, Toshinobu Kashiwabara Tree Pattern Rewriting Systems Blaise Genest, Anca Muscholl, Olivier Serre, Marc Zeitoun Deciding Bisimilarity of Full BPA Processes Locally Lingyun Luo Optimal Strategy Synthesis in Request-Response Games Florian Horn, Wolfgang Thomas, Nico Wallmeier

Tutorial 1

Title	Logic in Specification and Verification
Speaker	Natarajan Shankar (SRI)
Abstract	We explore the effective use of logic with automated tools such as PVS, Yices, and SAL. We look at the range of choices in logics and languages, modeling and formalization, and automation and interaction. PVS is a general-purpose framework for specification and verification. SAL is specialized to transition systems. Yices is a solver for satisfiability modulo theories.

Tutorial 2

Title	Boolean Modeling of Cell Biology
Speaker	David Dill (Stanford)
Abstract	Over the years, models similar to digital logic have been used in cell biology. Because much of the initial work was done by people not from the digital design community, there has been a certain amount of parallel evolution, where the questions asked and techniques used are sometimes different from the approaches used in the design of digital systems designed by engineers.  This tutorial will discuss why Boolean models of cell biology might be appropriate and useful, survey past work in the area, and compare with approaches used in analysis of human-designed systems, such as model checking.

Tutorial 3

Title	Checking Object Invariants by Combining Static and Dynamic Analysis
Speaker	Sriram Rajamani (Microsoft Research India)
Abstract	We consider object protocols that constrain interactions between objects in a program. The goal of an object protocol is expressed as a protocol invariant. Fundamental properties such as ownership can be expressed as protocol invariants. We present a language, PROLANG, to specify object protocols along with their protocol invariants, and a tool, INVCOP++, to check if a program satisfies a protocol invariant. INVCOP++ separates the problem of checking if a protocol satisfies its protocol invariant (called protocol correctness), from the problem of checking if a program conforms to a protocol (called program conformance). The former is solved using static analysis, and the latter using runtime analysis. We present theoretical guarantees about the way we combine static and runtime analysis, and empirical evidence that our tool INVCOP++ finds usage errors in widely used APIs. We also show that statically checking protocol correctness greatly optimizes the overhead of checking program conformance, thus enabling API clients to test whether their programs use the API as intended by the API designer.