LEADER 06119nam 22007095 450 001 996464498503316 005 20230222130704.0 010 $a3-030-81685-0 024 7 $a10.1007/978-3-030-81685-8 035 $a(CKB)5470000000830883 035 $aEBL6679367 035 $a(AU-PeEL)EBL6679367 035 $a(oapen)https://directory.doabooks.org/handle/20.500.12854/71643 035 $a(DE-He213)978-3-030-81685-8 035 $a(PPN)257359001 035 $a(EXLCZ)995470000000830883 100 $a20210717d2021 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 I /$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 (939 p.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v12759 300 $aDescription based upon print version of record. 311 $a3-030-81684-2 327 $aInvited Papers -- NNrepair: Constraint-based Repair of Neural Network Classifiers -- Balancing automation and control for formal verification of microprocessors -- Algebraic Program Analysis -- Programmable Program Synthesis -- Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities -- AI Verification -- DNNV: A Framework for Deep Neural Network Verification -- Robustness Verification of Quantum Classifiers -- BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks -- Automated Safety Verification of Programs Invoking Neural Networks -- Scalable Polyhedral Verification of Recurrent Neural Networks -- Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning -- Robustness Verification of Semantic Segmentation Neural Networks using Relaxed Reachability -- PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier -- Concurrency and Blockchain -- Isla: Integrating full-scale ISA semantics and axiomatic concurrency models -- Summing Up Smart Transitions -- Stateless Model Checking under a Reads-Value-From Equivalence -- Gobra: Modular Specification and Verification of Go Programs -- Delay-Bounded Scheduling Without Delay! -- Checking Data-Race Freedom of GPU Kernels, Compositionally -- GenMC: A Model Checker for Weak Memory Models -- Hybrid and Cyber-Physical Systems -- Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming -- An Iterative Scheme of Safe Reinforcement Learning for Nonlinear Systems via Barrier Certificate Generation -- HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL -- Computing Bottom SCCs Symbolically Using Transition Guided Reduction -- Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems -- IMITATOR 3: Synthesis of timing parameters beyond decidability -- Formally Verified Switching Logic for Recoverability of Aircraft Controller -- SceneChecker: Boosting Scenario Verification using Symmetry Abstractions -- Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness -- Fast zone-based algorithms for reachability in pushdown timed automata -- Security -- Verified Cryptographic Code for Everybody -- Not All Bugs Are Created Equal, But Robust Reachability Can Tell The Difference -- A Temporal Logic for Asynchronous Hyperproperties -- Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security -- Constraint-based Relational Verification -- Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning -- Synthesis -- Synthesis with Asymptotic Resource Bounds -- Program Sketching by Automatically Generating Mocks from Tests -- Counterexample-Guided Partial Bounding for Recursive Function Synthesis -- PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs -- Adapting Behaviors via Reactive Synthesis -- Causality-based Game Solving. 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. This is an open access book. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v12759 606 $aSoftware engineering 606 $aArtificial intelligence 606 $aComputer science 606 $aMachine theory 606 $aComputer simulation 606 $aSoftware Engineering 606 $aArtificial Intelligence 606 $aComputer Science Logic and Foundations of Programming 606 $aFormal Languages and Automata Theory 606 $aComputer Modelling 615 0$aSoftware engineering. 615 0$aArtificial intelligence. 615 0$aComputer science. 615 0$aMachine theory. 615 0$aComputer simulation. 615 14$aSoftware Engineering. 615 24$aArtificial Intelligence. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aFormal Languages and Automata Theory. 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 $a996464498503316 996 $aComputer Aided Verification$92870326 997 $aUNISA