![](https://dblp1.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp1.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp1.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
default search action
9th ATVA 2011: Taipei, Taiwan
- Tevfik Bultan, Pao-Ann Hsiung:
Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings. Lecture Notes in Computer Science 6996, Springer 2011, ISBN 978-3-642-24371-4
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 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 C. 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 A. 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 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
![](https://dblp1.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.