Call for Papers
[ PDF | TXT ]

Paper submissions
Accepted papers
Conference program
[ PDF]
Social events
Travel and local information


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
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