國立虎尾科技大學 |

Verification, Model Checking, and Abstract Interpretation = 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021, Proceedings /

紀錄類型:	書目-語言資料,印刷品 : Monograph/item
正題名/作者:	Verification, Model Checking, and Abstract Interpretation/ edited by Fritz Henglein, Sharon Shoham, Yakir Vizel.
其他題名:	22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021, Proceedings /
其他作者:	Vizel, Yakir.
面頁冊數:	XV, 604 p. 212 illus., 108 illus. in color.online resource. :
Contained By:	Springer Nature eBook
標題:	Special Purpose and Application-Based Systems. -
電子資源:	https://doi.org/10.1007/978-3-030-67067-2
ISBN:	9783030670672

Verification, Model Checking, and Abstract Interpretation = 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021, Proceedings /
Verification, Model Checking, and Abstract Interpretation22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021, Proceedings /[electronic resource] :edited by Fritz Henglein, Sharon Shoham, Yakir Vizel. - 1st ed. 2021. - XV, 604 p. 212 illus., 108 illus. in color.online resource. - Theoretical Computer Science and General Issues ;12597. - Theoretical Computer Science and General Issues ;9163.

Invited Papers -- Model Checking Algorithms for Hyperproperties -- Algebra-based Synthesis of Loops and their Invariants -- Generative Program Analysis and Beyond: The Power of Domain-Specific Languages -- Hyperproperties and Infinite-state Systems -- Compositional Model Checking for Multi-Properties -- Decomposing Data Structure Commutativity Proofs with mn-Differencing -- Proving the existence of fair paths in infinite-state systems -- A Self-Certifying Compilation Framework for WebAssembly -- Concurrent and Distributed Systems -- Concurrent Correctness in Vector Space -- Verification of Concurrent Programs Using Petri Net Unfoldings -- Eliminating Message Counters in Synchronous Threshold Automata -- A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries -- Checking -- Runtime Abstract Interpretation for Numerical Accuracy and Robustness -- Twinning automata and regular expressions for string static analysis -- Unbounded Procedure Summaries from Bounded Environments -- Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking -- Synthesis and Repair -- Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible -- Automated Repair of Heap-Manipulating Programs using Deductive Synthesis -- GPURepair: Automated Repair of GPU Kernels -- Applications -- A Synchronous Effects Logic for Temporal Verification of Pure Esterel -- A Design of GPU-Based Quantitative Model Checking -- Formal Semantics and Verification of Network Based Biocomputation Circuits -- Netter: Probabilistic, Stateful Network Models,. Decision Procedures -- Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories -- Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching -- On Preprocessing for Weighted MaxSAT -- Compositional Satisfiability Solving in Separation Logic.

This book constitutes the proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021, which was held virtually during January 17-19, 2021. The conference was planned to take place in Copenhagen, Denmark, but changed to an online event due to the COVID-19 pandemic. The 23 papers presented in this volume were carefully reviewed from 48 submissions. VMCAI provides a forum for researchers working on verification, model checking, and abstract interpretation and facilitates interaction, cross-fertilization, and advancement of hybrid methods that combine these and related areas. The papers presented in this volume were organized in the following topical sections: hyperproperties and infinite-state systems; concurrent and distributed systems; checking; synthesis and repair; applications; and decision procedures. .

ISBN: 9783030670672

Standard No.: 10.1007/978-3-030-67067-2doiSubjects--Topical Terms:

669833
Special Purpose and Application-Based Systems.

LC Class. No.: QA75.5-76.95

Dewey Class. No.: 004.0151

