國立虎尾科技大學 |

Computer aided verification = 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019 : proceedings.. Part I /

紀錄類型:	書目-語言資料,印刷品 : Monograph/item
正題名/作者:	Computer aided verification/ edited by Isil Dillig, Serdar Tasiran.
其他題名:	31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019 : proceedings.
其他題名:	CAV 2019
其他作者:	Dillig, Isil.
團體作者:	Workshop on the Preservation of Stability under Discretization
出版者:	Cham :Springer International Publishing : : 2019.,
面頁冊數:	xix, 673 p. :ill., digital ; : 24 cm.;
Contained By:	Springer eBooks
標題:	Computer programs - Congresses. - Verification -
電子資源:	https://doi.org/10.1007/978-3-030-25540-4
ISBN:	9783030255404

Computer aided verification = 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019 : proceedings.. Part I /
Computer aided verification31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019 : proceedings.Part I /[electronic resource] :CAV 2019edited by Isil Dillig, Serdar Tasiran. - Cham :Springer International Publishing :2019. - xix, 673 p. :ill., digital ;24 cm. - Lecture notes in computer science,115610302-9743 ;. - Lecture notes in computer science ;6140..

Automata and Timed Systems -- Symbolic Register Automata -- Abstraction Refinement Algorithms for Timed Automata -- Fast Algorithms for Handling Diagonal Constraints in Timed Automata -- Safety and co-safety comparator automata for discounted-sum inclusion -- Clock Bound Repair for Timed Systems -- Verifying Asynchronous Interactions via Communicating Session Automata -- Security and Hyperproperties -- Verifying Hyperliveness -- Quantitative Mitigation of Timing Side Channels -- Property Directed Self Composition -- Security-Aware Synthesis Using Delayed-Action Games -- Automated Hypersafety Verification -- Automated Synthesis of Secure Platform Mappings -- Synthesis -- Synthesizing Approximate Implementations for Unrealizable Specifications -- Quantified Invariants via Syntax-Guided Synthesis -- Efficient Synthesis with Probabilistic Constraints -- Membership-based Synthesis of Linear Hybrid Automata -- Overfitting in Synthesis: Theory and Practice -- Proving Unrealizability for Syntax-Guided Synthesis -- Model Checking -- BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings -- When Human Intuition Fails: Using Formal Methods to Find an Error in the "Proof" of a Multi-Agent Protocol -- Extending NUXMV with Timed Transition Systems and Timed Temporal Properties -- Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C -- Cyber-physical Systems and Machine Learning -- Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification -- StreamLAB: Stream-based Monitoring of Cyber-Physical Systems -- VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems -- The Marabou Framework for Verification and Analysis of Deep Neural Networks -- Probabilistic Systems, Runtime Techniques -- Probabilistic Bisimulation for Parameterized Systems -- Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks -- PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games -- Symbolic Monitoring against Specifications Parametric in Time and Data -- STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis -- Dynamical, Hybrid, and Reactive Systems -- Local and Compositional Reasoning For Optimized Reactive Systems -- Robust Controller Synthesis in Timed Buchi Automata: A Symbolic Approach -- Flexible Computational Pipelines for Robust Abstraction-based Control Synthesis -- Temporal Stream Logic: Synthesis beyond the Bools -- Run-Time Optimization for Learned Controllers through Quantitative Games -- Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations.

Open access.

This open access two-volume set LNCS 11561 and 11562 constitutes the refereed proceedings of the 31st International Conference on Computer Aided Verification, CAV 2019, held in New York City, USA, in July 2019. The 52 full papers presented together with 13 tool papers and 2 case studies, were carefully reviewed and selected from 258 submissions. The papers were organized in the following topical sections: Part I: automata and timed systems; security and hyperproperties; synthesis; model checking; cyber-physical systems and machine learning; probabilistic systems, runtime techniques; dynamical, hybrid, and reactive systems; Part II: logics, decision procedures; and solvers; numerical programs; verification; distributed systems and networks; verification and invariants; and concurrency.

ISBN: 9783030255404

Standard No.: 10.1007/978-3-030-25540-4doiSubjects--Topical Terms:

792454
Computer programs
--Verification--Congresses.

LC Class. No.: QA76.758 / .C38 2019

Dewey Class. No.: 005.1

