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