| Document Type
|
:
|
BL
|
| Record Number
|
:
|
866092
|
| Main Entry
|
:
|
TACAS (Conference)(24th :2018 :, Thessalonikē, Greece)
|
| Title & Author
|
:
|
Tools and algorithms for the construction and analysis of systems : : 24th International Conference, TACAS 2018, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings.\ Dirk Beyer, Marieke Huisman (eds.).
|
| Publication Statement
|
:
|
Cham, Switzerland :: Springer Open,, 2018.
|
| Series Statement
|
:
|
Advanced research in computing and software science
|
|
|
:
|
Lecture notes in computer science,; 10805
|
|
|
:
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues
|
| Page. NO
|
:
|
1 online resource (xx, 429 pages) :: illustrations
|
| ISBN
|
:
|
3319899600
|
|
|
:
|
: 9783319899602
|
|
|
:
|
9783319899596
|
| Notes
|
:
|
Includes author index.
|
|
|
:
|
International conference proceedings.
|
| Contents
|
:
|
Theorem Proving -- Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning -- Efficient verification of imperative programs using auto2 -- Frame Inference for Inductive Entailment Proofs in Separation Logic -- Verified Model Checking of Timed Automata -- SAT and SMT I -- Chain Reduction for Binary and Zero-Suppressed Decision Diagrams -- CDCLSym: Introducing E_ective Symmetry Breaking in SAT Solving -- Automatic Generation of Precise and Useful Commutativity Conditions -- Bit-Vector Model Counting using Statistical Estimation -- Deductive Verification -- Hoare Logics for Time Bounds -- A Verified Implementation of the Bounded List Container -- Automating Deductive Verification for Weak-Memory Programs -- Software Verification and Optimisation -- Property Checking Array Programs Using Loop Shrinking -- Invariant Synthesis for Incomplete Verification Engines -- Accelerating Syntax-Guided Invariant Synthesis -- Daisy -- Framework for Analysis and Optimization of Numerical Programs -- Model Checking -- Oink: an Implementation and Evaluation of Modern Parity Game Solvers -- More Scalable LTL Model Checking via Discovering Design-Space Dependencies (D^3) -- Generation of Minimum Tree-like Witnesses for Existential CTL -- From Natural Projection to Partial Model Checking and Back -- Machine Learning -- ICE-based Refinement Type Discovery for Higher-Order Functional Programs -- Strategy Representation by Decision Trees in Reactive Synthesis -- Feature-Guided Black-Box Safety Testing of Deep Neural Networks.
|
| Abstract
|
:
|
This book is Open Access under a CC BY licence.
|
| Subject
|
:
|
Computer software-- Verification, Congresses.
|
| Subject
|
:
|
System analysis, Congresses.
|
| Subject
|
:
|
System design, Congresses.
|
| Subject
|
:
|
Algorithms data structures.
|
| Subject
|
:
|
Computer programming-- software development.
|
| Subject
|
:
|
Computer software-- Verification.
|
| Subject
|
:
|
Computers-- Hardware-- Handheld Devices.
|
| Subject
|
:
|
Computers-- Information Theory.
|
| Subject
|
:
|
Computers-- Programming-- General.
|
| Subject
|
:
|
Computers-- Social Aspects-- Human-Computer Interaction.
|
| Subject
|
:
|
Computers-- Software Development Engineering-- General.
|
| Subject
|
:
|
Information technology: general issues.
|
| Subject
|
:
|
Software Engineering.
|
| Subject
|
:
|
System analysis.
|
| Subject
|
:
|
System design.
|
| Subject
|
:
|
Systems analysis design.
|
| Dewey Classification
|
:
|
004.2/1
|
| LC Classification
|
:
|
QA76.9.S88
|
| Added Entry
|
:
|
Beyer, Dirk,1972-
|
|
|
:
|
Huisman, Marieke
|
| Added Entry
|
:
|
ETAPS (Conference)(21st :2018 :, Thessalonikē , Greece)
|
| Parallel Title
|
:
|
TACAS 2018
|