guest ::
| 001 | 1020873 | ||
| 005 | 20251108054703.0 | ||
| 024 | 7 | _ | |2 datacite_doi |a 10.18154/RWTH-2025-09295 |
| 037 | _ | _ | |a RWTH-2025-09295 |
| 041 | _ | _ | |a English |
| 082 | _ | _ | |a 004 |
| 100 | 1 | _ | |0 P:(DE-82)1021015 |a Eissing, Marcel |b 0 |u rwth |
| 245 | _ | _ | |a On the relation of rely-guarantee and assume-guarantee reasoning |c by Marcel Eissing |h online |
| 260 | _ | _ | |a Aachen |b RWTH Aachen University |c 2025 |
| 300 | _ | _ | |a 1 Online-Ressource : Illustrationen |
| 336 | 7 | _ | |0 2 |2 EndNote |a Thesis |
| 336 | 7 | _ | |0 PUB:(DE-HGF)2 |2 PUB:(DE-HGF) |a Bachelor Thesis |b bachelor |m bachelor |
| 336 | 7 | _ | |2 BibTeX |a MASTERSTHESIS |
| 336 | 7 | _ | |2 DRIVER |a bachelorThesis |
| 336 | 7 | _ | |2 DataCite |a Output Types/Supervised Student Publication |
| 336 | 7 | _ | |2 ORCID |a SUPERVISED_STUDENT_PUBLICATION |
| 500 | _ | _ | |a Veröffentlicht auf dem Publikationsserver der RWTH Aachen University |
| 502 | _ | _ | |a Bachelorarbeit, RWTH Aachen University, 2025 |b Bachelorarbeit |c RWTH Aachen University |d 2025 |g Fak01 |o 2025-09-07 |
| 520 | 3 | _ | |l ger |
| 520 | _ | _ | |a Assume-guarantee and rely-guarantee reasoning are well-established compositional methods dealing with the verification of composite systems. While assume-guarantee reasoning targets parallel com- position of transition systems, rely-guarantee reasoning is tailored to concurrent shared memory pro- grams. Both concepts are similar in their approach, as they focus their analysis on a local component and introduce an abstraction of its environment. The abstraction of the environment is used as an assumption under which a desired property can be guaranteed. Though the concepts work in a similar fashion, they exhibit substantial differences. This thesis explores the concrete nature of the relationship of assume-guarantee and rely-guarantee reasoning. We propose a formal construction that translates the verification of a rely-guarantee specification on a concurrent program to the verification of properties on transition systems in the context of assume-guarantee reasoning. We show that our construction is indicative of a close relation between the inference rule for concurrency in rely-guarantee reasoning and a non-circular assume-guarantee inference rule. Additionally, we show that our construction can be used as a new means to prove a rely-guarantee specification of a concurrent program. |l eng |
| 591 | _ | _ | |a Germany |
| 700 | 1 | _ | |0 P:(DE-82)IDM00048 |a Katoen, Joost-Pieter |b 1 |e Thesis advisor |u rwth |
| 700 | 1 | _ | |0 P:(DE-82)IDM01580 |a Noll, Thomas |b 2 |e Thesis advisor |u rwth |
| 700 | 1 | _ | |0 P:(DE-82)TABP:(DE-82)942871 |a Verscht, Lena |b 3 |e Consultant |u rwth |
| 700 | 1 | _ | |0 P:(DE-82)IDM06570 |a Mertens, Hannah |b 4 |e Consultant |u rwth |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/1020873/files/1020873.pdf |y OpenAccess |
| 909 | C | O | |o oai:publications.rwth-aachen.de:1020873 |p openaire |p open_access |p VDB |p driver |p dnbdelivery |
| 910 | 1 | _ | |0 I:(DE-588b)36225-6 |6 P:(DE-82)1021015 |a RWTH Aachen |b 0 |k RWTH |
| 910 | 1 | _ | |0 I:(DE-588b)36225-6 |6 P:(DE-82)IDM00048 |a RWTH Aachen |b 1 |k RWTH |
| 910 | 1 | _ | |0 I:(DE-588b)36225-6 |6 P:(DE-82)IDM01580 |a RWTH Aachen |b 2 |k RWTH |
| 910 | 1 | _ | |0 I:(DE-588b)36225-6 |6 P:(DE-82)TABP:(DE-82)942871 |a RWTH Aachen |b 3 |k RWTH |
| 910 | 1 | _ | |0 I:(DE-588b)36225-6 |6 P:(DE-82)IDM06570 |a RWTH Aachen |b 4 |k RWTH |
| 914 | 1 | _ | |y 2025 |
| 915 | _ | _ | |0 StatID:(DE-HGF)0510 |2 StatID |a OpenAccess |
| 920 | 1 | _ | |0 I:(DE-82)121310_20140620 |k 121310 |l Lehrstuhl für Softwaremodellierung und Verifikation (Informatik 2) |x 0 |
| 920 | 1 | _ | |0 I:(DE-82)120000_20140620 |k 120000 |l Fachgruppe Informatik |x 1 |
| 980 | 1 | _ | |a FullTexts |
| 980 | _ | _ | |a I:(DE-82)120000_20140620 |
| 980 | _ | _ | |a I:(DE-82)121310_20140620 |
| 980 | _ | _ | |a UNRESTRICTED |
| 980 | _ | _ | |a VDB |
| 980 | _ | _ | |a bachelor |
| Library | Collection | CLSMajor | CLSMinor | Language | Author |
|---|