دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: 1 نویسندگان: Greg Morrisett (auth.), Chris Hawblitzel, Dale Miller (eds.) سری: Lecture Notes in Computer Science 7679 Theoretical Computer Science and General Issues ISBN (شابک) : 9783642353079, 9783642353086 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 2012 تعداد صفحات: 313 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 4 مگابایت
کلمات کلیدی مربوط به کتاب برنامه ها و اثبات های مجاز: دومین کنفرانس بین المللی ، CPP 2012 ، کیوتو ، ژاپن ، 13-15 دسامبر ، 2012. مجموعه مقالات: منطق و معانی برنامه ها، منطق ریاضی و زبان های رسمی، زبان های برنامه نویسی، کامپایلر، مفسر، دستکاری نمادین و جبری، مهندسی نرم افزار، هوش مصنوعی (شامل رباتیک)
در صورت تبدیل فایل کتاب Certified Programs and Proofs: Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب برنامه ها و اثبات های مجاز: دومین کنفرانس بین المللی ، CPP 2012 ، کیوتو ، ژاپن ، 13-15 دسامبر ، 2012. مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
این کتاب مجموعه مقالات داوری دومین کنفرانس بینالمللی برنامهها و شواهد گواهی شده، CPP 2012، که در کیوتو، ژاپن، در دسامبر 2012 برگزار شد، تشکیل میشود. آنها به موضوعاتی در علوم کامپیوتر و ریاضیات می پردازند که در آنها صدور گواهینامه از طریق تکنیک های رسمی بسیار مهم است.
This book constitutes the refereed proceedings of the Second International Conference on Certified Programs and Proofs, CPP 2012, held in Kyoto, Japan, in December 2012. The 18 revised regular papers presented were carefully reviewed and selected from 37 submissions. They deal with those topics in computer science and mathematics in which certification via formal techniques is crucial.
Front Matter....Pages -
Scalable Formal Machine Models....Pages 1-3
Mechanized Semantics for Compiler Verification....Pages 4-6
Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs....Pages 7-8
Program Certification by Higher-Order Model Checking....Pages 9-10
A Formally-Verified Alias Analysis....Pages 11-26
Mechanized Verification of Computing Dominators for Formalizing Compilers....Pages 27-42
On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor....Pages 43-59
An Executable Semantics for CompCert C....Pages 60-75
Producing Certified Functional Code from Inductive Specifications....Pages 76-91
The New Quickcheck for Isabelle....Pages 92-108
Proving Concurrent Noninterference....Pages 109-125
Noninterference for Operating System Kernels....Pages 126-142
Compositional Verification of a Baby Virtual Memory Manager....Pages 143-159
Shall We Juggle, Coinductively?....Pages 160-172
Proof Pearl: Abella Formalization of λ -Calculus Cube Property....Pages 173-187
A String of Pearls: Proofs of Fermat’s Little Theorem....Pages 188-207
Compact Proof Certificates for Linear Logic....Pages 208-223
Constructive Completeness for Modal Logic with Transitive Closure....Pages 224-239
Rating Disambiguation Errors....Pages 240-255
A Formal Proof of Square Root and Division Elimination in Embedded Programs....Pages 256-272
Coherent and Strongly Discrete Rings in Type Theory....Pages 273-288
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives....Pages 289-304
Back Matter....Pages -