محبوبترین نویسندگان :
نویسندگان مقالات پربازدید :
مجله استدلال خودکار 2013
جزئیات رویداد
همایش ، رویداد ، ژورنال
اینستاگرام تی پی بین

  • specification and verification of concurrent programs through refinements

    نویسندگان :
    کلمات کلیدی :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 720
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     we present a framework for the specification and verification of reactive concurrent programs using general-purpose mechanical theorem proving. we define specifications for concurrent programs by formalizing a notion of refinements analogous to stuttering trace containment. the formalization supports the definition of intuitive specifications of the intended behavior of a program. we present a collection of proof rules that can be effectively orchestrated by a theorem prover to reason about complex programs using refinements. the proof rules systematically reduce the correctness proof for a concurrent program to the definition and proof of an invariant. we include automated support for discharging this invariant proof with a predicate abstraction tool that leverages the existing theorems proven about the components of the concurrent programs. the framework is integrated with the acl2 theorem prover and we demonstrate its use in the verification of several concurrent programs in acl2.

سوال خود را در مورد این مقاله مطرح نمایید :

با انتخاب دکمه ثبت پرسش، موافقت خود را با قوانین انتشار محتوا در وبسایت تی پی بین اعلام می کنم
مقالات جدیدترین رویدادها
مقالات جدیدترین ژورنال ها