Automated Technology for Verification and Analysis : 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings / edited by Deepak D'Souza, K. Narayan Kumar.

Format:

Book

Contributor:

D'Souza, Deepak, Editor.

Narayan Kumar, K., Editor.

SpringerLink (Online service)

Series:

Computer Science (SpringerNature-11645)

LNCS sublibrary. Programming and software engineering 2945-9168 ; SL 2, 10482

Programming and Software Engineering, 2945-9168 ; 10482

Language:

English

Subjects (All):

Software engineering.

Compilers (Computer programs).

Computer engineering.

Computer networks.

Computers.

Computer science.

Artificial intelligence.

Software Engineering.

Compilers and Interpreters.

Computer Engineering and Networks.

Computing Milieux.

Theory of Computation.

Artificial Intelligence.

Local Subjects:

Software Engineering.

Compilers and Interpreters.

Computer Engineering and Networks.

Computing Milieux.

Theory of Computation.

Artificial Intelligence.

Physical Description:

1 online resource (XIX, 482 pages) : 106 illustrations

Edition:

1st ed. 2017.

Contained In:

Springer Nature eBook

Place of Publication:

Cham : Springer International Publishing : Imprint: Springer, 2017.

System Details:

text file PDF

Summary:

This book constitutes the refereed proceedings of the 15th International Symposium on Automated Technology for Verification and Analysis, ATVA 2017, held in Pune, India, in October 2017. The 22 full and 7 short papers presented in this volume were carefully reviewed and selected from 78 submissions. The book also contains one invited talk in full-paper length. The contributions are organized in topical sections named: program analysis; model checking and temporal logics; neural networks; learning and invariant synthesis; and hybrid systems and control.

Contents:

Invited Talk: Proving Absence of Starvation by Means of Abstract Interpretation and Model-checking

Program Analysis

Precise Null Pointer Analysis Through Global Value Numbering

May-Happen-in-Parallel Analysis with Returned Futures

JTDec: A Tool for Tree Decompositions in Soot

Fixing the State Budget: Approximation of Regular Languages with Small DFAs

An Equivalence Checking Framework for Array-Intensive Programs.-Loop Quasi-Invariant Chunk Detection

SamaTulyata: An Efficient Path Based Equivalence Checking Tool

Model Checking and Temporal Logics

Tests and Refutation

The Density of Linear-time Properties

HyLeak: Hybrid Analysis Tool for Information Leakage

Compositional Safety Refutation Techniques

Gradient-based variable ordering of Decision Diagrams for systems with structural units

Model Checking of C and C++ with DIVINE 4 (Tool Paper)

Dealing with priorities and locks for concurrent programs

Knowledge transfer and information leakage in protocols

Concurrent Program Verification With Invariant-guided Underapproximation

Neural Networks

Maximum Resilience of Artificial Neural Networks

Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks

Learning and Invariant Synthesis

Liquid Types for Array Invariant Synthesis

Lifting CDCL to Template-based Abstract Domains for Program Verification

Synthesizing invariants by solving solvable loops

Requirements and Specifications Exploiting Partial Knowledge for Efficient Model Analysis

A Language-theoretic View on Network Protocols

Probabilistic Systems Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes

Finding Polynomial Loop Invariants for Probabilistic Programs

Synthesis of Optimal Resilient Control Strategies

Hybrid Systems and Control

ForFET: A Formal Feature Evaluation Tool for Hybrid Systems

Attacking the V: On the Resiliency of Adaptive-Horizon MPC

The Reach-Avoid Problem for Constant-Rate Multi-Mode Systems.

Other Format:

Printed edition:

ISBN:

978-3-319-68167-2

9783319681672

Access Restriction:

Restricted for use by site license.