國立虎尾科技大學 |

Tools and Algorithms for the Construction and Analysis of Systems = 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings /

紀錄類型:	書目-語言資料,印刷品 : Monograph/item
正題名/作者:	Tools and Algorithms for the Construction and Analysis of Systems/ edited by Christel Baier, Cesare Tinelli.
其他題名:	21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings /
其他作者:	Baier, Christel.
面頁冊數:	XVIII, 725 p. 210 illus.online resource. :
Contained By:	Springer Nature eBook
標題:	Computer logic. -
電子資源:	https://doi.org/10.1007/978-3-662-46681-0
ISBN:	9783662466810

Tools and Algorithms for the Construction and Analysis of Systems = 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings /
Tools and Algorithms for the Construction and Analysis of Systems21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings /[electronic resource] :edited by Christel Baier, Cesare Tinelli. - 1st ed. 2015. - XVIII, 725 p. 210 illus.online resource. - Theoretical Computer Science and General Issues ;9035. - Theoretical Computer Science and General Issues ;9163.

Scalable Timing Analysis with Refinement -- A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System -- Verified Reachability Analysis of Continuous Systems -- HyComp: An SMT-Based Model Checker for Hybrid Systems -- C2E2: A Verification Tool for Stateflow Models -- Non-cumulative Resource Analysis -- Value Slice: A New Slicing Concept for Scalable Property Checking -- A Method for Improving the Precision and Coverage of Atomicity Violation Predictions -- Commutativity of Reducers -- Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling -- Analysis of Dynamic Process Networks -- MULTIGAIN: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives -- syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications -- vZ - An Optimizing SMT Solver -- dReach: δ-Reachability Analysis for Hybrid Systems -- Uppaal Stratego -- BINSEC: Binary Code Analysis with Low-Level Regions -- Insight: An Open Binary Analysis Framework -- SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform -- Symbolic Model-Checking Using ITS-Tools -- Semantic Importance Sampling for Statistical Model Checking -- Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives -- FAUST2: Formal Abstractions of Uncountable-State Stochastic Processes -- Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving -- On Parallel Scalable Uniform SAT Witness Generation -- Approximate Counting in SMT and Value Estimation for Probabilistic Programs -- Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions -- Stateless Model Checking for TSO and PSO -- GPU Accelerated Strong and Branching Bisimilarity Checking -- Fairness for Infinite-State Systems -- Software Verification and Verifiable Witnesses -- AProVE: Termination and Memory Safety of C Programs -- Cascade -- CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic -- CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation -- Framework for Embedded System Verification -- Forester: Shape Analysis Using Tree Automata -- MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings -- Perentie: Modular Trace Refinement and Selective Value Tracking -- Predator Hunting Party -- SeaHorn: A Framework for Verifying C Programs -- SMACK+Corral: A Modular Verifier -- Ultimate Automizer with Array Interpolation -- Ultimate Kojak with Memory Safety Checks -- Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches -- FuncTion: An Abstract Domain Functor for Termination -- Model Checking Gene Regulatory Networks -- Symbolic Quantitative Robustness Analysis of Timed Automata -- Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis -- Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information -- Shield Synthesis: Runtime Enforcement for Reactive Systems -- Verifying Concurrent Programs by Memory Unwinding -- AutoProof: Auto-Active Functional Verification of Object-Oriented Programs -- An LTL Proof System for Runtime Verification -- MARQ: Monitoring at Runtime with QEA -- Parallel Explicit Model Checking for Generalized Bchi Automata -- Limit Deterministic and Probabilistic Automata for LTL\GU -- Saturation-Based Incremental LTL Model Checking with Inductive Proofs -- Nested Antichains for WS1S -- Sylvan: Multi-core Decision Diagrams -- LTSmin: High-Performance Language-Independent Model Checking -- Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip.

This book constitutes the proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015, which took place in London, UK, in April 2015, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015. The 45 papers included in this volume, consisting of 27 research papers, 2 case-study papers, 7 regular tool papers and 9 tool demonstration papers, were carefully reviewed and selected from 164 submissions. In addition, the book contains one invited contribution. The papers have been organized in topical sections on hybrid systems; program analysis; verification and abstraction; tool demonstrations; stochastic models; SAT and SMT; partial order reduction, bisimulation, and fairness; competition on software verification; parameter synthesis; program synthesis; program and runtime verification; temporal logic and automata and model checking.

ISBN: 9783662466810

Standard No.: 10.1007/978-3-662-46681-0doiSubjects--Topical Terms:

786340
Computer logic.

LC Class. No.: QA76.9.L63

Dewey Class. No.: 005.1015113

