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.