LEADER 06771nam 22007695 450 001 996465474403316 005 20230221051904.0 010 $a1-280-95188-5 010 $a9786610951888 010 $a3-540-71209-7 024 7 $a10.1007/978-3-540-71209-1 035 $a(CKB)1000000000491039 035 $a(EBL)3061573 035 $a(SSID)ssj0000311642 035 $a(PQKBManifestationID)11214277 035 $a(PQKBTitleCode)TC0000311642 035 $a(PQKBWorkID)10328654 035 $a(PQKB)10699869 035 $a(DE-He213)978-3-540-71209-1 035 $a(MiAaPQ)EBC3061573 035 $a(MiAaPQ)EBC6708623 035 $a(Au-PeEL)EBL6708623 035 $a(PPN)123726891 035 $a(EXLCZ)991000000000491039 100 $a20100301d2007 u| 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt 182 $cc 183 $acr 200 10$aTools and Algorithms for the Construction and Analysis of Systems$b[electronic resource] $e13th International Conference, TACAS 2007 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007 Proceedings /$fedited by Orna Grumberg, Michael Huth 205 $a1st ed. 2007. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2007. 215 $a1 online resource (755 p.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4424 300 $a"... the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007)"--Pref. 311 $a3-540-71208-9 320 $aIncludes bibliographical references and index. 327 $aInvited Contributions -- THERE AND BACK AGAIN: Lessons Learned on the Way to the Market -- Verifying Object-Oriented Software: Lessons and Challenges -- Software Verification -- Shape Analysis by Graph Decomposition -- A Reachability Predicate for Analyzing Low-Level Software -- Generating Representation Invariants of Structurally Complex Data -- Probabilistic Model Checking and Markov Chains -- Multi-objective Model Checking of Markov Decision Processes -- PReMo: An Analyzer for Probabilistic Recursive Models -- Counterexamples in Probabilistic Model Checking -- Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking -- Static Analysis -- Causal Dataflow Analysis for Concurrent Programs -- Type-Dependence Analysis and Program Transformation for Symbolic Execution -- JPF?SE: A Symbolic Execution Extension to Java PathFinder -- Markov Chains and Real-Time Systems -- A Symbolic Algorithm for Optimal Markov Chain Lumping -- Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations -- Model Checking Probabilistic Timed Automata with One or Two Clocks -- Adaptor Synthesis for Real-Time Components -- Timed Automata and Duration Calculus -- Deciding an Interval Logic with Accumulated Durations -- From Time Petri Nets to Timed Automata: An Untimed Approach -- Complexity in Simplicity: Flexible Agent-Based State Space Exploration -- On Sampling Abstraction of Continuous Time Logic with Durations -- Assume-Guarantee Reasoning -- Assume-Guarantee Synthesis -- Optimized L*-Based Assume-Guarantee Reasoning -- Refining Interface Alphabets for Compositional Verification -- MAVEN: Modular Aspect Verification -- Biological Systems -- Model Checking Liveness Properties of Genetic Regulatory Networks -- Checking Pedigree Consistency with PCS -- ?Don?t Care? Modeling: A Logical Framework for Developing Predictive System Models -- Abstraction Refinement -- Deciding Bit-Vector Arithmetic with Abstraction -- Abstraction Refinement of Linear Programs with Arrays -- Property-Driven Partitioning for Abstraction Refinement -- Combining Abstraction Refinement and SAT-Based Model Checking -- Message Sequence Charts -- Detecting Races in Ensembles of Message Sequence Charts -- Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by Learning -- Automata-Based Model Checking -- Improved Algorithms for the Automata-Based Approach to Model-Checking -- GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae -- Faster Algorithms for Finitary Games -- Specification Languages -- Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs, -- motor:The modest Tool Environment -- Syntactic Optimizations for PSL Verification -- The Heterogeneous Tool Set, Hets -- Security -- Searching for Shapes in Cryptographic Protocols -- Automatic Analysis of the Security of XOR-Based Key Management Schemes -- Software and Hardware Verification -- State of the Union: Type Inference Via Craig Interpolation -- Hoare Logic for Realistically Modelled Machine Code -- VCEGAR: Verilog CounterExample Guided Abstraction Refinement -- Decision Procedures and Theorem Provers -- Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications -- Combined Satisfiability Modulo Parametric Theories -- A Gröbner Basis Approach to CNF-Formulae Preprocessing -- Kodkod: A Relational Model Finder -- Model Checking -- Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams -- Model Checking on Trees with Path Equivalences -- Uppaal/DMC ? Abstraction-Based Heuristics for Directed Model Checking -- Distributed Analysis with ?CRL: A Compendium of Case Studies -- Infinite-State Systems -- A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes -- Unfolding Concurrent Well-Structured Transition Systems -- Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems). 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4424 606 $aSoftware engineering 606 $aComputer science 606 $aComputer networks 606 $aAlgorithms 606 $aSoftware Engineering 606 $aComputer Science Logic and Foundations of Programming 606 $aComputer Communication Networks 606 $aAlgorithms 615 0$aSoftware engineering. 615 0$aComputer science. 615 0$aComputer networks. 615 0$aAlgorithms. 615 14$aSoftware Engineering. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aComputer Communication Networks. 615 24$aAlgorithms. 676 $a004.21 702 $aGrumberg$b Orna 702 $aHuth$b Michael$f1962- 712 12$aETAPS 2007$f(2007 :$eBraga, Portugal) 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996465474403316 996 $aTools and Algorithms for the Construction and Analysis of Systems$9772021 997 $aUNISA