Tools and Algorithms for the Construction and Analysis of Systems = 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings /
LDR:06284nam a22004335i 4500 001 969239
003 DE-He213
005 20200704083350.0
007 cr nn 008mamaa
008 201211s2015 gw | s |||| 0|eng d
020 $a 9783662466810 $9 978-3-662-46681-0
024 7 $a 10.1007/978-3-662-46681-0 $2 doi
035 $a 978-3-662-46681-0
050 4 $a QA76.9.L63
050 4 $a QA76.5913
072 7 $a UM $2 bicssc
072 7 $a COM051000 $2 bisacsh
072 7 $a UM $2 thema
072 7 $a UYF $2 thema
082 0 4 $a 005.1015113 $2 23
245 1 0 $a Tools and Algorithms for the Construction and Analysis of Systems $h [electronic resource] : $b 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings / $c edited by Christel Baier, Cesare Tinelli.
250 $a 1st ed. 2015.
264 1 $a Berlin, Heidelberg : $b Springer Berlin Heidelberg : $b Imprint: Springer, $c 2015.
300 $a XVIII, 725 p. 210 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 Theoretical Computer Science and General Issues ; $v 9035
505 0 $a Scalable Timing Analysis with Refinement -- A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System -- Verified Reachability Analysis of Continuous Systems -- HyComp: An SMT-Based Model Checker for Hybrid Systems -- C2E2: A Verification Tool for Stateflow Models -- Non-cumulative Resource Analysis -- Value Slice: A New Slicing Concept for Scalable Property Checking -- A Method for Improving the Precision and Coverage of Atomicity Violation Predictions -- Commutativity of Reducers -- Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling -- Analysis of Dynamic Process Networks -- MULTIGAIN: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives -- syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications -- vZ - An Optimizing SMT Solver -- dReach: δ-Reachability Analysis for Hybrid Systems -- Uppaal Stratego -- BINSEC: Binary Code Analysis with Low-Level Regions -- Insight: An Open Binary Analysis Framework -- SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform -- Symbolic Model-Checking Using ITS-Tools -- Semantic Importance Sampling for Statistical Model Checking -- Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives -- FAUST2: Formal Abstractions of Uncountable-State Stochastic Processes -- Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving -- On Parallel Scalable Uniform SAT Witness Generation -- Approximate Counting in SMT and Value Estimation for Probabilistic Programs -- Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions -- Stateless Model Checking for TSO and PSO -- GPU Accelerated Strong and Branching Bisimilarity Checking -- Fairness for Infinite-State Systems -- Software Verification and Verifiable Witnesses -- AProVE: Termination and Memory Safety of C Programs -- Cascade -- CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic -- CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation -- Framework for Embedded System Verification -- Forester: Shape Analysis Using Tree Automata -- MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings -- Perentie: Modular Trace Refinement and Selective Value Tracking -- Predator Hunting Party -- SeaHorn: A Framework for Verifying C Programs -- SMACK+Corral: A Modular Verifier -- Ultimate Automizer with Array Interpolation -- Ultimate Kojak with Memory Safety Checks -- Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches -- FuncTion: An Abstract Domain Functor for Termination -- Model Checking Gene Regulatory Networks -- Symbolic Quantitative Robustness Analysis of Timed Automata -- Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis -- Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information -- Shield Synthesis: Runtime Enforcement for Reactive Systems -- Verifying Concurrent Programs by Memory Unwinding -- AutoProof: Auto-Active Functional Verification of Object-Oriented Programs -- An LTL Proof System for Runtime Verification -- MARQ: Monitoring at Runtime with QEA -- Parallel Explicit Model Checking for Generalized Bchi Automata -- Limit Deterministic and Probabilistic Automata for LTL\GU -- Saturation-Based Incremental LTL Model Checking with Inductive Proofs -- Nested Antichains for WS1S -- Sylvan: Multi-core Decision Diagrams -- LTSmin: High-Performance Language-Independent Model Checking -- Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip.
520 $a This book constitutes the proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015, which took place in London, UK, in April 2015, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015. The 45 papers included in this volume, consisting of 27 research papers, 2 case-study papers, 7 regular tool papers and 9 tool demonstration papers, were carefully reviewed and selected from 164 submissions. In addition, the book contains one invited contribution. The papers have been organized in topical sections on hybrid systems; program analysis; verification and abstraction; tool demonstrations; stochastic models; SAT and SMT; partial order reduction, bisimulation, and fairness; competition on software verification; parameter synthesis; program synthesis; program and runtime verification; temporal logic and automata and model checking.
650 0 $a Computer logic. $3 786340
650 0 $a Algorithms. $3 527865
650 0 $a Software engineering. $3 562952
650 0 $a Computers. $3 565115
650 0 $a Programming languages (Electronic computers). $3 1127615
650 0 $a Mathematical logic. $2 bicssc $3 810627
650 1 4 $a Logics and Meanings of Programs. $3 670058
650 2 4 $a Algorithm Analysis and Problem Complexity. $3 593923
650 2 4 $a Software Engineering. $3 669632
650 2 4 $a Computation by Abstract Devices. $3 669792
650 2 4 $a Programming Languages, Compilers, Interpreters. $3 669782
650 2 4 $a Mathematical Logic and Formal Languages. $3 670059
700 1 $a Baier, Christel. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 574260
700 1 $a Tinelli, Cesare. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 815883
710 2 $a SpringerLink (Online service) $3 593884
773 0 $t Springer Nature eBook
776 0 8 $i Printed edition: $z 9783662466827
776 0 8 $i Printed edition: $z 9783662466803
830 0 $a Theoretical Computer Science and General Issues ; $v 9163 $3 1253524
856 4 0 $u https://doi.org/10.1007/978-3-662-46681-0
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)