國立虎尾科技大學 |

Automated Technology for Verification and Analysis = 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings /

紀錄類型:	書目-語言資料,印刷品 : Monograph/item
正題名/作者:	Automated Technology for Verification and Analysis/ edited by Cyrille Artho, Axel Legay, Doron Peled.
其他題名:	14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings /
其他作者:	Artho, Cyrille.
面頁冊數:	XI, 530 p. 102 illus.online resource. :
Contained By:	Springer Nature eBook
標題:	Software engineering. -
電子資源:	https://doi.org/10.1007/978-3-319-46520-3
ISBN:	9783319465203

Automated Technology for Verification and Analysis = 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings /
Automated Technology for Verification and Analysis14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings /[electronic resource] :edited by Cyrille Artho, Axel Legay, Doron Peled. - 1st ed. 2016. - XI, 530 p. 102 illus.online resource. - Programming and Software Engineering ;9938. - Programming and Software Engineering ;8987.

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. .

This 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. .

ISBN: 9783319465203

Standard No.: 10.1007/978-3-319-46520-3doiSubjects--Topical Terms:

562952
Software engineering.

LC Class. No.: QA76.758

Dewey Class. No.: 005.1

Automated Technology for Verification and Analysis = 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings /
LDR:04335nam a22004095i 4500 001 972762
003 DE-He213
005 20200629195935.0
007 cr nn 008mamaa
008 201211s2016 gw | s |||| 0|eng d
020 $a 9783319465203 $9 978-3-319-46520-3
024 7 $a 10.1007/978-3-319-46520-3 $2 doi
035 $a 978-3-319-46520-3
050 4 $a QA76.758
072 7 $a UMZ $2 bicssc
072 7 $a COM051230 $2 bisacsh
072 7 $a UMZ $2 thema
082 0 4 $a 005.1 $2 23
245 1 0 $a Automated Technology for Verification and Analysis $h [electronic resource] : $b 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings / $c edited by Cyrille Artho, Axel Legay, Doron Peled.
250 $a 1st ed. 2016.
264 1 $a Cham : $b Springer International Publishing : $b Imprint: Springer, $c 2016.
300 $a XI, 530 p. 102 illus. $b online resource.
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
347 $a text file $b PDF $2 rda
490 1 $a Programming and Software Engineering ; $v 9938
505 0 $a 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. .
520 $a This 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 $a Software engineering. $3 562952
650 0 $a Programming languages (Electronic computers). $3 1127615
650 0 $a Computer logic. $3 786340
650 0 $a Mathematical logic. $2 bicssc $3 810627
650 0 $a Artificial intelligence. $3 559380
650 0 $a Computer programming. $3 527822
650 1 4 $a Software Engineering. $3 669632
650 2 4 $a Programming Languages, Compilers, Interpreters. $3 669782
650 2 4 $a Logics and Meanings of Programs. $3 670058
650 2 4 $a Mathematical Logic and Formal Languages. $3 670059
650 2 4 $a Artificial Intelligence. $3 646849
650 2 4 $a Programming Techniques. $3 669781
700 1 $a Artho, Cyrille. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 1105749
700 1 $a Legay, Axel. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 1078519
700 1 $a Peled, Doron. $e editor. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 1267859
710 2 $a SpringerLink (Online service) $3 593884
773 0 $t Springer Nature eBook
776 0 8 $i Printed edition: $z 9783319465197
776 0 8 $i Printed edition: $z 9783319465210
830 0 $a Programming and Software Engineering ; $v 8987 $3 1253476
856 4 0 $u https://doi.org/10.1007/978-3-319-46520-3
912 $a ZDB-2-SCS
912 $a ZDB-2-SXCS
912 $a ZDB-2-LNC
950 $a Computer Science (SpringerNature-11645)
950 $a Computer Science (R0) (SpringerNature-43710)