Automated Technology for Verification and Analysis
Springer International Publishing (Verlag)
978-3-319-46519-7 (ISBN)
The 31 papers presented in this volume were carefully reviewed and selected from 82 submissions. They were organized in topical sections named: keynote; Markov models, chains, and decision processes; counter systems, automata; parallelism, concurrency; complexity, decidability; synthesis, refinement; optimization, heuristics, partial-order reductions; solving procedures, model checking; and program analysis.
Keynote.- Synthesizing and Completely Testing Hardware based on Templates through Small Numbers of Test Patterns.- Markov Models, Chains, and Decision Processes.- Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations. -Optimizing the Expected Mean Payoff in Energy Markov Decision Processes.- Parameter Synthesis for Markov Models: Faster Than Ever.- Bounded Model Checking for Probabilistic Programs.- Counter Systems, Automata.- How Hard Is It to Verify Flat Affine Counter Systems with the Finite Monoid Property.- Solving Language Equations using Flanked Automata.- Spot 2.0 - a Framework for LTL and -Automata Manipulation.- MoChiBA: Probabilistic LTL Model Checking Using Limit- Deterministic Büchi Automata.- Parallelism, Concurrency.- Synchronous Products of Rewrite Systems.- Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents.- Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs.- Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems.- Complexity, Decidability.- On Finite Domains in First-Order Linear Temporal Logic.- Decidability Results for Multi-Objective Stochastic Games.- A Decision Procedure for Separation Logic in SMT.- Solving Mean-Payoff Games on the GPU.- Synthesis, Refinement.- Synthesizing Skeletons for Reactive Systems.- Observational Refinement and Merge for Disjunctive MTSs.- Equivalence-Based Abstraction Refinement for muHORS Model Checking.- Optimization, Heuristics, Partial-Order Reductions.- Greener Bits: Formal Analysis of Demand Response.- Heuristics for Checking Liveness Properties with Partial Order Reductions. - Partial-Order Reduction for GPU Model Checking.- Efficient Verification of Program Fragments: Eager POR.- Solving Procedures, Model Checking.- Skolem Functions for DQBF.- STL Model Checking of Continuous and Hybrid Systems.- Clause Sharing and Partitioning for Cloud-Based SMT Solving.- Symbolic Model Checking for Factored Probabilistic Models.- Program Analysis.- A Sketching-Based Approach for Debugging Using Test Cases.- Polynomial Invariants by Linear Algebra.- Certified Symbolic Execution.- Tighter Loop Bound Analysis.
| Erscheinungsdatum | 26.10.2016 |
|---|---|
| Reihe/Serie | Lecture Notes in Computer Science | Programming and Software Engineering |
| Zusatzinfo | XI, 530 p. 102 illus. |
| Verlagsort | Cham |
| Sprache | englisch |
| Maße | 155 x 235 mm |
| Themenwelt | Mathematik / Informatik ► Informatik ► Software Entwicklung |
| Schlagworte | Applications • Complexity • Computer Science • Concurrency • conference proceedings • data center • Decidability • Dynamic Programming • formal modeling • GPGPU • Hybrid Systems • Informatics • Markov Decision Processes • Model Checking • Optimization • Parallelism • probabilistic model checking • program analysis • Reachability Analysis • Research • software certification • Software engineering • Static Analysis • symbolic execution • temporal logic • verification |
| ISBN-10 | 3-319-46519-8 / 3319465198 |
| ISBN-13 | 978-3-319-46519-7 / 9783319465197 |
| Zustand | Neuware |
| Haben Sie eine Frage zum Produkt? |
aus dem Bereich
