guest ::
001020873 001__ 1020873 001020873 005__ 20251108054703.0 001020873 0247_ $$2datacite_doi$$a10.18154/RWTH-2025-09295 001020873 037__ $$aRWTH-2025-09295 001020873 041__ $$aEnglish 001020873 082__ $$a004 001020873 1001_ $$0P:(DE-82)1021015$$aEissing, Marcel$$b0$$urwth 001020873 245__ $$aOn the relation of rely-guarantee and assume-guarantee reasoning$$cby Marcel Eissing$$honline 001020873 260__ $$aAachen$$bRWTH Aachen University$$c2025 001020873 300__ $$a1 Online-Ressource : Illustrationen 001020873 3367_ $$02$$2EndNote$$aThesis 001020873 3367_ $$0PUB:(DE-HGF)2$$2PUB:(DE-HGF)$$aBachelor Thesis$$bbachelor$$mbachelor 001020873 3367_ $$2BibTeX$$aMASTERSTHESIS 001020873 3367_ $$2DRIVER$$abachelorThesis 001020873 3367_ $$2DataCite$$aOutput Types/Supervised Student Publication 001020873 3367_ $$2ORCID$$aSUPERVISED_STUDENT_PUBLICATION 001020873 500__ $$aVeröffentlicht auf dem Publikationsserver der RWTH Aachen University 001020873 502__ $$aBachelorarbeit, RWTH Aachen University, 2025$$bBachelorarbeit$$cRWTH Aachen University$$d2025$$gFak01$$o2025-09-07 001020873 5203_ $$lger 001020873 520__ $$aAssume-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.$$leng 001020873 591__ $$aGermany 001020873 7001_ $$0P:(DE-82)IDM00048$$aKatoen, Joost-Pieter$$b1$$eThesis advisor$$urwth 001020873 7001_ $$0P:(DE-82)IDM01580$$aNoll, Thomas$$b2$$eThesis advisor$$urwth 001020873 7001_ $$0P:(DE-82)TABP:(DE-82)942871$$aVerscht, Lena$$b3$$eConsultant$$urwth 001020873 7001_ $$0P:(DE-82)IDM06570$$aMertens, Hannah$$b4$$eConsultant$$urwth 001020873 8564_ $$uhttps://publications.rwth-aachen.de/record/1020873/files/1020873.pdf$$yOpenAccess 001020873 909CO $$ooai:publications.rwth-aachen.de:1020873$$popenaire$$popen_access$$pVDB$$pdriver$$pdnbdelivery 001020873 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)1021015$$aRWTH Aachen$$b0$$kRWTH 001020873 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM00048$$aRWTH Aachen$$b1$$kRWTH 001020873 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM01580$$aRWTH Aachen$$b2$$kRWTH 001020873 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)TABP:(DE-82)942871$$aRWTH Aachen$$b3$$kRWTH 001020873 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM06570$$aRWTH Aachen$$b4$$kRWTH 001020873 9141_ $$y2025 001020873 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess 001020873 9201_ $$0I:(DE-82)121310_20140620$$k121310$$lLehrstuhl für Softwaremodellierung und Verifikation (Informatik 2)$$x0 001020873 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1 001020873 961__ $$c2025-11-07T13:41:56.361720$$x2025-11-05T12:32:38.654356$$z2025-11-07T13:41:56.361720 001020873 9801_ $$aFullTexts 001020873 980__ $$aI:(DE-82)120000_20140620 001020873 980__ $$aI:(DE-82)121310_20140620 001020873 980__ $$aUNRESTRICTED 001020873 980__ $$aVDB 001020873 980__ $$abachelor