06596nam 22007815 450 99646577280331620200705221920.03-540-36577-X10.1007/3-540-36577-X(CKB)1000000000211949(SSID)ssj0000327273(PQKBManifestationID)11232918(PQKBTitleCode)TC0000327273(PQKBWorkID)10301415(PQKB)10108850(DE-He213)978-3-540-36577-8(MiAaPQ)EBC3073356(PPN)155189832(EXLCZ)99100000000021194920121227d2003 u| 0engurnn|008mamaatxtccrTools and Algorithms for the Construction and Analysis of Systems[electronic resource] 9th 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 /edited by Hubert Garavel, John Hatcliff1st ed. 2003.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2003.1 online resource (XVI, 604 p.) Lecture Notes in Computer Science,0302-9743 ;2619Bibliographic Level Mode of Issuance: Monograph3-540-00898-5 Includes bibliographical references at the end of each chapters and index.Invited 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.Lecture Notes in Computer Science,0302-9743 ;2619ComputersSoftware engineeringComputer logicComputer communication systemsAlgorithmsTheory of Computationhttps://scigraph.springernature.com/ontologies/product-market-codes/I16005Software Engineering/Programming and Operating Systemshttps://scigraph.springernature.com/ontologies/product-market-codes/I14002Logics and Meanings of Programshttps://scigraph.springernature.com/ontologies/product-market-codes/I1603XComputer Communication Networkshttps://scigraph.springernature.com/ontologies/product-market-codes/I13022Software Engineeringhttps://scigraph.springernature.com/ontologies/product-market-codes/I14029Algorithm Analysis and Problem Complexityhttps://scigraph.springernature.com/ontologies/product-market-codes/I16021Computers.Software engineering.Computer logic.Computer communication systems.Algorithms.Theory of Computation.Software Engineering/Programming and Operating Systems.Logics and Meanings of Programs.Computer Communication Networks.Software Engineering.Algorithm Analysis and Problem Complexity.005.1Garavel Hubertedthttp://id.loc.gov/vocabulary/relators/edtHatcliff Johnedthttp://id.loc.gov/vocabulary/relators/edtTACAS 2003MiAaPQMiAaPQMiAaPQBOOK996465772803316Tools and Algorithms for the Construction and Analysis of Systems772021UNISA