دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: [1st ed.]
نویسندگان: Isil Dillig. Serdar Tasiran
سری: Lecture Notes in Computer Science 11562
ISBN (شابک) : 9783030255428
ناشر: Springer International Publishing
سال نشر: 2019
تعداد صفحات: XX, 549
[558]
زبان: English
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود)
حجم فایل: 20 Mb
در صورت ایرانی بودن نویسنده امکان دانلود وجود ندارد و مبلغ عودت داده خواهد شد
در صورت تبدیل فایل کتاب Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب تأیید به کمک رایانه: سی و یکمین کنفرانس بین المللی، CAV 2019، شهر نیویورک، نیویورک، ایالات متحده آمریکا، 15-18 ژوئیه، 2019، مجموعه مقالات، قسمت دوم نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
مجموعه دو جلدی دسترسی آزاد LNCS 11561 و 11562، مجموعه مقالات داوری سی و یکمین کنفرانس بین المللی تأیید به کمک رایانه، CAV 2019، که در شهر نیویورک، ایالات متحده آمریکا، در ژوئیه 2019 برگزار شد. 52 مقاله کامل همراه با 13 مقاله ابزار ارائه شده است. و 2 مطالعه موردی، به دقت بررسی و از بین 258 مورد ارسالی انتخاب شدند. مقالات در بخشهای موضوعی زیر سازماندهی شدند: بخش اول: سیستمهای خودکار و زمانبندیشده. امنیت و خواص فوق العاده; سنتز؛ بررسی مدل؛ سیستم های فیزیکی-سایبری و یادگیری ماشینی؛ سیستم های احتمالی، تکنیک های زمان اجرا. سیستم های دینامیکی، هیبریدی و واکنشی؛ بخش دوم: منطق، رویه های تصمیم گیری. و حل کننده ها برنامه های عددی؛ تایید؛ سیستم ها و شبکه های توزیع شده؛ تأیید و غیر متغیرها؛ و همزمانی
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.
Front Matter ....Pages i-xx
Front Matter ....Pages 1-1
Satisfiability Checking for Mission-Time LTL (Jianwen Li, Moshe Y. Vardi, Kristin Y. Rozier)....Pages 3-22
High-Level Abstractions for Simplifying Extended String Constraints in SMT (Andrew Reynolds, Andres Nötzli, Clark Barrett, Cesare Tinelli)....Pages 23-42
Alternating Automata Modulo First Order Theories (Radu Iosif, Xiao Xu)....Pages 43-63
Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors (Martin Jonáš, Jan Strejček)....Pages 64-73
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis (Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett, Cesare Tinelli)....Pages 74-83
Incremental Determinization for Quantifier Elimination and Functional Synthesis (Markus N. Rabe)....Pages 84-94
Front Matter ....Pages 95-95
Loop Summarization with Rational Vector Addition Systems (Jake Silverman, Zachary Kincaid)....Pages 97-115
Invertibility Conditions for Floating-Point Formulas (Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli)....Pages 116-136
Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems (Sicun Gao, James Kapinski, Jyotirmoy Deshmukh, Nima Roohi, Armando Solar-Lezama, Nikos Arechiga et al.)....Pages 137-154
Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler (Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock)....Pages 155-173
Sound Approximation of Programs with Elementary Functions (Eva Darulova, Anastasia Volkova)....Pages 174-183
Front Matter ....Pages 185-185
Formal Verification of Quantum Algorithms Using Quantum Hoare Logic (Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li et al.)....Pages 187-207
SecCSL: Security Concurrent Separation Logic (Gidon Ernst, Toby Murray)....Pages 208-230
Reachability Analysis for AWS-Based Networks (John Backes, Sam Bayless, Byron Cook, Catherine Dodge, Andrew Gacek, Alan J. Hu et al.)....Pages 231-241
Front Matter ....Pages 243-243
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics (Idan Berkovits, Marijana Lazić, Giuliano Losa, Oded Padon, Sharon Shoham)....Pages 245-266
Gradual Consistency Checking (Rachid Zennou, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi)....Pages 267-285
Checking Robustness Against Snapshot Isolation (Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea)....Pages 286-304
Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement (Nick Giannarakis, Ryan Beckett, Ratul Mahajan, David Walker)....Pages 305-323
On the Complexity of Checking Consistency for Replicated Data Types (Ranadeep Biswas, Michael Emmi, Constantin Enea)....Pages 324-343
Communication-Closed Asynchronous Protocols (Andrei Damian, Cezara Drăgoi, Alexandru Militaru, Josef Widder)....Pages 344-363
Front Matter ....Pages 365-365
Interpolating Strong Induction (Hari Govind Vediramana Krishnan, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel)....Pages 367-385
Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (Peizun Liu, Thomas Wahl, Akash Lal)....Pages 386-404
Inferring Inductive Invariants from Phase Structures (Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv)....Pages 405-425
Termination of Triangular Integer Loops is Decidable (Florian Frohn, Jürgen Giesl)....Pages 426-444
AliveInLean: A Verified LLVM Peephole Optimization Verifier (Juneyoung Lee, Chung-Kil Hur, Nuno P. Lopes)....Pages 445-455
Front Matter ....Pages 457-457
Automated Parameterized Verification of CRDTs (Kartik Nagar, Suresh Jagannathan)....Pages 459-477
What’s Wrong with On-the-Fly Partial Order Reduction (Stephen F. Siegel)....Pages 478-495
Integrating Formal Schedulability Analysis into a Verified OS Kernel (Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, Zhong Shao)....Pages 496-514
Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS (Yongwang Zhao, David Sanán)....Pages 515-533
Violat: Generating Tests of Observational Refinement for Concurrent Objects (Michael Emmi, Constantin Enea)....Pages 534-546
Back Matter ....Pages 547-549