Computer Aided Verification (Record no. 55752)

000 -LEADER
fixed length control field 05603nam a22005895i 4500
001 - CONTROL NUMBER
control field 978-3-319-21690-4
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20200421111845.0
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 150715s2015 gw | s |||| 0|eng d
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
ISBN 9783319216904
-- 978-3-319-21690-4
082 04 - CLASSIFICATION NUMBER
Call Number 005.1015113
245 10 - TITLE STATEMENT
Title Computer Aided Verification
Sub Title 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I /
300 ## - PHYSICAL DESCRIPTION
Number of Pages XXIII, 677 p. 141 illus.
490 1# - SERIES STATEMENT
Series statement Lecture Notes in Computer Science,
505 0# - FORMATTED CONTENTS NOTE
Remark 2 A Trusted Mechanised Specification of JavaScript: One Year On -- Model Checking and Refinements -- On Automation of CTL* Verification for Infinite-State Systems -- Algorithms for Model Checking HyperLTL and HyperCTL -- Fairness Modulo Theory: A New Approach to LTL Software Model Checking -- Model Checking Parameterized Asynchronous Shared-Memory Systems -- SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms -- Skipping Refinement -- Quantitative Reasoning -- Percentile Queries in Multi-dimensional Markov Decision Processes -- Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs -- Counterexample Explanation by Learning Small Strategies in Markov Decision Processes -- Symbolic Polytopes for Quantitative Interpolation and Verification -- Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks -- PROPhESY: A PRObabilistic ParamEter SYnthesis Tool -- Software Analysis -- Effective Search-Space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints -- Automata-Based Model Counting for String Constraints -- OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case -- Tree Buffers -- Learning Commutativity -- Specifications -- Angelic Verification: Precise Verification Modulo Unknowns -- The SeaHorn Verification Framework -- Automatic Rootcausing for Program Equivalence Failures in Binaries -- Fine-Grained Caching of Verification Results -- Predicting a Correct Program in Programming by Example -- Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation -- Lightning Talks -- ADAM: Causality-Based Synthesis of Distributed Systems -- Alchemist: Learning Guarded Affine Functions -- OptiMathSAT: A Tool for Optimization Modulo Theories -- Systematic Asynchrony Bug Exploration for Android Apps -- Norn: An SMT Solver for String Constraints -- PVSio-web 2.0: Joining PVS to HCI -- The Hanoi Omega-Automata Format -- The Open-Source LearnLib: A Framework for Active Automata Learning -- BBS: A Phase-Bounded Model Checker for Asynchronous Programs -- Time-Aware Abstractions in HybridSal -- A Type-Directed Approach to Program Repair -- Formal Design and Safety Analysis of AIR6110 Wheel Brake System -- Meeting a Powertrain Verification Challenge -- Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data -- Empirical Software Metrics for Benchmarking of Verification Tools -- Interpolation, IC3/PDR, and Invariants Property-Directed Inference of Universal Invariants or Proving Their Absence -- Efficient Anytime Techniques for Model-Based Safety Analysis -- Boosting k-induction with Continuously-Refined Invariants -- Fast Interpolating BMC -- Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation.
520 ## - SUMMARY, ETC.
Summary, etc The two-volume set LNCS 9206 and LNCS 9207 constitutes the refereed proceedings of the 27th International Conference on Computer Aided Verification, CAV 2015, held in San Francisco, CA, USA, in July 2015. The total of 58 full and 11 short papers presented in the proceedings was carefully reviewed and selected from 252 submissions. The papers were organized in topical sections named: model checking and refinements; quantitative reasoning; software analysis; lightning talks; interpolation, IC3/PDR, and Invariants; SMT techniques and applications; HW verification; synthesis; termination; and concurrency.
700 1# - AUTHOR 2
Author 2 Kroening, Daniel.
700 1# - AUTHOR 2
Author 2 Păsăreanu, Corina S.
856 40 - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier http://dx.doi.org/10.1007/978-3-319-21690-4
942 ## - ADDED ENTRY ELEMENTS (KOHA)
Koha item type eBooks
264 #1 -
-- Cham :
-- Springer International Publishing :
-- Imprint: Springer,
-- 2015.
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.