دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: 1 نویسندگان: Leslie Lamport (auth.), Gregor von Bochmann, David Karl Probst (eds.) سری: Lecture Notes in Computer Science 663 ISBN (شابک) : 9783540564966, 9783540475729 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 1993 تعداد صفحات: 432 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 7 مگابایت
در صورت تبدیل فایل کتاب Computer Aided Verification: Fourth International Workshop, CAV '92 Montreal, Canada, June 29 – July 1, 1992 Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب تأیید به کمک رایانه: چهارمین کارگاه بین المللی، CAV '92 مونترال، کانادا، 29 ژوئن - 1 ژوئیه 1992 مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
این جلد مجموعه مقالات چهارمین کارگاه تأیید به کمک رایانه (CAV '92) است که در مونترال، 29 ژوئن - 1 ژوئیه 1992 برگزار شد. هدف این مجموعه کارگاه ها گرد هم آوردن محققان و پزشکان علاقه مند است. در توسعه و استفاده از روشها، ابزارها و تئوریها برای تأیید رایانهای سیستمهای همزمان. کارگاه ها فرصتی را برای مقایسه روش های مختلف تأیید و ابزارهای عملی فراهم می کند که می تواند برای کمک به طراح برنامه ها مورد استفاده قرار گیرد. تاکید بر نتایج تحقیقات جدید و کاربرد نتایج موجود برای مشکلات راستیآزمایی واقعی است. این جلد شامل 31 مقاله است که از بین 75 مقاله ارسالی انتخاب شده است. اینها به بخشهایی در مورد تکنیکهای کاهش، بررسی اثبات، تأیید نمادین، تأیید زمان، رویکردهای سفارش جزئی، مطالعات موردی، بررسی مدل و اثبات، و سایر رویکردها سازماندهی میشوند. این جلد با یک سخنرانی دعوت شده توسط لزلی لامپورت با عنوان \"تأیید با مانع کامپیوتری (انسانها نیز می توانند آن را انجام دهند)\" شروع می شود.
This volume gives the proceedings of the Fourth Workshop on Computer-Aided Verification (CAV '92), held in Montreal, June 29 - July 1, 1992. The objective of this series of workshops is to bring together researchers and practitioners interested in the development and use of methods, tools and theories for the computer-aided verification of concurrent systems. The workshops provide an opportunity for comparing various verification methods and practical tools that can be used to assist the applications designer. Emphasis is placed on new research results and the application of existing results to real verification problems. The volume contains 31 papers selected from 75 submissions. These are organized into parts on reduction techniques, proof checking, symbolic verification, timing verification, partial-order approaches, case studies, model and proof checking, and other approaches. The volume starts with an invited lecture by Leslie Lamport entitled "Computer-hindered verification (humans can do it too)".
Computer-hindered verification (humans can do it too)....Pages 1-1
Modular abstractions for verifying real-time distributed systems....Pages 2-15
Layering techniques for development of parallel systems....Pages 16-29
Efficient local correctness checking....Pages 30-43
Mechanical verification of concurrent systems with TLA....Pages 44-55
Using a theorem prover for reasoning about concurrent algorithms....Pages 56-68
Verifying a logic synthesis tool in Nuprl: A case study in software verification....Pages 69-81
Higher-level specification and verification with BDDs....Pages 82-95
Symbolic bisimulation minimisation....Pages 96-108
Towards a verification technique for large synchronous circuits....Pages 109-122
Verifying timed behavior automata with nonbinary delay constraints....Pages 123-136
Timing verification by successive approximation....Pages 137-150
A verification strategy for timing constrained systems....Pages 151-163
Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits....Pages 164-177
State space caching revisited....Pages 178-191
Verification in process algebra of the distributed control of track vehicles—A case study....Pages 192-205
Design verification of a microprocessor using branching time regular temporal logic....Pages 206-219
A case study in safety-critical design....Pages 220-233
Automatic reduction in CTL compositional model checking....Pages 234-247
Compositional model checking for linear-time temporal logic....Pages 248-259
Property preserving simulations....Pages 260-273
Verification with real-time COSPAN....Pages 274-287
Model-checking for real-time systems specified in Lotos....Pages 288-301
Decidability of bisimulation equivalences for parallel timer processes....Pages 302-315
A proof assistant for symbolic model-checking....Pages 316-329
Tableau recycling....Pages 330-342
Crocos: An integrated environment for interactive verification of SDL specifications....Pages 343-356
Verifying general safety and liveness properties with integer programming....Pages 357-369
Generating diagnostic information for behavioral preorders....Pages 370-383
A verification procedure via invariant for extended communicating finite-state machines....Pages 384-395
Efficient ω-regular language containment....Pages 396-409
Faster model checking for the modal Mu-Calculus....Pages 410-422