LEADER 06571nam 22007815 450 001 9910143888703321 005 20200705221920.0 010 $a3-540-36577-X 024 7 $a10.1007/3-540-36577-X 035 $a(CKB)1000000000211949 035 $a(SSID)ssj0000327273 035 $a(PQKBManifestationID)11232918 035 $a(PQKBTitleCode)TC0000327273 035 $a(PQKBWorkID)10301415 035 $a(PQKB)10108850 035 $a(DE-He213)978-3-540-36577-8 035 $a(MiAaPQ)EBC3073356 035 $a(PPN)155189832 035 $a(EXLCZ)991000000000211949 100 $a20121227d2003 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTools and Algorithms for the Construction and Analysis of Systems $e9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings /$fedited by Hubert Garavel, John Hatcliff 205 $a1st ed. 2003. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2003. 215 $a1 online resource (XVI, 604 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v2619 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-00898-5 320 $aIncludes bibliographical references at the end of each chapters and index. 327 $aInvited Contributions -- What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code -- Bounded Model Checking and SAT-Based Methods -- Automatic Abstraction without Counterexamples -- Bounded Model Checking for Past LTL -- Experimental Analysis of Different Techniques for Bounded Model Checking -- Mu-Calculus and Temporal Logics -- On the Universal and Existential Fragments of the ?-Calculus -- Resets vs. Aborts in Linear Temporal Logic -- A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems -- Verification of Parameterized Systems -- Decidability of Invariant Validation for Paramaterized Systems -- Verification and Improvement of the Sliding Window Protocol -- Simple Representative Instantiations for Multicast Protocols -- Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols -- Abstractions and Counter-Examples -- Proof-Like Counter-Examples -- Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation -- Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement -- Counter-Example Guided Predicate Abstraction of Hybrid Systems -- Real-Time and Scheduling -- Schedulability Analysis Using Two Clocks -- On Optimal Scheduling under Uncertainty -- Static Guard Analysis in Timed Automata Verification -- Moby/DC ? A Tool for Model-Checking Parametric Real-Time Specifications -- ?erics: A Tool for Verifying Timed Automata and Estelle Specifications -- Security and Cryptography -- A New Knowledge Representation Strategy for Cryptographic Protocol Analysis -- Pattern-Based Abstraction for Verifying Secrecy in Protocols -- Modules and Compositional Verification -- Compositional Analysis for Verification of Parameterized Systems -- Learning Assumptions for Compositional Verification -- Automated Module Composition -- Modular Strategies for Recursive Game Graphs -- Symbolic State Spaces and Decision Diagrams -- Saturation Unbound -- Construction of Efficient BDDs for Bounded Arithmetic Constraints -- Performance and Mobility -- Modeling and Analysis of Power-Aware Systems -- A Set of Performance and Dependability Analysis Components for CADP -- The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems -- Banana - A Tool for Boundary Ambients Nesting ANAlysis -- State Space Reductions -- State Class Constructions for Branching Analysis of Time Petri Nets -- Branching Processes of High-Level Petri Nets -- Using Petri Net Invariants in State Space Construction -- Optimistic Synchronization-Based State-Space Reduction -- Constraint-Solving and Decision Procedures -- Checking Properties of Heap-Manipulating Procedures with a Constraint Solver -- An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic -- Strategies for Combining Decision Procedures -- Testing and Verification -- Generalized Symbolic Execution for Model Checking and Testing -- Code-Based Test Generation for Validation of Functional Processor Descriptions -- Large State Space Visualization -- Automatic Test Generation with AGATHA -- LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v2619 606 $aComputers 606 $aSoftware engineering 606 $aComputer logic 606 $aComputer communication systems 606 $aAlgorithms 606 $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aComputer Communication Networks$3https://scigraph.springernature.com/ontologies/product-market-codes/I13022 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aAlgorithm Analysis and Problem Complexity$3https://scigraph.springernature.com/ontologies/product-market-codes/I16021 615 0$aComputers. 615 0$aSoftware engineering. 615 0$aComputer logic. 615 0$aComputer communication systems. 615 0$aAlgorithms. 615 14$aTheory of Computation. 615 24$aSoftware Engineering/Programming and Operating Systems. 615 24$aLogics and Meanings of Programs. 615 24$aComputer Communication Networks. 615 24$aSoftware Engineering. 615 24$aAlgorithm Analysis and Problem Complexity. 676 $a005.1 702 $aGaravel$b Hubert$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aHatcliff$b John$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aTACAS 2003 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910143888703321 996 $aTools and Algorithms for the Construction and Analysis of Systems$9772021 997 $aUNINA