Verification, Model Checking, and Abstract Interpretation = 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021, Proceedings /
LDR:04399nam a22004335i 4500 001 1051818
003 DE-He213
005 20210826172140.0
007 cr nn 008mamaa
008 220103s2021 sz | s |||| 0|eng d
020 $a 9783030670672 $9 978-3-030-67067-2
024 7 $a 10.1007/978-3-030-67067-2 $2 doi
035 $a 978-3-030-67067-2
050 4 $a QA75.5-76.95
050 4 $a QA76.63
072 7 $a UY $2 bicssc
072 7 $a COM014000 $2 bisacsh
072 7 $a UY $2 thema
072 7 $a UYA $2 thema
082 0 4 $a 004.0151 $2 23
245 1 0 $a Verification, Model Checking, and Abstract Interpretation $h [electronic resource] : $b 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021, Proceedings / $c edited by Fritz Henglein, Sharon Shoham, Yakir Vizel.
250 $a 1st ed. 2021.
264 1 $a Cham : $b Springer International Publishing : $b Imprint: Springer, $c 2021.
300 $a XV, 604 p. 212 illus., 108 illus. in color. $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 12597
505 0 $a Invited Papers -- Model Checking Algorithms for Hyperproperties -- Algebra-based Synthesis of Loops and their Invariants -- Generative Program Analysis and Beyond: The Power of Domain-Specific Languages -- Hyperproperties and Infinite-state Systems -- Compositional Model Checking for Multi-Properties -- Decomposing Data Structure Commutativity Proofs with mn-Differencing -- Proving the existence of fair paths in infinite-state systems -- A Self-Certifying Compilation Framework for WebAssembly -- Concurrent and Distributed Systems -- Concurrent Correctness in Vector Space -- Verification of Concurrent Programs Using Petri Net Unfoldings -- Eliminating Message Counters in Synchronous Threshold Automata -- A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries -- Checking -- Runtime Abstract Interpretation for Numerical Accuracy and Robustness -- Twinning automata and regular expressions for string static analysis -- Unbounded Procedure Summaries from Bounded Environments -- Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking -- Synthesis and Repair -- Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible -- Automated Repair of Heap-Manipulating Programs using Deductive Synthesis -- GPURepair: Automated Repair of GPU Kernels -- Applications -- A Synchronous Effects Logic for Temporal Verification of Pure Esterel -- A Design of GPU-Based Quantitative Model Checking -- Formal Semantics and Verification of Network Based Biocomputation Circuits -- Netter: Probabilistic, Stateful Network Models,. Decision Procedures -- Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories -- Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching -- On Preprocessing for Weighted MaxSAT -- Compositional Satisfiability Solving in Separation Logic.
520 $a This book constitutes the proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021, which was held virtually during January 17-19, 2021. The conference was planned to take place in Copenhagen, Denmark, but changed to an online event due to the COVID-19 pandemic. The 23 papers presented in this volume were carefully reviewed from 48 submissions. VMCAI provides a forum for researchers working on verification, model checking, and abstract interpretation and facilitates interaction, cross-fertilization, and advancement of hybrid methods that combine these and related areas. The papers presented in this volume were organized in the following topical sections: hyperproperties and infinite-state systems; concurrent and distributed systems; checking; synthesis and repair; applications; and decision procedures. .
650 2 4 $a Special Purpose and Application-Based Systems. $3 669833
650 2 4 $a Control Structures and Microprogramming. $3 669788
650 2 4 $a Software Engineering. $3 669632
650 2 4 $a Natural Language Processing (NLP). $3 1254293
650 1 4 $a Theory of Computation. $3 669322
650 0 $a Special purpose computers. $3 1204562
650 0 $a Microprogramming . $3 1257366
650 0 $a Software engineering. $3 562952
650 0 $a Natural language processing (Computer science). $3 802180
650 0 $a Computers. $3 565115
700 1 $a Vizel, Yakir. $e editor. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 1356396
700 1 $a Shoham, Sharon. $e editor. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 1356395
700 1 $a Henglein, Fritz. $e editor. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 1356394
710 2 $a SpringerLink (Online service) $3 593884
773 0 $t Springer Nature eBook
776 0 8 $i Printed edition: $z 9783030670665
776 0 8 $i Printed edition: $z 9783030670689
830 0 $a Theoretical Computer Science and General Issues ; $v 9163 $3 1253524
856 4 0 $u https://doi.org/10.1007/978-3-030-67067-2
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)