7. ATVA 2009: Macao, China

Zhiming Liu, Anders P. Ravn (Eds.): Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings. Lecture Notes in Computer Science 5799 Springer 2009, ISBN 978-3-642-04760-2

Invited Talks

Mark R. Greenstreet:
Verifying VLSI Circuits. 1-20
Orna Grumberg:
3-Valued Abstraction for (Bounded) Model Checking. 21
A. W. Roscoe, Philip J. Armstrong, Pragyesh:
Local Search in Model Checking. 22-38

State Space Reduction

Jaco Geldenhuys, Henri Hansen, Antti Valmari:
Exploring the Scope for Partial Order Reduction. 39-53
Jaco van de Pol, Mark Timmer:
State Space Reduction of Linear Processes Using Control Flow Reconstruction. 54-68
Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu:
A Data Symmetry Reduction Technique for Temporal-epistemic Logic. 69-83

Tools

Joakim Byg, Kenneth Yrke Jørgensen, Jirí Srba:
TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets. 84-89
Stephen Fenech, Gordon J. Pace, Gerardo Schneider:
CLAN: A Tool for Contract Analysis and Conflict Discovery. 90-96
Michal Kebrt, Ondrej Sery:
UnitCheck: Unit Testing and Model Checking Combined. 97-103

Probabilistic Systems

Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre:
LTL Model Checking of Time-Inhomogeneous Markov Chains. 104-119
Diana El Rabih, Nihal Pekergin:
Statistical Model Checking Using Perfect Simulation. 120-134
Christel Baier, Marcus Größer, Frank Ciesinski:
Quantitative Analysis under Fairness Constraints. 135-150
Jens Oehlerking, Oliver E. Theel:
A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems. 151-165

Medley

Guanhua He, Shengchao Qin, Chenguang Luo, Wei-Ngan Chin:
Memory Usage Verification Using Hip/Sleek. 166-181
Oliver Friedmann, Martin Lange:
Solving Parity Games in Practice. 182-196
Parosh Aziz Abdulla, Muhsin Atto, Jonathan Cederberg, Ran Ji:
Automated Analysis of Data-Dependent Programs with Dynamic Memory. 197-212

Temporal Logic I

Alexandre Duret-Lutz, Denis Poitrenaud, Jean-Michel Couvreur:
On-the-fly Emptiness Check of Transition-Based Streett Automata. 213-227
Hrishikesh Karmarkar, Supratik Chakraborty:
On Minimal Odd Rankings for Büchi Complementation. 228-243
Christian Dax, Felix Klaedtke, Stefan Leue:
Specification Languages for Stutter-Invariant Regular Properties. 244-254

Abstraction and Refinement

Ansgar Fehnker, Ralf Huuck, Sean Seefried:
Incremental False Path Elimination for Static Software Analysis. 255-270
Yael Meller, Orna Grumberg, Sharon Shoham:
A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement. 271-288
Alarico Campetelli, Alexander Gruler, Martin Leucker, Daniel Thoma:
Don't Know for Multi-valued Systems. 289-305
Jacob M. Howe, Andy King:
Logahedra: A New Weakly Relational Domain. 306-320

Fault Tolerant Systems

Rayna Dimitrova, Bernd Finkbeiner:
Synthesis of Fault-Tolerant Distributed Systems. 321-336
Sandip Ray, Kecheng Hao, Yan Chen, Fei Xie, Jin Yang:
Formal Verification for High-Assurance Behavioral Synthesis. 337-351
Franck Cassez, Jérémy Dubreil, Hervé Marchand:
Dynamic Observers for the Synthesis of Opaque Systems. 352-367

Temporal Logic II

Yang Zhao, Gianfranco Ciardo:
Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation. 368-381
Geng-Dian Huang, Lin-Zan Cai, Farn Wang:
LTL Model Checking for Recursive Programs. 382-396
Hongtao Huang:
On Detecting Regular Predicates in Distributed Systems. 397-411

Last update Sat May 25 02:00:57 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page