default search action
3rd ATVA 2005: Taipei, Taiwan
- Doron A. Peled, Yih-Kuen Tsay:
Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings. Lecture Notes in Computer Science 3707, Springer 2005, ISBN 3-540-29209-8
Keynote Speeches
- Amir Pnueli:
Ranking Abstraction as a Companion to Predicate Abstraction, . 1 - Aaron R. Bradley, Zohar Manna:
Termination and Invariance Analysis of Loops. 2 - Wolfgang Thomas:
Some Perspectives of Infinite-State Verification. 3-10
Model Checking
- Limor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, Assaf Schuster:
Verifying Very Large Industrial Circuits Using 100 Processes and Beyond. 11-25 - Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill:
A New Reachability Algorithm for Symmetric Multi-processor Architecture. 26-38 - Yuhong Zhao, Martin Kardos, Simon Oberthür, Franz J. Rammig:
Comprehensive Verification Framework for Dependability of Self-optimizing Systems. 39-53 - Giuseppe Della Penna, Igor Melatti, Benedetto Intrigila, Enrico Tronci:
Exploiting Hub States in Automatic Verification. 54-68
Combined Methods
- Ali Habibi, Sofiène Tahar:
An Approach for the Verification of SystemC Designs Using AsmL. 69-83 - Yongsun Choi, J. Leon Zhao:
Decomposition-Based Verification of Cyclic Workflows. 84-98
Timed, Embedded, and Hybrid Systems (I)
- Werner Damm, Guilherme Pinto, Stefan Ratschan:
Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems. 99-113 - Abhishek Dubey
, Xianbin Wu, Hang Su, Tak-John Koo:
Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach. 114-128 - Andrei Voinikonis:
Quantitative and Qualitative Analysis of Temporal Aspects of Complex Activities. 129-143 - Geng-Dian Huang, Farn Wang:
Automatic Test Case Generation with Region-Related Coverage Annotations for Real-Time Systems. 144-158
Abstraction and Reduction Techniques
- Maciej Szreter:
Selective Search in Bounded Model Checking of Reachability Properties. 159-173 - Tun Li, Yang Guo, Sikun Li, GongJie Liu:
Predicate Abstraction of RTL Verilog Descriptions Using Constraint Logic Programming. 174-186 - Charles A. Lakos, Lars Michael Kristensen:
State Space Exploration of Object-Based Systems Using Equivalence Reduction and the Sweepline Method. 187-201 - Sami Evangelista, Serge Haddad, Jean-François Pradat-Peyre:
Syntactical Colored Petri Nets Reductions. 202-216
Decidability and Complexity
- Venkatesh Mysore, Carla Piazza
Algorithmic Algebraic Model Checking II: Decidability of Semi-algebraic Model Checking and Its Applications to Systems Biology. 217-233 - Isao Yagi
A Static Analysis Using Tree Automata for XML Access Control. 234-247 - Stéphane Demri, David Nowak:
Reasoning About Transfinite Sequences. 248-262 - Bernd Finkbeiner, Sven Schewe
Semi-automatic Distributed Synthesis. 263-277
Established Formalisms and Standards
- Xiaoyu Mao, Janette Cardoso
A New Graph of Classes for the Preservation of Quantitative Temporal Constraints. 278-292 - Béatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, Olivier H. Roux:
Comparison of Different Semantics for Time Petri Nets. 293-307 - Mouna Saad, Leila Jemni Ben Ayed:
Introducing Dynamic Properties with Past Temporal Operators in the B Refinement. 308-322 - Olivier Tardieu, Stephen A. Edwards
Approximate Reachability for Dead Code Elimination in Esterel. 323-337
Compositional Verification and Games
- Purandar Bhaduri
Synthesis of Interface Automata. 338-353 - Sharon Shoham
Multi-valued Model Checking Games. 354-369
Timed, Embedded, and Hybrid Systems (II)
- Shang-Wei Lin
Model Checking Prioritized Timed Automata. 370-384 - Fuzhi Wang, Marta Z. Kwiatkowska:
An MTBDD-Based Implementation of Forward Reachability for Probabilistic Timed Automata. 385-399
Protocols Analysis, Case Studies, and Tools
- Jean-Marie Orset, Baptiste Alcalde, Ana R. Cavalli:
An EFSM-Based Intrusion Detection System for Ad Hoc Networks. 400-413 - Pierre Combes, David Harel, Hillel Kugler
Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-Engine Tool. 414-428 - Moonzoo Kim, Kyo Chul Kang:
Formal Construction and Verification of Home Service Robots: A Case Study. 429-443 - Gary Lindstrom, Peter C. Mehlitz, Willem Visser:
Model Checking Real Time Java Using Java PathFinder. 444-456
Infinite-State and Parameterized Systems
- Guy Edward Gallasch, Jonathan Billington:
Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols. 457-473 - Sébastien Bardin, Alain Finkel, Jérôme Leroux, Philippe Schnoebelen:
Flat Acceleration in Symbolic Model Checking. 474-488 - Jérôme Leroux, Grégoire Sutre:
Flat Counter Automata Almost Everywhere! 489-503
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.
last updated on 2025-03-10 20:31 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: