LEADER 06755nam 22006975 450 001 9910739423503321 005 20230329171747.0 010 $a3-642-36742-9 024 7 $a10.1007/978-3-642-36742-7 035 $a(CKB)3520000000003549 035 $a(SSID)ssj0000880079 035 $a(PQKBManifestationID)11546674 035 $a(PQKBTitleCode)TC0000880079 035 $a(PQKBWorkID)10872915 035 $a(PQKB)10035881 035 $a(DE-He213)978-3-642-36742-7 035 $a(MiAaPQ)EBC3092996 035 $a(PPN)168330393 035 $a(EXLCZ)993520000000003549 100 $a20130220d2013 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 $e19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Proceedings /$fedited by Nir Piterman, Scott Smolka 205 $a1st ed. 2013. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2013. 215 $a1 online resource (XXIV, 646 p. 137 illus.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v7795 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-642-36741-0 327 $aOn-the-Fly Exact Computation of Bisimilarity Distances -- The Quest for Minimal Quotients for Probabilistic Automata -- LTL Model Checking of Interval Markov Chains -- Ramsey vs. Lexicographic Termination Proving -- Structural Counter Abstraction -- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors -- The MathSAT5 SMT Solver -- Formula Preprocessing in MUS Extraction -- Proof Tree Preserving Interpolation -- Asynchronous Multi-core Incremental SAT Solving -- Model-Checking Iterated Games -- PRISM-games: A Model Checker for Stochastic Multi-Player Games -- PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus -- An Overview of the mCRL2 Toolset and Its Recent Advances -- Analysis of Boolean Programs -- Weighted Pushdown Systems with Indexed Weight Domains -- Underapproximation of Procedure Summaries for Integer Programs -- Runtime Verification Based on Register Automata -- Unbounded Model-Checking with Interpolation for Regular Language Constraints -- eVolCheck: Incremental Upgrade Checker for C -- Intertwined Forward-Backward Reachability Analysis Using Interpolants -- An Integrated Specification and Verification Technique or Highly Concurrent Data Structures -- A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems -- Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory -- Synthesis of Circular Compositional Program Proofs via Abduction -- As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty -- Integer Parameter Synthesis for Timed Automata -- LTL Model-Checking for Malware Detection -- Policy Analysis for Self-administrated Role-Based Access Control -- Model Checking Agent Knowledge in Dynamic Access Control Policies -- Frontiers (Graphics and Quantum) Automatic Testing of Real-Time Graphics Systems -- Equivalence Checking of Quantum Protocols -- Encoding Monomorphic and Polymorphic Types -- Deriving Probability Density Functions from Probabilistic Functional Programs -- Tool Demonstrations Polyglot: Systematic Analysis for Multiple Statechart Formalisms -- Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO -- BULL: A Library for Learning Algorithms of Boolean Functions -- AppGuard ? Enforcing User Requirements on Android Apps -- Model Checking Database Applications -- Efficient Property Preservation Checking of Model Refinements -- Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking -- Competition on Software Verification Second Competition on Software Verification (Summary of SV-COMP 2013) -- CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation (Competition Contribution) -- CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution) -- CSeq: A Sequentialization Tool for C (Competition Contribution) -- Handling Unbounded Loops with ESBMC 1.20 (Competition Contribution) -- LLBMC: Improved Bounded Model Checking of C Programs Using LLVM (Competition Contribution) -- Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution) -- Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution (Competition Contribution) -- Threader: A Verifier for Multi-threaded Programs (Competition Contribution) -- UFO: Verification with Interpolants and Abstract Interpretation (Competition Contribution) -- Ultimate Automizer with SMTInterpol (Competition Contribution). 330 $aThis book constitutes the proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, held in Rome, Italy, in March 2013. The 42 papers presented in this volume were carefully reviewed and selected from 172 submissions. They are organized in topical sections named: Markov chains; termination; SAT/SMT; games and synthesis; process algebra; pushdown; runtime verification and model checking; concurrency; learning and abduction; timed automata; security and access control; frontiers (graphics and quantum); functional programs and types; tool demonstrations; explicit-state model checking; Büchi automata; and competition on software verification. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v7795 606 $aComputer science 606 $aSoftware engineering 606 $aAlgorithms 606 $aCompilers (Computer programs) 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 606 $aAlgorithms 606 $aCompilers and Interpreters 615 0$aComputer science. 615 0$aSoftware engineering. 615 0$aAlgorithms. 615 0$aCompilers (Computer programs). 615 14$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 615 24$aAlgorithms. 615 24$aCompilers and Interpreters. 676 $a004.21 702 $aPiterman$b Nir$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSmolka$b Scott$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910739423503321 996 $aTools and Algorithms for the Construction and Analysis of Systems$9772021 997 $aUNINA