Computer Aided Verification (Record no. 53434)

000 -LEADER
fixed length control field 06369nam a22005895i 4500
001 - CONTROL NUMBER
control field 978-3-319-08867-9
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20200421111154.0
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 140628s2014 gw | s |||| 0|eng d
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
ISBN 9783319088679
-- 978-3-319-08867-9
082 04 - CLASSIFICATION NUMBER
Call Number 005.1015113
245 10 - TITLE STATEMENT
Title Computer Aided Verification
Sub Title 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings /
300 ## - PHYSICAL DESCRIPTION
Number of Pages XXXIV, 877 p. 205 illus.
490 1# - SERIES STATEMENT
Series statement Lecture Notes in Computer Science,
505 0# - FORMATTED CONTENTS NOTE
Remark 2 Software 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.
520 ## - SUMMARY, ETC.
Summary, etc This 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.
700 1# - AUTHOR 2
Author 2 Biere, Armin.
700 1# - AUTHOR 2
Author 2 Bloem, Roderick.
856 40 - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier http://dx.doi.org/10.1007/978-3-319-08867-9
942 ## - ADDED ENTRY ELEMENTS (KOHA)
Koha item type eBooks
264 #1 -
-- Cham :
-- Springer International Publishing :
-- Imprint: Springer,
-- 2014.
336 ## -
-- text
-- txt
-- rdacontent
337 ## -
-- computer
-- c
-- rdamedia
338 ## -
-- online resource
-- cr
-- rdacarrier
347 ## -
-- text file
-- PDF
-- rda
650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Computer science.
650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Computer organization.
650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Software engineering.
650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Computer logic.
650 #0 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Mathematical logic.
650 14 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Computer Science.
650 24 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Logics and Meanings of Programs.
650 24 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Software Engineering/Programming and Operating Systems.
650 24 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Mathematical Logic and Formal Languages.
650 24 - SUBJECT ADDED ENTRY--SUBJECT 1
-- Computer Systems Organization and Communication Networks.
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
-- 0302-9743 ;
912 ## -
-- ZDB-2-SCS
912 ## -
-- ZDB-2-LNC

No items available.