Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, ProceedingsDoron A. Peled, Yih-Kuen Tsay Springer Science & Business Media, 19 בספט׳ 2005 - 508 עמודים The Automated Technology for Veri?cation and Analysis (ATVA) international symposium series was initiated in 2003, responding to a growing interest in formal veri?cation spurred by the booming IT industry, particularly hardware design and manufacturing in East Asia. Its purpose is to promote research on automated veri?cation and analysis in the region by providing a forum for int- action between the regional and the international research/industrial commu- ties of the ?eld. ATVA 2005, the third of the ATVA series, was held in Taipei, Taiwan, October 4–7, 2005. The main theme of the symposium encompasses - sign, complexities, tools, and applications of automated methods for veri?cation and analysis. The symposium was co-located and had a two-day overlap with FORTE 2005, which was held October 2–5, 2005. We received a total of 95 submissions from 17 countries. Each submission was assigned to three Program Committee members, who were helped by their subreviewers, for rigorous and fair evaluation. The ?nal deliberation by the P- gram Committee was conducted over email for a duration of about 10 days after nearly all review reports had been collected. In the end, 33 papers were - lectedforinclusionintheprogram.ATVA2005hadthreekeynotespeechesgiven respectively by Amir Pnueli (joint with FORTE 2005), Zohar Manna, and Wo- gang Thomas. The main symposium was preceded by a tutorial day, consisting of three two-hour lectures given also by the keynote speakers. |
תוכן
Ranking Abstraction as a Companion to Predicate Abstraction | 1 |
A New Reachability Algorithm for Symmetric Multiprocessor | 26 |
Comprehensive Verification Framework for Dependability | 39 |
Exploiting Hub States in Automatic Verification | 54 |
Combined Methods | 69 |
DecompositionBased Verification of Cyclic Workflows | 84 |
Timed Embedded and Hybrid Systems | 99 |
Computation Platform for Automatic Analysis of Embedded Software | 114 |
Established Formalisms and Standards | 278 |
Comparison of Different Semantics for Time Petri Nets | 293 |
Introducing Dynamic Properties with Past Temporal Operators in | 308 |
Approximate Reachability for Dead Code Elimination in Esterel | 323 |
Compositional Verification and Games | 338 |
Multivalued Model Checking Games | 354 |
Timed Embedded and Hybrid Systems II | 370 |
An MTBDDBased Implementation of Forward Reachability | 385 |
Quantitative and Qualitative Analysis of Temporal Aspects of Complex | 129 |
Automatic Test Case Generation with RegionRelated Coverage | 144 |
Abstraction and Reduction Techniques | 159 |
Predicate Abstraction of RTL Verilog Descriptions Using Constraint | 174 |
State Space Exploration of ObjectBased Systems Using Equivalence | 187 |
Syntactical Colored Petri Nets Reductions | 202 |
Decidability and Complexity | 217 |
A Static Analysis Using Tree Automata for XML Access Control | 234 |
Reasoning About Transfinite Sequences | 248 |
Semiautomatic Distributed Synthesis | 263 |
Protocols Analysis Case Studies and Tools | 400 |
Modeling and Verification of a Telecommunication Application Using | 414 |
A Case | 429 |
Model Checking Real Time Java Using Java PathFinder | 444 |
InfiniteState and Parameterized Systems | 457 |
Flat Acceleration in Symbolic Model Checking | 474 |
488 | |
Author Index | 505 |
מהדורות אחרות - הצג הכל
מונחים וביטויים נפוצים
abstraction actions algorithm allows analysis application approach assigned automata automaton block bounded called clock complexity components Computer consider constraints construction corresponding counter defined Definition denote different discrete distributed enabled equivalent event example execution exists expression extended finite firing first formal formula function given global graph hybrid implementation initial input International labeled language LNCS logic machine mapping method model checking node Note obtained operations output parallel partition path perform Petri nets play possible present problem proof properties proposed protocol prove provides reachability reached reduced relation represented respectively rule Science semantics sequence simulation space specification step strategy structure symbolic Table techniques temporal termination Theorem tion tool transition tree variables verification verify zone