LEADER 05965nam 22007095 450 001 996464499103316 005 20230330055754.0 010 $a3-030-81688-5 024 7 $a10.1007/978-3-030-81688-9 035 $a(CKB)5470000000830882 035 $aEBL6679368 035 $a(AU-PeEL)EBL6679368 035 $a(oapen)https://directory.doabooks.org/handle/20.500.12854/71644 035 $a(DE-He213)978-3-030-81688-9 035 $a(PPN)25735901X 035 $a(EXLCZ)995470000000830882 100 $a20210716d2021 u| 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aComputer Aided Verification$b[electronic resource] $e33rd International Conference, CAV 2021, Virtual Event, July 20?23, 2021, Proceedings, Part II /$fedited by Alexandra Silva, K. Rustan M. Leino 205 $a1st ed. 2021. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2021. 215 $a1 online resource (955 p.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v12760 300 $aDescription based upon print version of record. 311 $a3-030-81687-7 327 $aComplexity and Termination -- Learning Probabilistic Termination Proofs -- Ghost Signals: Verifying Termination of Busy Waiting -- Reflections on Termination of Linear Loops -- Decision Tree Learning in CEGIS-Based Termination Analysis -- ATLAS: Automated Amortised Complexity Analysis of Self-Adjusting Data Structures -- Decision Procedures and Solvers -- Theory Exploration Powered by Deductive Synthesis -- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver -- Porous Invariants -- JavaSMT 3: Interacting with SMT Solvers in Java -- Efficient SMT-based Analysis of Failure Propagation -- ToolX : Better Delta Debugging for the SMT-LIBv2 Language and Friends -- Learning Union of Integer Hypercubes with Queries (with applications to monadic decomposition) -- Interpolation and Model Checking for Nonlinear Arithmetic -- An SMT Solver for Regular Expressions and Linear Arithmetic over String Length -- Counting Minimal Unsatisfiable Subsets -- Sound Verification Procedures for Temporal Properties of Infinite-State Systems -- Hardware and Model Checking -- Progress in Certifying Hardware Model Checking Results -- Model-Checking Structured Context-Free Languages -- Model Checking ! -Regular Properties with Decoupled Search -- AIGEN: Random Generation of Symbolic Transition Systems -- GPU Acceleration of Bounded Model Checking with ParaFROST -- Pono: A Flexible and Extensible SMT-based Model Checker -- Logical Foundations -- Towards a Trustworthy Semantics-Based Language Framework via Proof Generation -- Formal Foundations of Fine-Grained Explainability -- Latticed k-Induction with an Application to Probabilistic Programs -- Stochastic Systems -- Runtime Monitors for Markov Decision Processes -- Model Checking Finite-Horizon Markov Chains with Probabilistic Inference -- Enforcing Almost-Sure Reachability in POMDPs -- Rigorous Floating-Point Roundo Error Analysis of Probabilistic Computations -- Model-free Reinforcement Learning for Branching Markov Decision Processes -- Software Verification -- Cameleer: a Deductive Verification Tool for OCaml -- LLMC: Verifying High-Performance Software -- Formally Validating a Practical Verification Condition Generator -- Automatic Generation and Validation of Instruction Encoders and Decoders -- An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation -- Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios -- Functional Correctness of C implementations of Dijkstra's, Kruskal's, and Prim's Algorithms -- Gillian, Part II: Real-World Verification for JavaScript and C -- Debugging Network Reachability with Blocked Paths -- Lower-Bound Synthesis using Loop Specialization and Max-SMT -- Fast Computation of Strong Control Dependencies -- Di y: Inductive Reasoning of Array Programs using Difference Invariants. 330 $aThis open access two-volume set LNCS 12759 and 12760 constitutes the refereed proceedings of the 33rd International Conference on Computer Aided Verification, CAV 2021, held virtually in July 2021. The 63 full papers presented together with 16 tool papers and 5 invited papers were carefully reviewed and selected from 290 submissions. The papers were organized in the following topical sections: Part I: invited papers; AI verification; concurrency and blockchain; hybrid and cyber-physical systems; security; and synthesis. Part II: complexity and termination; decision procedures and solvers; hardware and model checking; logical foundations; and software verification. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v12760 606 $aSoftware engineering 606 $aMachine theory 606 $aArtificial intelligence 606 $aComputer science 606 $aComputer simulation 606 $aSoftware Engineering 606 $aFormal Languages and Automata Theory 606 $aArtificial Intelligence 606 $aComputer Science Logic and Foundations of Programming 606 $aComputer Modelling 615 0$aSoftware engineering. 615 0$aMachine theory. 615 0$aArtificial intelligence. 615 0$aComputer science. 615 0$aComputer simulation. 615 14$aSoftware Engineering. 615 24$aFormal Languages and Automata Theory. 615 24$aArtificial Intelligence. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aComputer Modelling. 676 $a005.1 700 $aSilva$b Alexandra$0943824 701 $aLeino$b K. Rustan M$01235981 801 0$bAU-PeEL 801 1$bAU-PeEL 801 2$bAU-PeEL 906 $aBOOK 912 $a996464499103316 996 $aComputer Aided Verification$92870326 997 $aUNISA