Computer Aided Verification : : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / / edited by Isil Dillig, Serdar Tasiran.
The 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 careful...
Saved in:
Superior document: | Theoretical Computer Science and General Issues, 11562 |
---|---|
HerausgeberIn: | |
Place / Publishing House: | Cham : : Springer International Publishing :, Imprint: Springer,, 2019. |
Year of Publication: | 2019 |
Edition: | 1st ed. 2019. |
Language: | English |
Series: | Theoretical Computer Science and General Issues,
11562 |
Physical Description: | 1 online resource (XX, 549 p. 1209 illus., 42 illus. in color.) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
993543769804498 |
---|---|
ctrlnum |
(CKB)4100000008707563 (DE-He213)978-3-030-25543-5 (MiAaPQ)EBC5927086 (Au-PeEL)EBL5927086 (OCoLC)1132424096 (oapen)https://directory.doabooks.org/handle/20.500.12854/34409 (PPN)238488586 (EXLCZ)994100000008707563 |
collection |
bib_alma |
record_format |
marc |
spelling |
Dillig, Isil edt Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / edited by Isil Dillig, Serdar Tasiran. 1st ed. 2019. Cham : Springer International Publishing : Imprint: Springer, 2019. 1 online resource (XX, 549 p. 1209 illus., 42 illus. in color.) text txt rdacontent computer c rdamedia online resource cr rdacarrier Theoretical Computer Science and General Issues, 2512-2029 ; 11562 English Logics, Decision Procedures, and Solvers -- Satisfiability Checking for Mission-Time LTL -- High-Level Abstractions for Simplifying Extended String Constraints in SMT -- Alternating Automata Modulo First Order Theories -- Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors -- CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis -- Incremental Determinization for Quantifier Elimination and Functional Synthesis -- Numerical Programs -- Loop Summarization with Rational Vector Addition Systems -- Invertibility Conditions for Floating-Point Formulas -- Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems -- Icing: Supporting Fast-math Style Optimizations in a Verified Compiler -- Sound Approximation of Programs with Elementary Functions -- Verification -- Formal verification of quantum algorithms using quantum Hoare logic -- SecCSL: Security Concurrent Separation Logic -- Reachability Analysis for AWS-based Networks -- Distributed Systems and Networks -- Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics -- Gradual Consistency Checking -- Checking Robustness Against Snapshot Isolation -- Efficient verification of network fault tolerance via counterexampleguided refinement -- On the Complexity of Checking Consistency for Replicated Data Types -- Communication-closed asynchronous protocols -- Verification and Invariants -- Interpolating Strong Induction -- Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers -- Inferring Inductive Invariants from Phase Structures -- Termination of Triangular Integer Loops is Decidable -- AliveInLean: A Verified LLVM Peephole Optimization Verifier -- Concurrency -- Automated Parameterized Verification of CRDTs -- What's wrong with on-the-y partial order reduction -- Integrating Formal Schedulability Analysis into a Verifed OS Kernel -- Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS -- Violat: Generating Tests of Observational Refinement for Concurrent Objects. . The 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. . Open Access Software engineering. Computer science. Machine theory. Electronic digital computers—Evaluation. Computers. Professions. Logic programming. Software Engineering. Computer Science Logic and Foundations of Programming. Formal Languages and Automata Theory. System Performance and Evaluation. The Computing Profession. Logic in AI. 3-030-25542-5 Dillig, Isil. editor. edt http://id.loc.gov/vocabulary/relators/edt Tasiran, Serdar. editor. edt http://id.loc.gov/vocabulary/relators/edt |
language |
English |
format |
eBook |
author2 |
Dillig, Isil. Dillig, Isil. Tasiran, Serdar. Tasiran, Serdar. |
author_facet |
Dillig, Isil. Dillig, Isil. Tasiran, Serdar. Tasiran, Serdar. |
author2_variant |
i d id i d id i d id s t st s t st |
author2_role |
HerausgeberIn HerausgeberIn HerausgeberIn HerausgeberIn |
author_sort |
Dillig, Isil. |
title |
Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / |
spellingShingle |
Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / Theoretical Computer Science and General Issues, Logics, Decision Procedures, and Solvers -- Satisfiability Checking for Mission-Time LTL -- High-Level Abstractions for Simplifying Extended String Constraints in SMT -- Alternating Automata Modulo First Order Theories -- Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors -- CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis -- Incremental Determinization for Quantifier Elimination and Functional Synthesis -- Numerical Programs -- Loop Summarization with Rational Vector Addition Systems -- Invertibility Conditions for Floating-Point Formulas -- Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems -- Icing: Supporting Fast-math Style Optimizations in a Verified Compiler -- Sound Approximation of Programs with Elementary Functions -- Verification -- Formal verification of quantum algorithms using quantum Hoare logic -- SecCSL: Security Concurrent Separation Logic -- Reachability Analysis for AWS-based Networks -- Distributed Systems and Networks -- Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics -- Gradual Consistency Checking -- Checking Robustness Against Snapshot Isolation -- Efficient verification of network fault tolerance via counterexampleguided refinement -- On the Complexity of Checking Consistency for Replicated Data Types -- Communication-closed asynchronous protocols -- Verification and Invariants -- Interpolating Strong Induction -- Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers -- Inferring Inductive Invariants from Phase Structures -- Termination of Triangular Integer Loops is Decidable -- AliveInLean: A Verified LLVM Peephole Optimization Verifier -- Concurrency -- Automated Parameterized Verification of CRDTs -- What's wrong with on-the-y partial order reduction -- Integrating Formal Schedulability Analysis into a Verifed OS Kernel -- Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS -- Violat: Generating Tests of Observational Refinement for Concurrent Objects. . |
title_sub |
31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / |
title_full |
Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / edited by Isil Dillig, Serdar Tasiran. |
title_fullStr |
Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / edited by Isil Dillig, Serdar Tasiran. |
title_full_unstemmed |
Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / edited by Isil Dillig, Serdar Tasiran. |
title_auth |
Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / |
title_new |
Computer Aided Verification : |
title_sort |
computer aided verification : 31st international conference, cav 2019, new york city, ny, usa, july 15-18, 2019, proceedings, part ii / |
series |
Theoretical Computer Science and General Issues, |
series2 |
Theoretical Computer Science and General Issues, |
publisher |
Springer International Publishing : Imprint: Springer, |
publishDate |
2019 |
physical |
1 online resource (XX, 549 p. 1209 illus., 42 illus. in color.) |
edition |
1st ed. 2019. |
contents |
Logics, Decision Procedures, and Solvers -- Satisfiability Checking for Mission-Time LTL -- High-Level Abstractions for Simplifying Extended String Constraints in SMT -- Alternating Automata Modulo First Order Theories -- Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors -- CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis -- Incremental Determinization for Quantifier Elimination and Functional Synthesis -- Numerical Programs -- Loop Summarization with Rational Vector Addition Systems -- Invertibility Conditions for Floating-Point Formulas -- Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems -- Icing: Supporting Fast-math Style Optimizations in a Verified Compiler -- Sound Approximation of Programs with Elementary Functions -- Verification -- Formal verification of quantum algorithms using quantum Hoare logic -- SecCSL: Security Concurrent Separation Logic -- Reachability Analysis for AWS-based Networks -- Distributed Systems and Networks -- Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics -- Gradual Consistency Checking -- Checking Robustness Against Snapshot Isolation -- Efficient verification of network fault tolerance via counterexampleguided refinement -- On the Complexity of Checking Consistency for Replicated Data Types -- Communication-closed asynchronous protocols -- Verification and Invariants -- Interpolating Strong Induction -- Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers -- Inferring Inductive Invariants from Phase Structures -- Termination of Triangular Integer Loops is Decidable -- AliveInLean: A Verified LLVM Peephole Optimization Verifier -- Concurrency -- Automated Parameterized Verification of CRDTs -- What's wrong with on-the-y partial order reduction -- Integrating Formal Schedulability Analysis into a Verifed OS Kernel -- Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS -- Violat: Generating Tests of Observational Refinement for Concurrent Objects. . |
isbn |
3-030-25543-3 3-030-25542-5 |
issn |
2512-2029 ; |
callnumber-first |
Q - Science |
callnumber-subject |
QA - Mathematics |
callnumber-label |
QA76 |
callnumber-sort |
QA 276.758 |
illustrated |
Not Illustrated |
dewey-hundreds |
000 - Computer science, information & general works |
dewey-tens |
000 - Computer science, knowledge & systems |
dewey-ones |
005 - Computer programming, programs & data |
dewey-full |
005.1 |
dewey-sort |
15.1 |
dewey-raw |
005.1 |
dewey-search |
005.1 |
oclc_num |
1132424096 |
work_keys_str_mv |
AT dilligisil computeraidedverification31stinternationalconferencecav2019newyorkcitynyusajuly15182019proceedingspartii AT tasiranserdar computeraidedverification31stinternationalconferencecav2019newyorkcitynyusajuly15182019proceedingspartii |
status_str |
n |
ids_txt_mv |
(CKB)4100000008707563 (DE-He213)978-3-030-25543-5 (MiAaPQ)EBC5927086 (Au-PeEL)EBL5927086 (OCoLC)1132424096 (oapen)https://directory.doabooks.org/handle/20.500.12854/34409 (PPN)238488586 (EXLCZ)994100000008707563 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Theoretical Computer Science and General Issues, 11562 |
hierarchy_sequence |
11562 |
is_hierarchy_title |
Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / |
container_title |
Theoretical Computer Science and General Issues, 11562 |
author2_original_writing_str_mv |
noLinkedField noLinkedField noLinkedField noLinkedField |
_version_ |
1804715493452414976 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>05265nam a22006375i 4500</leader><controlfield tag="001">993543769804498</controlfield><controlfield tag="005">20230329193848.0</controlfield><controlfield tag="006">m o d | </controlfield><controlfield tag="007">cr nn 008mamaa</controlfield><controlfield tag="008">190712s2019 sz | o |||| 0|eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">3-030-25543-3</subfield></datafield><datafield tag="024" ind1="7" ind2=" "><subfield code="a">10.1007/978-3-030-25543-5</subfield><subfield code="2">doi</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(CKB)4100000008707563</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(DE-He213)978-3-030-25543-5</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(MiAaPQ)EBC5927086</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(Au-PeEL)EBL5927086</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(OCoLC)1132424096</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(oapen)https://directory.doabooks.org/handle/20.500.12854/34409</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(PPN)238488586</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(EXLCZ)994100000008707563</subfield></datafield><datafield tag="040" ind1=" " ind2=" "><subfield code="a">MiAaPQ</subfield><subfield code="b">eng</subfield><subfield code="e">rda</subfield><subfield code="e">pn</subfield><subfield code="c">MiAaPQ</subfield><subfield code="d">MiAaPQ</subfield></datafield><datafield tag="041" ind1="0" ind2=" "><subfield code="a">eng</subfield></datafield><datafield tag="050" ind1=" " ind2="4"><subfield code="a">QA76.758</subfield></datafield><datafield tag="072" ind1=" " ind2="7"><subfield code="a">UMZ</subfield><subfield code="2">bicssc</subfield></datafield><datafield tag="072" ind1=" " ind2="7"><subfield code="a">COM051230</subfield><subfield code="2">bisacsh</subfield></datafield><datafield tag="072" ind1=" " ind2="7"><subfield code="a">UMZ</subfield><subfield code="2">thema</subfield></datafield><datafield tag="082" ind1="0" ind2="4"><subfield code="a">005.1</subfield><subfield code="2">23</subfield></datafield><datafield tag="082" ind1=" " ind2=" "><subfield code="a">005.1</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Dillig, Isil</subfield><subfield code="4">edt</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">Computer Aided Verification :</subfield><subfield code="b">31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II /</subfield><subfield code="c">edited by Isil Dillig, Serdar Tasiran.</subfield></datafield><datafield tag="250" ind1=" " ind2=" "><subfield code="a">1st ed. 2019.</subfield></datafield><datafield tag="264" ind1=" " ind2="1"><subfield code="a">Cham :</subfield><subfield code="b">Springer International Publishing :</subfield><subfield code="b">Imprint: Springer,</subfield><subfield code="c">2019.</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (XX, 549 p. 1209 illus., 42 illus. in color.) </subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="490" ind1="1" ind2=" "><subfield code="a">Theoretical Computer Science and General Issues,</subfield><subfield code="x">2512-2029 ;</subfield><subfield code="v">11562</subfield></datafield><datafield tag="546" ind1=" " ind2=" "><subfield code="a">English</subfield></datafield><datafield tag="505" ind1="0" ind2=" "><subfield code="a">Logics, Decision Procedures, and Solvers -- Satisfiability Checking for Mission-Time LTL -- High-Level Abstractions for Simplifying Extended String Constraints in SMT -- Alternating Automata Modulo First Order Theories -- Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors -- CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis -- Incremental Determinization for Quantifier Elimination and Functional Synthesis -- Numerical Programs -- Loop Summarization with Rational Vector Addition Systems -- Invertibility Conditions for Floating-Point Formulas -- Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems -- Icing: Supporting Fast-math Style Optimizations in a Verified Compiler -- Sound Approximation of Programs with Elementary Functions -- Verification -- Formal verification of quantum algorithms using quantum Hoare logic -- SecCSL: Security Concurrent Separation Logic -- Reachability Analysis for AWS-based Networks -- Distributed Systems and Networks -- Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics -- Gradual Consistency Checking -- Checking Robustness Against Snapshot Isolation -- Efficient verification of network fault tolerance via counterexampleguided refinement -- On the Complexity of Checking Consistency for Replicated Data Types -- Communication-closed asynchronous protocols -- Verification and Invariants -- Interpolating Strong Induction -- Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers -- Inferring Inductive Invariants from Phase Structures -- Termination of Triangular Integer Loops is Decidable -- AliveInLean: A Verified LLVM Peephole Optimization Verifier -- Concurrency -- Automated Parameterized Verification of CRDTs -- What's wrong with on-the-y partial order reduction -- Integrating Formal Schedulability Analysis into a Verifed OS Kernel -- Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS -- Violat: Generating Tests of Observational Refinement for Concurrent Objects. .</subfield></datafield><datafield tag="520" ind1=" " ind2=" "><subfield code="a">The 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. .</subfield></datafield><datafield tag="506" ind1="0" ind2=" "><subfield code="a">Open Access</subfield></datafield><datafield tag="650" ind1=" " ind2="0"><subfield code="a">Software engineering.</subfield></datafield><datafield tag="650" ind1=" " ind2="0"><subfield code="a">Computer science.</subfield></datafield><datafield tag="650" ind1=" " ind2="0"><subfield code="a">Machine theory.</subfield></datafield><datafield tag="650" ind1=" " ind2="0"><subfield code="a">Electronic digital computers—Evaluation.</subfield></datafield><datafield tag="650" ind1=" " ind2="0"><subfield code="a">Computers.</subfield></datafield><datafield tag="650" ind1=" " ind2="0"><subfield code="a">Professions.</subfield></datafield><datafield tag="650" ind1=" " ind2="0"><subfield code="a">Logic programming.</subfield></datafield><datafield tag="650" ind1="1" ind2="4"><subfield code="a">Software Engineering.</subfield></datafield><datafield tag="650" ind1="2" ind2="4"><subfield code="a">Computer Science Logic and Foundations of Programming.</subfield></datafield><datafield tag="650" ind1="2" ind2="4"><subfield code="a">Formal Languages and Automata Theory.</subfield></datafield><datafield tag="650" ind1="2" ind2="4"><subfield code="a">System Performance and Evaluation.</subfield></datafield><datafield tag="650" ind1="2" ind2="4"><subfield code="a">The Computing Profession.</subfield></datafield><datafield tag="650" ind1="2" ind2="4"><subfield code="a">Logic in AI.</subfield></datafield><datafield tag="776" ind1=" " ind2=" "><subfield code="z">3-030-25542-5</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Dillig, Isil.</subfield><subfield code="e">editor.</subfield><subfield code="4">edt</subfield><subfield code="4">http://id.loc.gov/vocabulary/relators/edt</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Tasiran, Serdar.</subfield><subfield code="e">editor.</subfield><subfield code="4">edt</subfield><subfield code="4">http://id.loc.gov/vocabulary/relators/edt</subfield></datafield><datafield tag="830" ind1=" " ind2="0"><subfield code="a">Theoretical Computer Science and General Issues,</subfield><subfield code="x">2512-2029 ;</subfield><subfield code="v">11562</subfield></datafield><datafield tag="906" ind1=" " ind2=" "><subfield code="a">BOOK</subfield></datafield><datafield tag="ADM" ind1=" " ind2=" "><subfield code="b">2024-07-16 07:52:59 Europe/Vienna</subfield><subfield code="f">system</subfield><subfield code="c">marc21</subfield><subfield code="a">2019-07-17 01:51:25 Europe/Vienna</subfield><subfield code="g">false</subfield></datafield><datafield tag="AVE" ind1=" " ind2=" "><subfield code="i">DOAB Directory of Open Access Books</subfield><subfield code="P">DOAB Directory of Open Access Books</subfield><subfield code="x">https://eu02.alma.exlibrisgroup.com/view/uresolver/43ACC_OEAW/openurl?u.ignore_date_coverage=true&portfolio_pid=5337423500004498&Force_direct=true</subfield><subfield code="Z">5337423500004498</subfield><subfield code="b">Available</subfield><subfield code="8">5337423500004498</subfield></datafield></record></collection> |