دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
دانلود کتاب Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings
دانلود کتاب اثبات قضیه تعاملی: سومین کنفرانس بین المللی، ITP 2012، پرینستون، نیوجرسی، ایالات متحده آمریکا، 13-15 اوت 2012. مجموعه مقالات
مشخصات کتاب
Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings
ویرایش: 1 نویسندگان: Lawrence C. Paulson (auth.), Lennart Beringer, Amy Felty (eds.) سری: Lecture Notes in Computer Science 7406 ISBN (شابک) : 9783642323461, 9783642323478 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 2012 تعداد صفحات: 428 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 7 مگابایت
قیمت کتاب (تومان) : 33,000
کلمات کلیدی مربوط به کتاب اثبات قضیه تعاملی: سومین کنفرانس بین المللی، ITP 2012، پرینستون، نیوجرسی، ایالات متحده آمریکا، 13-15 اوت 2012. مجموعه مقالات: منطق ریاضی و زبان های رسمی، هوش مصنوعی (شامل رباتیک)، منطق و معانی برنامه ها، مهندسی نرم افزار، سیستم ها و امنیت داده ها، محاسبات با دستگاه های انتزاعی
در صورت تبدیل فایل کتاب Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب اثبات قضیه تعاملی: سومین کنفرانس بین المللی، ITP 2012، پرینستون، نیوجرسی، ایالات متحده آمریکا، 13-15 اوت 2012. مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
توضیحاتی در مورد کتاب اثبات قضیه تعاملی: سومین کنفرانس بین المللی، ITP 2012، پرینستون، نیوجرسی، ایالات متحده آمریکا، 13-15 اوت 2012. مجموعه مقالات
این کتاب مجموعه مقالات کامل داوری شده سومین کنفرانس بین المللی اثبات قضیه تعاملی، ITP 2012، برگزار شده در پرینستون، نیوجرسی، ایالات متحده آمریکا، در آگوست 2012 است. گفتگوها و یک آموزش دعوت شده به دقت بررسی و از بین 40 مورد ارسالی انتخاب شد. از جمله موضوعات تحت پوشش رسمی سازی ریاضیات است. انتزاع برنامه و منطق. ساختار داده و سنتز؛ امنیت؛ (غیر) خاتمه و خودکار. تایید برنامه؛ قضیه اثبات توسعه; استدلال در مورد اجرای برنامه؛ و زیرساخت ها و سبک های مدل سازی را ارائه کنید.
توضیحاتی درمورد کتاب به خارجی
This book constitutes the thoroughly refereed proceedings of the Third International Conference on Interactive Theorem Proving, ITP 2012, held in Princeton, NJ, USA, in August 2012. The 21 revised full papers presented together with 4 rough diamond papers, 3 invited talks, and one invited tutorial were carefully reviewed and selected from 40 submissions. Among the topics covered are formalization of mathematics; program abstraction and logics; data structures and synthesis; security; (non-)termination and automata; program verification; theorem prover development; reasoning about program execution; and prover infrastructure and modeling styles.
فهرست مطالب
Front Matter....Pages -
MetiTarski: Past and Future....Pages 1-10
Computer-Aided Cryptographic Proofs....Pages 11-27
A Differential Operator Approach to Equational Differential Invariants....Pages 28-48
Abella: A Tutorial....Pages 49-50
A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers....Pages 51-66
Construction of Real Algebraic Numbers in C oq ....Pages 67-82
A Refinement-Based Approach to Computational Algebra in Coq ....Pages 83-98
Bridging the Gap: Automatic Verified Abstraction of C....Pages 99-115
Abstract Interpretation of Annotated Commands....Pages 116-132
Verifying and Generating WP Transformers for Procedures on Complex Data....Pages 133-148
Bag Equivalence via a Proof-Relevant Membership Relation....Pages 149-165
Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm....Pages 166-182
Synthesis of Distributed Mobile Programs Using Monadic Types in Coq....Pages 183-200
Towards Provably Robust Watermarking....Pages 201-216
Priority Inheritance Protocol Proved Correct....Pages 217-232
Formalization of Shannon’s Theorems in SSReflect-Coq....Pages 233-249
Stop When You Are Almost-Full....Pages 250-265
Certification of Nontermination Proofs....Pages 266-282
A Compact Proof of Decidability for Regular Expression Equivalence....Pages 283-298
Using Locales to Define a Rely-Guarantee Temporal Logic....Pages 299-314
Charge!....Pages 315-331
Mechanised Separation Algebra....Pages 332-337
Directions in ISA Specification....Pages 338-344
More SPASS with Isabelle....Pages 345-360
A Language of Patterns for Subterm Selection....Pages 361-376
Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL....Pages 377-392
Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem....Pages 393-404
Standalone Tactics Using OpenTheory....Pages 405-411
Functional Programs: Conversions between Deep and Shallow Embeddings....Pages 412-417
Back Matter....Pages -
