دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: 1 نویسندگان: K. Rustan M. Leino (auth.), Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, Rajeev Joshi (eds.) سری: Lecture Notes in Computer Science 6617 : Programming and Software Engineering ISBN (شابک) : 9783642203978, 9783642203985 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 2011 تعداد صفحات: 545 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 8 مگابایت
کلمات کلیدی مربوط به کتاب روش های رسمی ناسا: سومین همایش بین المللی ، NFM 2011 ، پاسادنا ، کالیفرنیا ، ایالات متحده آمریکا ، 18-20 آوریل 2011. مجموعه مقالات: مهندسی نرم افزار، زبان های برنامه نویسی، کامپایلرها، مترجمان، سیستم های عامل، منطق و معانی برنامه ها، مهندسی نرم افزار/برنامه نویسی و سیستم های عامل، تکنیک های برنامه نویسی
در صورت تبدیل فایل کتاب NASA Formal Methods: Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب روش های رسمی ناسا: سومین همایش بین المللی ، NFM 2011 ، پاسادنا ، کالیفرنیا ، ایالات متحده آمریکا ، 18-20 آوریل 2011. مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
این کتاب مجموعه مقالات داوری سومین سمپوزیوم بینالمللی
روشهای رسمی ناسا، NFM 2011 است که در پاسادنا، کالیفرنیا،
ایالات متحده آمریکا، در آوریل 2011 برگزار شد.
26 مقاله کامل اصلاحشده همراه با 12 مقاله ابزار، 3 گفتگوهای
دعوت شده، و 2 آموزش دعوت شده به دقت بررسی و از 141 مورد
ارسالی انتخاب شدند. موضوعات تحت پوشش NFM 2011 شامل اثبات
قضیه، بررسی مدل منطقی، آزمایش و شبیهسازی خودکار، مهندسی
مبتنی بر مدل، سیستمهای بلادرنگ و تصادفی، حلکنندههای SAT و
SMT، اجرای نمادین، اصلاح انتزاع و انتزاع، اما محدود به این
موارد نبودند. تکنیک های تایید ترکیبی؛ تکنیکهای تحلیل استاتیک
و پویا، حفاظت از خطا، امنیت سایبری، فرمالیسمهای مشخصات،
تحلیل نیازمندیها و کاربردهای تکنیکهای رسمی.
This book constitutes the refereed proceedings of the Third
International Symposium on NASA Formal Methods, NFM 2011,
held in Pasadena, CA, USA, in April 2011.
The 26 revised full papers presented together with 12 tool
papers, 3 invited talks, and 2 invited tutorials were
carefully reviewed and selected from 141 submissions. The
topics covered by NFM 2011 included but were not limited to:
theorem proving, logic model checking, automated testing and
simulation, model-based engineering, real-time and stochastic
systems, SAT and SMT solvers, symbolic execution, abstraction
and abstraction refinement, compositional verification
techniques; static and dynamic analysis techniques, fault
protection, cyber security, specification formalisms,
requirements analysis, and applications of formal techniques.
Front Matter....Pages -
From Retrospective Verification to Forward-Looking Development....Pages 1-1
Specifications for Free....Pages 2-12
The Theory and Practice of SALT....Pages 13-40
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java....Pages 41-55
Verifying Functional Correctness of C Programs with VCC....Pages 56-57
Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution....Pages 58-72
Approximate Quantifier Elimination for Propositional Boolean Formulae....Pages 73-88
Towards Flight Control Verification Using Automated Theorem Proving....Pages 89-100
Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis....Pages 101-115
Integrating an Automated Theorem Prover into Agda....Pages 116-130
Efficient Predicate Abstraction of Program Summaries....Pages 131-145
Synthesis for PCTL in Parametric Markov Decision Processes....Pages 146-161
Formalizing Probabilistic Safety Claims....Pages 162-176
The OpenTheory Standard Theory Library....Pages 177-191
Instantiation-Based Invariant Discovery....Pages 192-206
Stuttering Mostly Speeds Up Solving Parity Games....Pages 207-221
Counterexample-Based Error Localization of Behavior Models....Pages 222-236
Call Invariants....Pages 237-251
Symmetry for the Analysis of Dynamic Systems....Pages 252-266
Implementing Cryptographic Primitives in the Symbolic Model....Pages 267-281
Model Checking Using SMT and Theory of Lists....Pages 282-297
Automated Test Case Generation with SMT-Solving and Abstract Interpretation....Pages 298-312
Generating Data Race Witnesses by an SMT-Based Analysis....Pages 313-327
Applying Atomicity and Model Decomposition to a Space Craft System in Event-B....Pages 328-342
A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes....Pages 343-358
CORAL: Solving Complex Constraints for Symbolic PathFinder....Pages 359-374
Automated Formal Verification of the TTEthernet Synchronization Quality....Pages 375-390
Extending the GWV Security Policy and Its Modular Application to a Separation Kernel....Pages 391-405
Combining Partial-Order Reduction and Symbolic Model Checking to Verify LTL Properties....Pages 406-421
Towards Informed Swarm Verification....Pages 422-437
Scaling Up with Event-B: A Case Study....Pages 438-452
D-Finder 2: Towards Efficient Correctness of Incremental Design....Pages 453-458
Infer: An Automatic Program Verifier for Memory Safety of C Programs....Pages 459-465
Model Construction and Priority Synthesis for Simple Interaction Systems....Pages 466-471
OpenJML: JML for Java 7 by Extending OpenJDK....Pages 472-479
jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2....Pages 480-486
opaal : A Lattice Model Checker....Pages 487-493
A Tabular Expression Toolbox for Matlab/Simulink....Pages 494-499
LLVM2CSP : Extracting CSP Models from Concurrent Programs....Pages 500-505
Multi-Core LTS min : Marrying Modularity and Scalability....Pages 506-511
GiNaCRA : A C++ Library for Real Algebraic Computations....Pages 512-517
Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code....Pages 518-524
Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction....Pages 525-531
Back Matter....Pages -