Automated Technology for Verification and Analysis: 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, ProceedingsShuvendu K. Lahiri, Chao Wang This book constitutes the refereed proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis, ATVA 2018, held in Los Angeles, CA, USA in October 2018. The 27 full papers presented together with 5 short papers and 3 invited talks were carefully reviewed and selected from 82 submissions.
The symposium is dedicated to the promotion of research on theoretical and practical aspects of automated analysis, verification and synthesis by providing a forum for interaction between the regional and the international research communities and industry in the field. |
Contents
| 3 | |
| 20 | |
Regular Papers | 35 |
Optimal Proofs for Linear Temporal Logic on Lasso Words | 36 |
Whats to Come is Still Unsure | 56 |
A Formally Verified Motion Planner for Autonomous Vehicles | 75 |
Robustness Testing of Intermediate Verifiers | 91 |
Simulation Algorithms for Symbolic Automata | 109 |
A Fragment of Linear Temporal Logic for Universal Very Weak Automata | 335 |
Quadratic Word Equations with Length Constraints Counter Systems and Presburger Arithmetic with Divisibility | 352 |
RoundBounded Control of Parameterized Systems | 370 |
Automatic Sensitivity Analysis for Probabilistic Programs | 387 |
Information Leakage in Arbiter Protocols | 404 |
Neural State Classification for Hybrid Systems | 422 |
Bounded Synthesis of Reactive Programs | 441 |
Maximum Realizability for Linear Temporal Logic Specifications | 458 |
Quantitative Projection Coverage for Testing MLenabled Autonomous Systems | 126 |
Recursive Online Enumeration of All Minimal Unsatisfiable Subsets | 143 |
A Tale of 1001 Parameters | 160 |
Temporal Logic Verification of Stochastic Systems Using Barrier Certificates | 177 |
Bisimilarity Distances for Approximate Differential Privacy | 194 |
A Symbolic Algorithm for Lazy Synthesis of Eager Strategies | 211 |
Modular Verification of Concurrent Programs via Sequential Model Checking | 228 |
Quantifiers on Demand | 248 |
Signal Convolution Logic | 267 |
Efficient Symbolic Representation of Convex Polyhedra in HighDimensional Spaces | 284 |
Accelerated Model Checking of Parametric Markov Chains | 300 |
ContinuousTime Markov Decisions Based on Partial Exploration | 317 |
Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs | 476 |
Bounded Synthesis of Register Transducers | 494 |
Tool Papers | 511 |
A Framework for HighLevel Analysis of Ethereum Bytecode | 513 |
Checking Satisfiability of HyperLTL Formulas Beyond the Fragment | 521 |
Verifying Rust Programs with SMACK | 528 |
Statistical Model Checking Stochastic RealTime Systems | 536 |
A Library for Words Automata and LTL | 543 |
A Tool for Temporal Equilibrium Analysis | 551 |
| 558 | |
Other editions - View all
Automated Technology for Verification and Analysis: 16th International ... Shuvendu K. Lahiri,Chao Wang No preview available - 2018 |
Common terms and phrases
abstraction adversarial algorithm analysis applying approach ATVA automata automaton benchmarks bisimulation Boogie Boolean bounded synthesis Büchi Büchi automaton clusters computation counterexample CTMDP defined denote DNNs domain encoding evaluation example finite formal formal verification function given graph Heidelberg Hyperglycemia IEEE implementation infinite initial input instantiations iteration label Lemma linear linear temporal logic LLVM LNCS LTL formula Markov Markov chains metric mintermisation model checking mutants neural networks node operators output parameters path player polynomial probabilistic programs problem procedure properties protocols PSense quantified QUIC3 represent robustness safety sampling satisfies Sect semantics simulation simulation preorder smart contracts solver solving specification Springer stochastic strategy subset symbolic TACAS techniques temporal logic testing Theorem tion tool trace transducer transition relation transition system tuple variables verification violation word equations