Home

Call for Papers
[ PDF | TXT ]

Paper submissions
Accepted papers
Conference program
[ PDF]
Accomodation
Registration
Social events
Travel and local information
Organization
Poster

 

Previous ATVAs
ATVA 2007
ATVA 2006
ATVA 2005
ATVA 2004
ATVA 2003

 

ATVA2008 is sponsored by the following institutions and companies:
 
 
ATVA2008 is organized by the following society:
 
 
For further information, please contact
kimyunho@kaist.ac.kr
 
 
Last updated: Aug 11,2008



 

Research Papers

  • Automating Algebraic Specifications of Non-freely Generated Data Types
    Andriy Dunets, Gerhard Schellhorn and Wolfgang Reif.
  • Optimal Strategy Synthesis in Request Response Games
    Florian Horn, Wolfgang Thomas and Nico Wallmeier.
  • Model Checking Recursive Programs with Exact Predicate Abstraction
    Arie Gurfinkel, Ou Wei and Marsha Chechik.
  • Yices Interpolants
    Yuefeng tang and Christopher Lynch.
  • SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
    Andreas Eggers, Martin Franzle and Christian Herde.
  • Deciding bisimilarity of full BPA processes locally
    Lingyun Luo.
  • Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic
    Hiroaki Shimizu, Kiyoharu Hamaguchi and Toshinobu Kashiwabara.
  • Compositional Verification for Component-based Systems and Application
    Saddek Bensalem, Marius Bozga, Joseph Sifakis and Thanh-Hung Nguyen.
  • Decidable Compositions of O-minimal Automata
    Alberto Casagrande, Pietro Corvaja, Carla Piazza and Bud Mishra.
  • CTL Model-Checking with Graded Quantifiers
    Alessandro Ferrante, Margherita Napoli and Mimmo Parente.
  • Model Based Importance Analysis for Minimal Cut Sets
    Thomas Peikenkamp, Eckard Bode, Jan-Hendrik Rakow and Samuel Wischmeyer.
  • A Direct Algorithm for Multi-Valued Bounded Model Checking
    Jefferson Andrade and Yukiyoshi Kameyama.
  • On the Applicability of Stochastic Petri Nets for Analysis of Multiserver Retrial Systems with Different Vacation Policies
    Nawel GHARBI.
  • Controllable test cases for the distributed test architecture
    Rob Hierons, Mercedes Merayo and Manuel Nunez.
  • Loop Summarization using Abstract Transformers
    Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich and Christoph Wintersteiger.
  • Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
    Chao Wang, Yu Yang, Aarti Gupta and Ganesh Gopalakrishnan.
  • Tree Pattern Rewriting Systems
    Blaise genest, Anca Muscholl, Olivier Serre and Marc Zeitoun.
  • Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms
    Gal Katz and Doron Peled.
  • SMELS: Satisfiability Modulo Equality with Lazy Superposition
    Christopher Lynch and Duc-Khanh Tran.
  • Computation Tree Regular Logic for Genetic Regulatory Networks
    Radu Mateescu, Pedro T. Monteiro, Estelle Dumas and Hidde de Jong.
  • Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions
    Farn Wang.

  • Tool Demonstration Papers


  • DiVinE Multi-Core -- A Parallel LTL Model-Checker
    Jiri Barnat, Lubos Brim and Petr Rockai.
  • Alaska : Antichains for Logic, Automata and Symbolic Kripke structure Analysis
    Martin De Wulf, Laurent Doyen, Jean-Francois Raskin and Nicolas Maquet.
  • CheckSpec: A Tool for Consistency and Coverage analysis of Assertion Specifications
    Ansuman Banerjee, Kausik Datta and Pallab Dasgupta.
  • A Dynamic Assertion-based Verification Platform for Validation of UML designs
    Ansuman Banerjee, Sayak Ray, Pallab Dasgupta, Chakrabarti P P Chakrabarti P P, Ramesh S and P Vignesh Ganesan.
  • Goanna: Syntactic Software Model Checking
    Ralf Huuck, Ansgar Fehnker, Sean Seefried and Joerg Brauer.
  • Component-Based Design and Analysis of Embedded Systems with UPPAAL PORT
    John Hakansson, Paul Pettersson, Jan Carlson, Davor Slutej and aurelien monot.
  • NetQi: A Model checker for Anticipation Game
    Elie Bursztein.

  • Short Research Papers


  • Authentication Revisited - Flaw or Not, the Recursive Authentication
    Guoqiang Li and Mizuhito Ogawa
  • Practical Efficient Modular Linear-Time Model-Checking
    Carlo Alberto Furia and Paola Spoletini.
  • Passive Testing of Timed Systems
    Cesar Andres, Mercedes Merayo and Manuel Nunez
  • Run-time Monitoring of Electronic Contracts
    Marcel Kyas, Cristian Prisacariu, and Gerardo Schneider
  • Impartial Anticipation in Runtime-Verification
    Wei Dong, Martin Leucker and Christian Schallhart
  •