國立虎尾科技大學 |

Automated Technology for Verification and Analysis = 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021, Proceedings /

紀錄類型:	書目-語言資料,印刷品 : Monograph/item
正題名/作者:	Automated Technology for Verification and Analysis/ edited by Zhe Hou, Vijay Ganesh.
其他題名:	19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021, Proceedings /
其他作者:	Hou, Zhe.
面頁冊數:	XV, 382 p. 103 illus., 49 illus. in color.online resource. :
Contained By:	Springer Nature eBook
標題:	Software engineering. -
電子資源:	https://doi.org/10.1007/978-3-030-88885-5
ISBN:	9783030888855

Automated Technology for Verification and Analysis = 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021, Proceedings /
Automated Technology for Verification and Analysis19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021, Proceedings /[electronic resource] :edited by Zhe Hou, Vijay Ganesh. - 1st ed. 2021. - XV, 382 p. 103 illus., 49 illus. in color.online resource. - Programming and Software Engineering,129712945-9168 ;. - Programming and Software Engineering,12857.

Invited Paper -- Linear Temporal Logic – From Infinite to Finite Horizon -- Automata Theory -- Determinization and Limit-determinization of Emerson-Lei automata -- Automatic discovery of fair paths in infinite-state transition systems -- Certifying DFA Bounds for Recognition and Separation -- Machine Learning for Formal Methods -- AALpy: An Active Automata Learning Library -- Learning Linear Temporal Properties from Noisy Data: A MaxSAT-based Approach -- Mining Interpretable Spatio-temporal Logic Properties for Spatially Distributed Systems -- Theorem Proving and Tools -- A Formal Semantics of the GraalVM Intermediate Representation -- A Verified Decision Procedure for Orders in Isabelle/HOL -- PJBDD: A BDD Library for Java and Multi-Threading -- Model Checking -- Live Synthesis -- Faster Pushdown Reachability Analysis with Applications in Network Verification -- Verifying Verified Code -- Probabilistic Analysis -- Probabilistic causes in Markov Chains -- TEMPEST - Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments -- AQUA: Automated Quantized Inference for Probabilistic Programs -- Software and Hardware Verification -- Proving SIFA Protection of Masked Redundant Circuits -- Verification by Gambling on Program Slices -- Runtime Enforcement of Hyperproperties -- System Synthesis and Approximation -- Compositional Synthesis of Modular Systems -- Event-B Refinement for Continuous Behaviours Approximation -- Incorporating Monitors in Reactive Synthesis without Paying the Price -- Verification of Machine Learning -- pyNever: a Framework for Learning and Verification of Neural Networks -- Property-Directed Verification and Robustness Certification of Recurrent Neural Networks.

This book constitutes the refereed proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021, held in Gold Coast, Australia in October 2021. The symposium is dedicated to promoting research in theoretical and practical aspects of automated analysis, verification and synthesis by providing an international venue for the researchers to present new results. The 19 regular papers presented together with 4 tool papers and 1 invited paper were carefully reviewed and selected from 75 submissions. The papers are divided into the following topical sub-headings: Automata Theory; Machine learning for Formal Methods; Theorem Proving and Tools; Model Checking; Probabilistic Analysis; Software and Hardware Verification; System Synthesis and Approximation; and Verification of Machine Learning.

ISBN: 9783030888855

Standard No.: 10.1007/978-3-030-88885-5doiSubjects--Topical Terms:

562952
Software engineering.

LC Class. No.: QA76.758

Dewey Class. No.: 005.1

Automated Technology for Verification and Analysis = 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021, Proceedings /
LDR:04085nam a22004095i 4500 001 1059381
003 DE-He213
005 20220311183623.0
007 cr nn 008mamaa
008 220414s2021 sz | s |||| 0|eng d
020 $a 9783030888855 $9 978-3-030-88885-5
024 7 $a 10.1007/978-3-030-88885-5 $2 doi
035 $a 978-3-030-88885-5
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 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021, Proceedings / $c edited by Zhe Hou, Vijay Ganesh.
250 $a 1st ed. 2021.
264 1 $a Cham : $b Springer International Publishing : $b Imprint: Springer, $c 2021.
300 $a XV, 382 p. 103 illus., 49 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 Programming and Software Engineering, $x 2945-9168 ; $v 12971
505 0 $a Invited Paper -- Linear Temporal Logic – From Infinite to Finite Horizon -- Automata Theory -- Determinization and Limit-determinization of Emerson-Lei automata -- Automatic discovery of fair paths in infinite-state transition systems -- Certifying DFA Bounds for Recognition and Separation -- Machine Learning for Formal Methods -- AALpy: An Active Automata Learning Library -- Learning Linear Temporal Properties from Noisy Data: A MaxSAT-based Approach -- Mining Interpretable Spatio-temporal Logic Properties for Spatially Distributed Systems -- Theorem Proving and Tools -- A Formal Semantics of the GraalVM Intermediate Representation -- A Verified Decision Procedure for Orders in Isabelle/HOL -- PJBDD: A BDD Library for Java and Multi-Threading -- Model Checking -- Live Synthesis -- Faster Pushdown Reachability Analysis with Applications in Network Verification -- Verifying Verified Code -- Probabilistic Analysis -- Probabilistic causes in Markov Chains -- TEMPEST - Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments -- AQUA: Automated Quantized Inference for Probabilistic Programs -- Software and Hardware Verification -- Proving SIFA Protection of Masked Redundant Circuits -- Verification by Gambling on Program Slices -- Runtime Enforcement of Hyperproperties -- System Synthesis and Approximation -- Compositional Synthesis of Modular Systems -- Event-B Refinement for Continuous Behaviours Approximation -- Incorporating Monitors in Reactive Synthesis without Paying the Price -- Verification of Machine Learning -- pyNever: a Framework for Learning and Verification of Neural Networks -- Property-Directed Verification and Robustness Certification of Recurrent Neural Networks.
520 $a This book constitutes the refereed proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021, held in Gold Coast, Australia in October 2021. The symposium is dedicated to promoting research in theoretical and practical aspects of automated analysis, verification and synthesis by providing an international venue for the researchers to present new results. The 19 regular papers presented together with 4 tool papers and 1 invited paper were carefully reviewed and selected from 75 submissions. The papers are divided into the following topical sub-headings: Automata Theory; Machine learning for Formal Methods; Theorem Proving and Tools; Model Checking; Probabilistic Analysis; Software and Hardware Verification; System Synthesis and Approximation; and Verification of Machine Learning.
650 0 $a Software engineering. $3 562952
650 0 $a Artificial intelligence. $3 559380
650 0 $a Computers. $3 565115
650 0 $a Computer engineering. $3 569006
650 0 $a Computer networks . $3 1365720
650 1 4 $a Software Engineering. $3 669632
650 2 4 $a Artificial Intelligence. $3 646849
650 2 4 $a Computer Hardware. $3 669779
650 2 4 $a Computer Engineering and Networks. $3 1365733
700 1 $a Hou, Zhe. $e editor. $1 https://orcid.org/0000-0001-7164-0580 $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 1327956
700 1 $a Ganesh, Vijay. $e editor. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 1361404
710 2 $a SpringerLink (Online service) $3 593884
773 0 $t Springer Nature eBook
776 0 8 $i Printed edition: $z 9783030888848
776 0 8 $i Printed edition: $z 9783030888862
830 0 $a Programming and Software Engineering, $x 2945-9168 ; $v 12857 $3 1365731
856 4 0 $u https://doi.org/10.1007/978-3-030-88885-5
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)