9. ATVA 2011: Taipei, Taiwan

Invited Papers

• Edmund M. Clarke, Paolo Zuliani:
  Statistical Model Checking for Cyber-Physical Systems. 1-12
  
• Shaull Almagor, Orna Kupferman:
  Max and Sum Semantics for Alternating Weighted Automata. 13-27
  
• Jade Alglave, Alastair F. Donaldson, Daniel Kroening, Michael Tautschnig:
  Making Software Verification Tools Really Work. 28-42
  
• Masahiro Fujita:
  Synthesizing, Verifying, and Debugging SoC with FSM-Based Specification of On-Chip Communication Protocols. 43-50
  
• Moonzoo Kim, Yunho Kim:
  Automated Analysis of Industrial Embedded Software. 51-59
  

Regular Papers

• Miguel A. Carrillo, David A. Rosenblueth:
  Nondeterministic Update of CTL Models by Preserving Satisfaction through Protections. 60-74
  
• Morten Dahl, Naoki Kobayashi, Yunde Sun, Hans Hüttel:
  Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols. 75-89
  
• Liya Liu, Osman Hasan, Sofiène Tahar:
  Formalization of Finite-State Discrete-Time Markov Chains in HOL. 90-104
  
• Jean-Paul Bodeveix, Abdeldjalil Boudjadar, Mamoun Filali:
  An Alternative Definition for Timed Automata Composition. 105-119
  
• Hongfei Fu:
  Model Checking EGF on Basic Parallel Processes. 120-134
  
• Patricia Bouyer, Nicolas Markey, Jörg Olschewski, Michael Ummels:
  Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited. 135-149
  
• Chih-Hong Cheng, Saddek Bensalem, Yu-Fang Chen, Rongjie Yan, Barbara Jobstmann, Harald Ruess, Christian Buckl, Alois Knoll:
  Algorithms for Synthesizing Priorities in Component-Based Systems. 150-167
  
• Dominik Wojtczak:
  Trust Metrics for the SPKI/SDSI Authorisation Framework. 168-182
  
• Thomas Brihaye, Véronique Bruyère, Laurent Doyen, Marc Ducobu, Jean-François Raskin:
  Antichain-Based QBF Solving. 183-197
  
• Janusz Malinowski, Peter Niebert, Pierre-Alain Reynier:
  A Hierarchical Approach for the Synthesis of Stabilizing Controllers for Hybrid Systems. 198-212
  
• Benjamin Aminof, Orna Kupferman, Robby Lampert:
  Formal Analysis of Online Algorithms. 213-227
  
• Nikola Benes, Ivana Cerná, Jan Kretínský:
  Modal Transition Systems: Composition and LTL Model Checking. 228-242
  
• Lukás Holík, Ondrej Lengál, Jirí Simácek, Tomás Vojnar:
  Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata. 243-258
  
• Philippe Darondeau, Loïc Hélouët, Madhavan Mukund:
  Assembling Sessions. 259-274
  
• Nikola Benes, Jan Kretínský, Kim G. Larsen, Mikael H. Møller, Jirí Srba:
  Parametric Modal Transition Systems. 275-289
  
• Pascal Sotin, Bertrand Jeannet, Franck Védrine, Eric Goubault:
  Policy Iteration within Logico-Numerical Abstract Domains. 290-305
  
• Daniel Neider:
  Small Strategies for Safety Games. 306-320
  
• Alfons Laarman, Rom Langerak, Jaco van de Pol, Michael Weber, Anton Wijs:
  Multi-core Nested Depth-First Search. 321-335
  
• Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg:
  Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking. 336-350
  
• Mohamed Nassim Seghir:
  A Lightweight Approach for Loop Summarization. 351-365
  
• Sofia Cassel, Falk Howar, Bengt Jonsson, Maik Merten, Bernhard Steffen:
  A Succinct Canonical Register Automaton Model. 366-380
  
• Sami Evangelista, Laure Petrucci, Samir Youcef:
  Parallel Nested Depth-First Searches for LTL Model Checking. 381-396
  
• Viktor Schuppan, Luthfi Darmawan:
  Evaluating LTL Satisfiability Solvers. 397-413
  

Tool Papers

• Mingsong Lv, Nan Guan, Qingxu Deng, Ge Yu, Wang Yi:
  McAiT - A Timing Analyzer for Multicore Real-Time Software. 414-417
  
• Sebastian S. Bauer, Philip Mayer, Axel Legay:
  MIO Workbench: A Tool for Compositional Design with Modal Input/Output Interfaces. 418-421
  

Short Papers

• Gal Katz, Doron Peled, Sven Schewe:
  The Buck Stops Here: Order, Chance, and Coordination in Distributed Control. 422-431
  
• Xiaoqing Jin, Gianfranco Ciardo, Tae-Hyong Kim, Yang Zhao:
  Symbolic Verification and Test Generation for a Network of Communicating FSMs. 432-442
  
• Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker:
  Hierarchical Counterexamples for Discrete-Time Markov Chains. 443-452
  
• Jan Obdrzálek, Marek Trtík:
  Efficient Loop Navigation for Symbolic Execution. 453-462
  
• Shang-Wei Lin, Étienne André, Jin Song Dong, Jun Sun, Yang Liu:
  An Efficient Algorithm for Learning Event-Recording Automata. 463-472
  
• Thao Dang, Thomas Martin Gawlitza:
  Discretizing Affine Hybrid Automata with Uncertainty. 473-481
  
• Shaull Almagor, Udi Boker, Orna Kupferman:
  What's Decidable about Weighted Automata? 482-491
  
• Lies Lakhdar-Chaouch, Bertrand Jeannet, Alain Girault:
  Widening with Thresholds for Programs with Complex Control Graphs. 492-502
  
• Houssam Abbas, Georgios E. Fainekos:
  Linear Hybrid System Falsification through Local Search. 503-510
  
• Lu Feng, Tingting Han, Marta Z. Kwiatkowska, David Parker:
  Learning-Based Compositional Verification for Synchronous Probabilistic Systems. 511-521
  
• E. Allen Emerson, Roopsha Samanta:
  An Algorithmic Framework for Synthesis of Concurrent Programs. 522-530
  

Last update Wed May 22 00:37:51 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page