LEADER 07460nam 22007935 450 001 996465750603316 005 20200701023335.0 010 $a3-540-30476-2 024 7 $a10.1007/b102065 035 $a(CKB)1000000000212613 035 $a(DE-He213)978-3-540-30476-0 035 $a(SSID)ssj0000107944 035 $a(PQKBManifestationID)11128900 035 $a(PQKBTitleCode)TC0000107944 035 $a(PQKBWorkID)10013032 035 $a(PQKB)11534390 035 $a(MiAaPQ)EBC3088894 035 $a(PPN)155203312 035 $a(EXLCZ)991000000000212613 100 $a20121227d2004 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aAutomated Technology for Verification and Analysis$b[electronic resource] $eSecond International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31 - November 3, 2004. Proceedings /$fedited by Farn Wang 205 $a1st ed. 2004. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2004. 215 $a1 online resource (XII, 510 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v3299 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-23610-4 320 $aIncludes bibliographical references at the end of each chapters and index. 327 $aKeynote Speech -- Games for Formal Design and Verification of Reactive Systems -- Evolution of Model Checking into the EDA Industry -- Abstraction Refinement -- Invited Speech -- Tools for Automated Verification of Web Services -- Theorem Proving Languages for Verification -- An Automated Rigorous Review Method for Verifying and Validating Formal Specifications -- Papers -- Toward Unbounded Model Checking for Region Automata -- Search Space Partition and Case Basis Exploration for Reducing Model Checking Complexity -- Synthesising Attacks on Cryptographic Protocols -- Büchi Complementation Made Tighter -- SAT-Based Verification of Safe Petri Nets -- Disjunctive Invariants for Numerical Systems -- Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas -- Fair Testing Revisited: A Process-Algebraic Characterisation of Conflicts -- Exploiting Symmetries for Testing Equivalence in the Spi Calculus -- Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors -- Abstraction-Based Model Checking Using Heuristical Refinement -- A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata -- Design and Evaluation of a Symbolic and Abstraction-Based Model Checker -- Component-Wise Instruction-Cache Behavior Prediction -- Validating the Translation of an Industrial Optimizing Compiler -- Composition of Accelerations to Verify Infinite Heterogeneous Systems -- Hybrid System Verification Is Not a Sinecure -- Providing Automated Verification in HOL Using MDGs -- Specification, Abduction, and Proof -- Introducing Structural Dynamic Changes in Petri Nets: Marked-Controlled Reconfigurable Nets -- Typeness for ?-Regular Automata -- Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits -- Mutation Coverage Estimation for Model Checking -- Modular Model Checking of Software Specifications with Simultaneous Environment Generation -- Rabin Tree and Its Application to Group Key Distribution -- Using Overlay Networks to Improve VoIP Reliability -- Integrity-Enhanced Verification Scheme for Software-Intensive Organizations -- RCGES: Retargetable Code Generation for Embedded Systems -- Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets -- First-Order LTL Model Checking Using MDGs -- Localizing Errors in Counterexample with Iteratively Witness Searching -- Verification of WCDMA Protocols and Implementation -- Efficient Representation of Algebraic Expressions -- Development of RTOS for PLC Using Formal Methods -- Reducing Parametric Automata: A Multimedia Protocol Service Case Study -- Synthesis of State Feedback Controllers for Parameterized Discrete Event Systems -- Solving Box-Pushing Games via Model Checking with Optimizations -- CLP Based Static Property Checking -- A Temporal Assertion Extension to Verilog. 330 $aIt was our great pleasure to hold the 2nd International Symposium onAutomated Te- nology on Veri?cation and Analysis (ATVA) in Taipei, Taiwan, ROC, October 31? November3,2004.TheseriesofATVAmeetingsisintendedforthepromotionofrelated research in eastern Asia. In the last decade, automated technology on veri?cation has become the new strength in industry and brought forward various hot research activities in both Europe and USA. In comparison, easternAsia has been quiet in the forum.With more and more IC design houses moving from SiliconValley to easternAsia, we believe this is a good time to start cultivating related research activities in the region. TheemphasisoftheATVAworkshopseriesisonvariousmechanicalandinformative techniques, which can give engineers valuable feedback to fast converge their designs according to the speci?cations. The scope of interest contains the following research - eas: model-checking theory, theorem-proving theory, state-space reduction techniques, languages in automated veri?cation, parametric analysis, optimization, formal perf- mance analysis, real-time systems, embedded systems, in?nite-state systems, Petri nets, UML, synthesis, tools, and practice in industry. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v3299 606 $aComputer-aided engineering 606 $aComputer logic 606 $aComputers 606 $aComputer communication systems 606 $aSpecial purpose computers 606 $aSoftware engineering 606 $aComputer-Aided Engineering (CAD, CAE) and Design$3https://scigraph.springernature.com/ontologies/product-market-codes/I23044 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aInformation Systems and Communication Service$3https://scigraph.springernature.com/ontologies/product-market-codes/I18008 606 $aComputer Communication Networks$3https://scigraph.springernature.com/ontologies/product-market-codes/I13022 606 $aSpecial Purpose and Application-Based Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I13030 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 615 0$aComputer-aided engineering. 615 0$aComputer logic. 615 0$aComputers. 615 0$aComputer communication systems. 615 0$aSpecial purpose computers. 615 0$aSoftware engineering. 615 14$aComputer-Aided Engineering (CAD, CAE) and Design. 615 24$aLogics and Meanings of Programs. 615 24$aInformation Systems and Communication Service. 615 24$aComputer Communication Networks. 615 24$aSpecial Purpose and Application-Based Systems. 615 24$aSoftware Engineering. 676 $a004.015113 702 $aWang$b Farn$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996465750603316 996 $aAutomated Technology for Verification and Analysis$9772478 997 $aUNISA