دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: 1 نویسندگان: Wolfgang Paul (auth.), Rajeev Joshi, Peter Müller, Andreas Podelski (eds.) سری: Lecture Notes in Computer Science 7152 ISBN (شابک) : 9783642277047, 9783642277054 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 2012 تعداد صفحات: 335 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 6 مگابایت
کلمات کلیدی مربوط به کتاب نرم افزار تأیید شده: نظریه ها ، ابزارها ، آزمایشات: چهارمین کنفرانس بین المللی ، VSTTE 2012 ، فیلادلفیا ، پنسیلوانیا ، ایالات متحده آمریکا ، 28 تا 29 ژانویه 2012. مجموعه مقالات: مهندسی نرم افزار، منطق و معانی برنامه ها، زبان های برنامه نویسی، کامپایلرها، مترجمان، تکنیک های برنامه نویسی، منطق ریاضی و زبان های رسمی، هوش مصنوعی (شامل رباتیک)
در صورت تبدیل فایل کتاب Verified Software: Theories, Tools, Experiments: 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب نرم افزار تأیید شده: نظریه ها ، ابزارها ، آزمایشات: چهارمین کنفرانس بین المللی ، VSTTE 2012 ، فیلادلفیا ، پنسیلوانیا ، ایالات متحده آمریکا ، 28 تا 29 ژانویه 2012. مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
این جلد شامل مجموعه مقالات چهارمین کنفرانس بینالمللی نرمافزار تایید شده: نظریهها، ابزارها و آزمایشها، VSTTE 2012 است که در فیلادلفیا، PA، ایالات متحده آمریکا، در ژانویه 2012 برگزار شد. و 2 آموزش با دقت اصلاح و از بین 54 مورد ارسالی اولیه برای گنجاندن در کتاب انتخاب شدند. هدف کنفرانس VSTTE ارتقای وضعیت هنر از طریق تعامل توسعه نظریه، تکامل ابزار و اعتبار سنجی تجربی است. این مقالات به موضوعاتی مانند: مشخصات و تکنیکهای تأیید، پشتیبانی ابزار برای زبانهای مشخصات، ابزاری برای روشهای مختلف طراحی، یکپارچهسازی ابزار و افزونهها، اتوماسیون در تأیید رسمی، مقایسه ابزار و مخازن معیار، ترکیب ابزارها و تکنیکها، ابزارهای سفارشیسازی میپردازد. برای کاربردهای خاص، مشکلات چالش، روششناسی اصلاح، مدلسازی نیازمندیها، زبانهای مشخصات، مطالعات موردی مشخصات/تأیید، روشهای طراحی نرمافزار، و منطق برنامه.
This volume contains the proceedings of the 4th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2012, held in Philadelphia, PA, USA, in January 2012. The 20 revised full papers presented together with 2 invited talks and 2 tutorials were carefully revised and selected from 54 initial submissions for inclusion in the book. The goal of the VSTTE conference is to advance the state of the art through the interaction of theory development, tool evolution, and experimental validation. The papers address topics such as: specification and verification techniques, tool support for specification languages, tool for various design methodologies, tool integration and plug-ins, automation in formal verification, tool comparisons and benchmark repositories, combination of tools and techniques, customizing tools for particular applications, challenge problems, refinement methodologies, requirements modeling, specification languages, specification/verification case-studies, software design methods, and program logic.
Front Matter....Pages -
Cyber War, Formal Verification and Certified Infrastructure....Pages 1-1
A Certified Multi-prover Verification Condition Generator....Pages 2-17
Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXT....Pages 18-33
The Location Linking Concept: A Basis for Verification of Code Using Pointers....Pages 34-49
Verifying Implementations of Security Protocols by Refinement....Pages 50-65
Deciding Functional Lists with Sublist Sets....Pages 66-81
Developing Verified Programs with Dafny....Pages 82-82
Verifying Two Lines of C with Why3: An Exercise in Program Verification....Pages 83-97
Development and Evaluation of LAV: An SMT-Based Error Finding Platform....Pages 98-113
A Lightweight Technique for Distributed and Incremental Program Verification....Pages 114-129
A Comparison of Intermediate Verification Languages: Boogie and Sireum/Pilar....Pages 130-145
LLBMC : Bounded Model Checking of C and C++ Programs Using a Compiler IR....Pages 146-161
The Marriage of Exploration and Deduction....Pages 162-162
Modeling and Validating the Train Fare Calculation and Adjustment System Using VDM++....Pages 163-178
Formalized Verification of Snapshotable Trees: Separation and Sharing....Pages 179-195
Comparing Verification Condition Generation with Symbolic Execution: An Experience Report....Pages 196-208
Verification of TLB Virtualization Implemented in C....Pages 209-224
Formalization and Analysis of Real-Time Requirements: A Feasibility Study at BOSCH....Pages 225-240
Our Experience with the CodeContracts Static Checker....Pages 241-242
Isabelle/ Circus : A Process Specification and Verification Environment....Pages 243-260
Termination Analysis of Imperative Programs Using Bitvector Arithmetic....Pages 261-277
Specifying and Verifying the Correctness of Dynamic Software Updates....Pages 278-293
Symbolic Execution Enhanced System Testing....Pages 294-309
Infeasible Code Detection....Pages 310-325
Back Matter....Pages -