001431102 000__ 05951cam\a2200637\i\4500
001431102 001__ 1431102
001431102 003__ OCoLC
001431102 005__ 20230308003221.0
001431102 006__ m\\\\\o\\d\\\\\\\\
001431102 007__ cr\cn\nnnunnun
001431102 008__ 210728s2021\\\\sz\a\\\\ob\\\\101\0\eng\d
001431102 019__ $$a1266809737
001431102 020__ $$a9783030816889$$q(electronic bk.)
001431102 020__ $$a3030816885$$q(electronic bk.)
001431102 020__ $$z9783030816872
001431102 0247_ $$a10.1007/978-3-030-81688-9$$2doi
001431102 035__ $$aSP(OCoLC)1261897041
001431102 040__ $$aGW5XE$$beng$$erda$$epn$$cGW5XE$$dOCLCO$$dYDX$$dDCT$$dOCLCF$$dOCLCQ$$dEBLCP$$dOCLCQ
001431102 049__ $$aISEA
001431102 050_4 $$aQA76.76.V47$$bC38 2021
001431102 08204 $$a005.1/4$$223
001431102 1112_ $$aCAV (Conference)$$n(33rd :$$d2021 :$$cOnline)
001431102 24510 $$aComputer aided verification :$$b33rd international conference, CAV 2021, virtual event, July 20-23, 2021 : proceedings.$$nPart II /$$cAlexandra Silva, K. Rustan M. Leino (eds.).
001431102 24630 $$aCAV 2021
001431102 264_1 $$aCham :$$bSpringer,$$c[2021]
001431102 264_4 $$c©2021
001431102 300__ $$a1 online resource (xxiii, 940 pages) :$$billustrations (some color)
001431102 336__ $$atext$$btxt$$2rdacontent
001431102 337__ $$acomputer$$bc$$2rdamedia
001431102 338__ $$aonline resource$$bcr$$2rdacarrier
001431102 347__ $$atext file
001431102 347__ $$bPDF
001431102 4901_ $$aLecture notes in computer science ;$$v12760
001431102 4901_ $$aLNCS sublibrary: SL1 - Theoretical computer science and general issues
001431102 500__ $$aInternational conference proceedings.
001431102 504__ $$aIncludes bibliographical references and author index.
001431102 5050_ $$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.
001431102 5060_ $$aOpen access$$5GW5XE
001431102 520__ $$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.
001431102 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed July 28, 2021).
001431102 650_0 $$aComputer software$$xVerification$$vCongresses.
001431102 655_7 $$aConference papers and proceedings.$$2fast$$0(OCoLC)fst01423772
001431102 655_7 $$aConference papers and proceedings.$$2lcgft
001431102 655_0 $$aElectronic books.
001431102 7001_ $$aSilva, Alexandra$$q(Alexandra Martins da),$$eeditor.
001431102 7001_ $$aLeino, K. Rustan M.,$$eeditor.
001431102 77608 $$iPrint version: $$z9783030816872
001431102 77608 $$iPrint version: $$z9783030816896
001431102 830_0 $$aLecture notes in computer science ;$$v12760.
001431102 830_0 $$aLNCS sublibrary.$$nSL 1,$$pTheoretical computer science and general issues.
001431102 852__ $$bebk
001431102 85640 $$3Springer Nature$$uhttps://link.springer.com/10.1007/978-3-030-81688-9$$zOnline Access$$91397441.2
001431102 909CO $$ooai:library.usi.edu:1431102$$pGLOBAL_SET
001431102 980__ $$aBIB
001431102 980__ $$aEBOOK
001431102 982__ $$aEbook
001431102 983__ $$aOnline
001431102 994__ $$a92$$bISE