LEADER 06752nam 22006855 450 001 996199992703316 005 20230329210500.0 010 $a3-319-08867-X 024 7 $a10.1007/978-3-319-08867-9 035 $a(CKB)3710000000143900 035 $a(SSID)ssj0001275068 035 $a(PQKBManifestationID)11810317 035 $a(PQKBTitleCode)TC0001275068 035 $a(PQKBWorkID)11337453 035 $a(PQKB)10551027 035 $a(DE-He213)978-3-319-08867-9 035 $a(MiAaPQ)EBC3093389 035 $a(PPN)17976666X 035 $a(EXLCZ)993710000000143900 100 $a20140628d2014 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aComputer Aided Verification$b[electronic resource] $e26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, Proceedings /$fedited by Armin Biere, Roderick Bloem 205 $a1st ed. 2014. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2014. 215 $a1 online resource (XXXIV, 877 p. 205 illus.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v8559 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-319-08866-1 327 $aSoftware Verification -- The Spirit of Ghost Code -- SMT-Based Model Checking for Recursive Programs -- Property-Directed Shape Analysis -- Shape Analysis via Second-Order Bi-Abduction -- ICE: A Robust Framework for Learning Invariants -- From Invariant Checking to Invariant Inference Using Randomized Search -- SMACK: Decoupling Source Language Details from Verifier Implementations -- Security -- Synthesis of Masking Countermeasures against Side Channel Attacks -- Temporal Mode-Checking for Runtime Monitoring of Privacy Policies -- String Constraints for Verification -- A Conference Management System with Verified Document Confidentiality -- VAC - Verifier of Administrative Role-Based Access Control Policies -- Automata -- From LTL to Deterministic Automata: A Safraless Compositional Approach -- Symbolic Visibly Pushdown Automata -- Model Checking and Testing -- Engineering a Static Verification Tool for GPU Kernels -- Lazy Annotation Revisited -- Interpolating Property Directed Reachability -- Verifying Relative Error Bounds Using Symbolic Simulation -- Regression Test Selection for Distributed Software Histories -- GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components -- Software Verification in the Google App-Engine Cloud -- The nuXmv Symbolic Model Checker -- Biology and Hybrid Systems Analyzing and Synthesizing Genomic Logic Functions -- Finding Instability in Biological Models -- Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells -- Diamonds Are a Girl?s Best Friend: Partial Order Reduction for Timed Automata with Abstractions -- Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections -- Verifying LTL Properties of Hybrid Systems with K-Liveness -- Games and Synthesis -- Safraless Synthesis for Epistemic Temporal Specifications -- Minimizing Running Costs in Consumption Systems -- CEGAR for Qualitative Analysis of Probabilistic Systems -- Optimal Guard Synthesis for Memory Safety -- Don?t Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion -- MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications -- Solving Games without Controllable Predecessor -- G4LTL-ST: Automatic Generation of PLC Programs -- Concurrency -- Automatic Atomicity Verification for Clients of Concurrent Data Structures -- Regression-Free Synthesis for Concurrency -- Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization -- An SMT-Based Approach to Coverability Analysis -- LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes -- SMT and Theorem Proving -- Monadic Decomposition -- A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions -- Bit-Vector Rewriting with Automatic Rule Generation -- A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors -- AVATAR: The Architecture for First-Order Theorem Provers -- Automating Separation Logic with Trees and Data -- A Nonlinear Real Arithmetic Fragment -- Yices 2.2 -- Bounds and Termination -- A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis -- Symbolic Resource Bound Inference for Functional Programs -- Proving Non-termination Using Max-SMT -- Termination Analysis by Learning Terminating Programs -- Causal Termination of Multi-threaded Programs -- Abstraction -- Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) -- Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction -- QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers. 330 $aThis book constitutes the proceedings of the 26th International Conference on Computer Aided Verification, CAV 2014, held as part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 46 regular papers and 11 short papers presented in this volume were carefully reviewed and selected from a total of 175 regular and 54 short paper submissions. The contributions are organized in topical sections named: software verification; automata; model checking and testing; biology and hybrid systems; games and synthesis; concurrency; SMT and theorem proving; bounds and termination; and abstraction. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v8559 606 $aComputer science 606 $aSoftware engineering 606 $aMachine theory 606 $aComputer engineering 606 $aComputer networks 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 606 $aFormal Languages and Automata Theory 606 $aComputer Engineering and Networks 615 0$aComputer science. 615 0$aSoftware engineering. 615 0$aMachine theory. 615 0$aComputer engineering. 615 0$aComputer networks. 615 14$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 615 24$aFormal Languages and Automata Theory. 615 24$aComputer Engineering and Networks. 676 $a005.1015113 702 $aBiere$b Armin$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aBloem$b Roderick$4edt$4http://id.loc.gov/vocabulary/relators/edt 906 $aBOOK 912 $a996199992703316 996 $aComputer Aided Verification$9772228 997 $aUNISA