000 05403nam a22006375i 4500
001 978-3-319-46520-3
003 DE-He213
005 20240730165026.0
007 cr nn 008mamaa
008 160921s2016 sz | s |||| 0|eng d
020 _a9783319465203
_9978-3-319-46520-3
024 7 _a10.1007/978-3-319-46520-3
_2doi
050 4 _aQA76.758
072 7 _aUMZ
_2bicssc
072 7 _aCOM051230
_2bisacsh
072 7 _aUMZ
_2thema
082 0 4 _a005.1
_223
245 1 0 _aAutomated Technology for Verification and Analysis
_h[electronic resource] :
_b14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings /
_cedited by Cyrille Artho, Axel Legay, Doron Peled.
250 _a1st ed. 2016.
264 1 _aCham :
_bSpringer International Publishing :
_bImprint: Springer,
_c2016.
300 _aXI, 530 p. 102 illus.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aProgramming and Software Engineering,
_x2945-9168 ;
_v9938
505 0 _aKeynote -- 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. .
520 _aThis book constitutes the proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016, held in Chiba, Japan, in October 2016. 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. .
650 0 _aSoftware engineering.
_94138
650 0 _aCompilers (Computer programs).
_93350
650 0 _aComputer science.
_99832
650 0 _aMachine theory.
_987140
650 0 _aArtificial intelligence.
_93407
650 0 _aComputer programming.
_94169
650 1 4 _aSoftware Engineering.
_94138
650 2 4 _aCompilers and Interpreters.
_931853
650 2 4 _aComputer Science Logic and Foundations of Programming.
_942203
650 2 4 _aFormal Languages and Automata Theory.
_987143
650 2 4 _aArtificial Intelligence.
_93407
650 2 4 _aProgramming Techniques.
_987146
700 1 _aArtho, Cyrille.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_987147
700 1 _aLegay, Axel.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_987149
700 1 _aPeled, Doron.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_987151
710 2 _aSpringerLink (Online service)
_987153
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783319465197
776 0 8 _iPrinted edition:
_z9783319465210
830 0 _aProgramming and Software Engineering,
_x2945-9168 ;
_v9938
_987155
856 4 0 _uhttps://doi.org/10.1007/978-3-319-46520-3
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c86057
_d86057