Computer aided verification = 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019 : proceedings.. Part I /
LDR:04723nam a2200373 a 4500 001 941763
003 DE-He213
005 20190712192101.0
006 m d
007 cr nn 008maaau
008 200417s2019 gw s 0 eng d
020 $a 9783030255404 $q (electronic bk.)
020 $a 9783030255398 $q (paper)
024 7 $a 10.1007/978-3-030-25540-4 $2 doi
035 $a 978-3-030-25540-4
040 $a GP $c GP
041 0 $a eng
050 4 $a QA76.758 $b .C38 2019
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
090 $a QA76.758 $b .C376 2019
111 2 $a Workshop on the Preservation of Stability under Discretization $d (2001 : $c Fort Collins, Colo.) $3 527686
245 1 0 $a Computer aided verification $h [electronic resource] : $b 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019 : proceedings. $n Part I / $c edited by Isil Dillig, Serdar Tasiran.
246 3 $a CAV 2019
260 $a Cham : $c 2019. $b Springer International Publishing : $b Imprint: Springer,
300 $a xix, 673 p. : $b ill., digital ; $c 24 cm.
490 1 $a Lecture notes in computer science, $x 0302-9743 ; $v 11561
490 1 $a Theoretical computer science and general issues
505 0 $a Automata and Timed Systems -- Symbolic Register Automata -- Abstraction Refinement Algorithms for Timed Automata -- Fast Algorithms for Handling Diagonal Constraints in Timed Automata -- Safety and co-safety comparator automata for discounted-sum inclusion -- Clock Bound Repair for Timed Systems -- Verifying Asynchronous Interactions via Communicating Session Automata -- Security and Hyperproperties -- Verifying Hyperliveness -- Quantitative Mitigation of Timing Side Channels -- Property Directed Self Composition -- Security-Aware Synthesis Using Delayed-Action Games -- Automated Hypersafety Verification -- Automated Synthesis of Secure Platform Mappings -- Synthesis -- Synthesizing Approximate Implementations for Unrealizable Specifications -- Quantified Invariants via Syntax-Guided Synthesis -- Efficient Synthesis with Probabilistic Constraints -- Membership-based Synthesis of Linear Hybrid Automata -- Overfitting in Synthesis: Theory and Practice -- Proving Unrealizability for Syntax-Guided Synthesis -- Model Checking -- BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings -- When Human Intuition Fails: Using Formal Methods to Find an Error in the "Proof" of a Multi-Agent Protocol -- Extending NUXMV with Timed Transition Systems and Timed Temporal Properties -- Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C -- Cyber-physical Systems and Machine Learning -- Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification -- StreamLAB: Stream-based Monitoring of Cyber-Physical Systems -- VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems -- The Marabou Framework for Verification and Analysis of Deep Neural Networks -- Probabilistic Systems, Runtime Techniques -- Probabilistic Bisimulation for Parameterized Systems -- Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks -- PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games -- Symbolic Monitoring against Specifications Parametric in Time and Data -- STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis -- Dynamical, Hybrid, and Reactive Systems -- Local and Compositional Reasoning For Optimized Reactive Systems -- Robust Controller Synthesis in Timed Buchi Automata: A Symbolic Approach -- Flexible Computational Pipelines for Robust Abstraction-based Control Synthesis -- Temporal Stream Logic: Synthesis beyond the Bools -- Run-Time Optimization for Learned Controllers through Quantitative Games -- Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations.
506 $a Open access.
520 $a This open access two-volume set LNCS 11561 and 11562 constitutes the refereed proceedings of the 31st International Conference on Computer Aided Verification, CAV 2019, held in New York City, USA, in July 2019. The 52 full papers presented together with 13 tool papers and 2 case studies, were carefully reviewed and selected from 258 submissions. The papers were organized in the following topical sections: Part I: automata and timed systems; security and hyperproperties; synthesis; model checking; cyber-physical systems and machine learning; probabilistic systems, runtime techniques; dynamical, hybrid, and reactive systems; Part II: logics, decision procedures; and solvers; numerical programs; verification; distributed systems and networks; verification and invariants; and concurrency.
650 0 $a Computer programs $x Verification $v Congresses. $3 792454
650 0 $a Software engineering. $3 562952
650 0 $a Computer science. $3 573171
650 0 $a Information theory. $3 595305
650 0 $a Artificial intelligence. $3 559380
650 0 $a Computer simulation. $3 560190
650 0 $a Computer network architectures. $3 565372
650 1 4 $a Software Engineering. $3 669632
650 2 4 $a Programming Languages, Compilers, Interpreters. $3 669782
650 2 4 $a Theory of Computation. $3 669322
650 2 4 $a Artificial Intelligence. $3 646849
650 2 4 $a Simulation and Modeling. $3 669249
650 2 4 $a Computer Systems Organization and Communication Networks. $3 669309
700 1 $a Dillig, Isil. $3 1229173
700 1 $a Tasiran, Serdar. $3 1074167
710 2 $a SpringerLink (Online service) $3 593884
773 0 $t Springer eBooks
830 0 $a Lecture notes in computer science ; $v 6140. $3 744199
830 0 $a Theoretical computer science and general issues. $3 1208307
856 4 0 $u https://doi.org/10.1007/978-3-030-25540-4
950 $a Computer Science (Springer-11645)