6. ATVA 2008: Seoul, Korea

Sung Deok Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee, Mahesh Viswanathan (Eds.): Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008. Proceedings. Lecture Notes in Computer Science 5311 Springer 2008, ISBN 978-3-540-88386-9

Invited Talks

Alessandro Ferrante, Margherita Napoli, Mimmo Parente:
CTLModel-Checking with Graded Quantifiers. 18-32
Gal Katz, Doron Peled:
Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms. 33-47
Radu Mateescu, Pedro T. Monteiro, Estelle Dumas, Hidde de Jong:
Computation Tree Regular Logic for Genetic Regulatory Networks. 48-63
Saddek Bensalem, Marius Bozga, Joseph Sifakis, Thanh-Hung Nguyen:
Compositional Verification for Component-Based Systems and Application. 64-79
Jefferson O. Andrade, Yukiyoshi Kameyama:
A Direct Algorithm for Multi-valued Bounded Model Checking. 80-94

Arie Gurfinkel, Ou Wei, Marsha Chechik:
Model Checking Recursive Programs with Exact Predicate Abstraction. 95-110
Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger:
Loop Summarization Using Abstract Transformers. 111-125
Chao Wang, Yu Yang, Aarti Gupta, Ganesh Gopalakrishnan:
Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions. 126-140

Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif:
Automating Algebraic Specifications of Non-freely Generated Data Types. 141-155
Christopher Lynch, Yuefeng Tang:
Interpolants for Linear Arithmetic in SMT. 156-170
Andreas Eggers, Martin Fränzle, Christian Herde:
SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems. 171-185
Christopher Lynch, Duc-Khanh Tran:
SMELS: Satisfiability Modulo Equality with Lazy Superposition. 186-200

Robert M. Hierons, Mercedes G. Merayo, Manuel Núñez:
Controllable Test Cases for the Distributed Test Architecture. 201-215

Ralf Huuck, Ansgar Fehnker, Sean Seefried, Jörg Brauer:
Goanna: Syntactic Software Model Checking. 216-221
Ansuman Banerjee, Sayak Ray, Pallab Dasgupta, Partha Pratim Chakrabarti, S. Ramesh, P. Vignesh V. Ganesan:
A Dynamic Assertion-Based Verification Platform for Validation of UML Designs. 222-227
Ansuman Banerjee, Kausik Datta, Pallab Dasgupta:
CheckSpec: A Tool for Consistency and Coverage Analysis of Assertion Specifications. 228-233
Jiri Barnat, Lubos Brim, Petr Rockai:
DiVinE Multi-Core - A Parallel LTL Model-Checker. 234-239
Martin De Wulf, Laurent Doyen, Nicolas Maquet, Jean-François Raskin:
Alaska. 240-245
Elie Bursztein:
NetQi: A Model Checker for Anticipation Game. 246-251
John Håkansson, Jan Carlson, Aurelien Monot, Paul Pettersson, Davor Slutej:
Component-Based Design and Analysis of Embedded Systems with UPPAAL PORT. 252-257

Farn Wang:
Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions. 258-273
Alberto Casagrande, Pietro Corvaja, Carla Piazza, Bud Mishra:
Decidable Compositions of O-Minimal Automata. 274-288
Nawel Gharbi:
On the Applicability of Stochastic Petri Nets for Analysis of Multiserver Retrial Systems with Different Vacation Policies. 289-302
Eckard Böde, Thomas Peikenkamp, Jan Rakow, Samuel Wischmeyer:
Model Based Importance Analysis for Minimal Cut Sets. 303-317

Hiroaki Shimizu, Kiyoharu Hamaguchi, Toshinobu Kashiwabara:
Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic. 318-331
Blaise Genest, Anca Muscholl, Olivier Serre, Marc Zeitoun:
Tree Pattern Rewriting Systems. 332-346
Lingyun Luo:
Deciding Bisimilarity of Full BPA Processes Locally. 347-360
Florian Horn, Wolfgang Thomas, Nico Wallmeier:
Optimal Strategy Synthesis in Request-Response Games. 361-373

Guoqiang Li, Mizuhito Ogawa:
Authentication Revisited: Flaw or Not, the Recursive Authentication Protocol. 374-385
Wei Dong, Martin Leucker, Christian Schallhart:
Impartial Anticipation in Runtime-Verification. 386-396
Marcel Kyas, Cristian Prisacariu, Gerardo Schneider:
Run-Time Monitoring of Electronic Contracts. 397-407
Carlo A. Furia, Paola Spoletini:
Practical Efficient Modular Linear-Time Model-Checking. 408-417
César Andrés, Mercedes G. Merayo, Manuel Núñez:
Passive Testing of Timed Systems. 418-427