تقرير
RHLE: Modular Deductive Verification of Relational $\forall\exists$ Properties
العنوان: | RHLE: Modular Deductive Verification of Relational $\forall\exists$ Properties |
---|---|
المؤلفون: | Dickerson, Robert, Ye, Qianchuan, Zhang, Michael K., Delaware, Benjamin |
سنة النشر: | 2020 |
المجموعة: | Computer Science |
مصطلحات موضوعية: | Computer Science - Programming Languages, Computer Science - Logic in Computer Science, F.3.1, D.2.4 |
الوصف: | Hoare-style program logics are a popular and effective technique for software verification. Relational program logics are an instance of this approach that enables reasoning about relationships between the execution of two or more programs. Existing relational program logics have focused on verifying that all runs of a collection of programs do not violate a specified relational behavior. Several important relational properties, including refinement and noninterference, do not fit into this category, as they also mandate the existence of specific desirable executions. This paper presents RHLE, a logic for verifying these sorts of relational $\forall\exists$ properties. Key to our approach is a novel form of function specification that employs a variant of ghost variables to ensure that valid implementations exhibit certain behaviors. We have used a program verifier based on RHLE to verify a diverse set of relational $\forall\exists$ properties drawn from the literature. |
نوع الوثيقة: | Working Paper |
URL الوصول: | http://arxiv.org/abs/2002.02904 |
رقم الأكسشن: | edsarx.2002.02904 |
قاعدة البيانات: | arXiv |
كن أول من يترك تعليقا!