Search results for "rely-guarantee"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
123	Xinyu Feng 0001	Local rely-guarantee reasoning.	POPL	2009	DBLP DOI BibTeX RDF	rely-guarantee reasoning, concurrency, information hiding, separation logic, local reasoning
93	Raffi Khatchadourian, Neelam Soundarajan	Rely-guarantee approach to reasoning about aspect-oriented programs.	SPLAT	2007	DBLP DOI BibTeX RDF	aspect-oriented software, modular verification, rely-guarantee
86	Neil Henderson	Proving the Correctness of Simpson's 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method.	FME	2003	DBLP DOI BibTeX RDF	assertion networks, asynchronous communication, rely-guarantee
86	Jürgen Dingel, David Garlan, Somesh Jha, David Notkin	Towards a Formal Treatment of Implicit Invocation Using Rely/Guarantee Reasoning.	Formal Aspects Comput.	1998	DBLP DOI BibTeX RDF	Rely/guarantee, Assumption/commitment, Implicit invocation
78	Pascal Fenkam, Harald C. Gall, Mehdi Jazayeri	Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach.	FME	2003	DBLP DOI BibTeX RDF	rely/guarantee, deadlock, parallel systems, event-based systems, auxiliary variables
78	Peter Grønning, Thomas Qvist Nielsen, Hans Henrik Løvengreen	Refinement and Composition of Transition-based Rely-Guarantee Specification with Auxiliary Variables.	FSTTCS	1990	DBLP DOI BibTeX RDF	Rely-guarantee specification, transition systems, compositional verification, safety properties, shared variables
70	Eugene W. Stark	A Proof Technique for Rely/Guarantee Properties.	FSTTCS	1985	DBLP DOI BibTeX RDF
55	Viktor Vafeiadis, Matthew J. Parkinson	A Marriage of Rely/Guarantee and Separation Logic.	CONCUR	2007	DBLP DOI BibTeX RDF
48	Joey W. Coleman	Expression Decomposition in a Rely/Guarantee Context.	VSTTE	2008	DBLP DOI BibTeX RDF
48	Cliff B. Jones, Ken G. Pierce	Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification.	ABZ	2008	DBLP DOI BibTeX RDF
46	Tom Ridge	Verifying distributed systems: the operational approach.	POPL	2009	DBLP DOI BibTeX RDF	ground and symbolic evaluation, hoare-style assertions, persistent queue, rely/guarantee, distributed, refinement, invariants, network protocol, operational semantics, infrastructure, separation, linearizability, hol, ocaml, local reasoning, inductive reasoning
46	Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro 0001	Proving correctness of highly-concurrent linearisable objects.	PPoPP	2006	DBLP DOI BibTeX RDF	rely-guarantee reasoning, shared-memory concurrency, formal verification, concurrent programming, linearisability
46	Xinyu Feng 0001, Zhong Shao	Modular verification of concurrent assembly code with dynamic thread creation and termination.	ICFP	2005	DBLP DOI BibTeX RDF	concurrency verification, dynamic thread creation, proof-carrying code, rely-guarantee
44	Mike Dodds, Xinyu Feng 0001, Matthew J. Parkinson, Viktor Vafeiadis	Deny-Guarantee Reasoning.	ESOP	2009	DBLP DOI BibTeX RDF
40	Hasan Amjad, Richard Bornat	Towards Automatic Stability Analysis for Rely-Guarantee Proofs.	VMCAI	2009	DBLP DOI BibTeX RDF
40	Leonor Prensa Nieto	The Rely-Guarantee Method in Isabelle/HOL.	ESOP	2003	DBLP DOI BibTeX RDF
40	Frank S. de Boer, Ulrich Hannemann, Willem P. de Roever	Formal Justification of the Rely-Guarantee Paradigm for Shared-Variable Concurrency: A Semantic Approach.	World Congress on Formal Methods	1999	DBLP DOI BibTeX RDF
38	Raffi Khatchadourian, Johan Dovland, Neelam Soundarajan	Enforcing behavioral constraints in evolving aspect-oriented programs.	FOAL	2008	DBLP DOI BibTeX RDF	aspect-oriented programming, modular reasoning, rely-guarantee
38	Neil Evans, Helen Treharne	Interactive tool support for CSP \|\| B consistency checking.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Formal method integration, Tool supported verification, Rely/guarantee techniques, CSP, B
38	Alan Burns 0001, Tse-Min Lin	An engineering process for the verification of real-time systems.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Rely/guarantee conditions, Model checking, Scheduling analysis, UPPAAL, SPARK, Ada95, Ravenscar profile
38	Marc Shapiro 0001	Practical proofs of concurrent programs.	ICFP	2006	DBLP DOI BibTeX RDF	concurrent programming, assertions, hoare logic, program proofs, rely-guarantee
38	Ralph-Johan Back, Joakim von Wright	Compositional Action System Refinement.	Formal Aspects Comput.	2003	DBLP DOI BibTeX RDF	Rely/guarantee, Refinement, Compositionality, Action systems
38	Ekkart Kindler	A Compositional Partial Order Semantics for Petri Net Components.	ICATPN	1997	DBLP DOI BibTeX RDF	Petri net component, rely-guarantee specification, fully abstract, compositional semantics, partial order semantics
33	Yongwang Zhao, David Sanán	Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications.	CoRR	2023	DBLP DOI BibTeX RDF
33	Yongwang Zhao, David Sanán	Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security.	CoRR	2023	DBLP DOI BibTeX RDF
33	Cliff B. Jones, Alan Burns 0001	Extending Rely-Guarantee thinking to handle Real-Time Scheduling.	CoRR	2023	DBLP DOI BibTeX RDF
33	Nisansala P. Yatapanage	Rely/Guarantee, Refinement and the ABA Problem: Part 1.	CoRR	2023	DBLP DOI BibTeX RDF
33	Ori Lahav 0001, Brijesh Dongol, Heike Wehrheim	Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version).	CoRR	2023	DBLP DOI BibTeX RDF
33	Nisansala P. Yatapanage, Cliff B. Jones	Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols.	CoRR	2023	DBLP DOI BibTeX RDF
33	ShangBei Wang, WeiYu Dong	Matching Logic for Concurrent Programs Based on Rely/Guarantee and Abstract Patterns.	Int. J. Softw. Eng. Knowl. Eng.	2023	DBLP DOI BibTeX RDF
33	Ori Lahav 0001, Brijesh Dongol, Heike Wehrheim	Rely-Guarantee Reasoning for Causally Consistent Shared Memory.	CAV (1)	2023	DBLP DOI BibTeX RDF
33	Huan Sun, Ziyu Mao, Jingyi Wang, Ziyan Zhao, Wenhai Wang	Applying Rely-Guarantee Reasoning on Concurrent Memory Management and Mailbox in μC/OS-II: A Case Study.	FMICS	2023	DBLP DOI BibTeX RDF
33	Larissa A. Meinicke, Ian J. Hayes	Using scylindric algebra to support local variables in rely/guarantee concurrency.	FormaliSE	2023	DBLP DOI BibTeX RDF
33	Thomas Pani, Georg Weissenbacher, Florian Zuleger	Rely-guarantee bound analysis of parameterized concurrent shared-memory programs.	Formal Methods Syst. Des.	2021	DBLP DOI BibTeX RDF
33	Ian J. Hayes, Larissa A. Meinicke, Patrick A. Meiring	Deriving Laws for Developing Concurrent Programs in a Rely-Guarantee Style.	CoRR	2021	DBLP BibTeX RDF
33	David Sanán, Yongwang Zhao, Shang-Wei Lin 0001, Yang Liu 0003	CSim2: Compositional Top-down Verification of Concurrent Systems using Rely-Guarantee.	ACM Trans. Program. Lang. Syst.	2021	DBLP DOI BibTeX RDF
33	Nicholas Coughlin, Kirsten Winter, Graeme Smith 0001	Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models.	FM	2021	DBLP DOI BibTeX RDF
33	Cliff B. Jones, Alan Burns 0001	A Rely-Guarantee Specification of Mixed-Criticality Scheduling.	CoRR	2020	DBLP BibTeX RDF
33	Nicholas Coughlin, Graeme Smith 0001	Rely/Guarantee Reasoning for Noninterference in Non-Blocking Algorithms.	CSF	2020	DBLP DOI BibTeX RDF
33	Wenjing Xul, Yongwang Zhao, Dianfu Ma, YuXin Zhang, Qian Xiao	Rely-Guarantee Reasoning about Messaging System for Autonomous Vehicles.	TASE	2020	DBLP DOI BibTeX RDF
33	Xuan-Bach Le, David Sanán, Jun Sun 0001, Shang-Wei Lin 0001	Automatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications.	ICECCS	2020	DBLP DOI BibTeX RDF
33	Larissa A. Meinicke, Ian J. Hayes	Handling localisation in rely/guarantee concurrency: An algebraic approach.	CoRR	2019	DBLP BibTeX RDF
33	Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek	Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology.	J. Autom. Reason.	2019	DBLP DOI BibTeX RDF
33	Cliff B. Jones, Nisansala Yatapanage	Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example.	Formal Aspects Comput.	2019	DBLP DOI BibTeX RDF
33	Yongwang Zhao, David Sanán	Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS.	CAV (2)	2019	DBLP DOI BibTeX RDF
33	Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu 0003	A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems.	FM	2019	DBLP DOI BibTeX RDF
33	Ian J. Hayes, Larissa A. Meinicke	Developing an Algebra for Rely/Guarantee Concurrency: Design Decisions and Challenges.	UTP	2019	DBLP DOI BibTeX RDF
33	Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie	Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement.	SAC	2018	DBLP DOI BibTeX RDF
33	Thomas Pani, Georg Weissenbacher, Florian Zuleger	Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms.	FMCAD	2018	DBLP DOI BibTeX RDF
33	Elvira Albert, Antonio Flores-Montoya, Samir Genaim, Enrique Martin-Martin	Rely-Guarantee Termination and Cost Analyses of Loops with Concurrent Interleavings.	J. Autom. Reason.	2017	DBLP DOI BibTeX RDF
33	Colin S. Gordon, Michael D. Ernst, Dan Grossman, Matthew J. Parkinson	Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types.	ACM Trans. Program. Lang. Syst.	2017	DBLP DOI BibTeX RDF
33	Ian J. Hayes, Cliff B. Jones	A Guide to Rely/Guarantee Thinking.	SETSS	2017	DBLP DOI BibTeX RDF
33	David Sanán, Yongwang Zhao, Zhe Hou, Fuyuan Zhang, Alwen Tiu, Yang Liu 0003	CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs.	TACAS (1)	2017	DBLP DOI BibTeX RDF
33	Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek	Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology.	ITP	2017	DBLP DOI BibTeX RDF
33	Cliff B. Jones, Andrius Velykis, Nisansala Yatapanage	General Lessons from a Rely/Guarantee Development.	SETTA	2017	DBLP DOI BibTeX RDF
33	Diego Machado Dias	Mechanising an algebraic rely-guarantee refinement calculus.		2017	RDF
33	Annabelle McIver, Tahiry M. Rabehaja, Georg Struth	Probabilistic rely-guarantee calculus.	Theor. Comput. Sci.	2016	DBLP DOI BibTeX RDF
33	Ian J. Hayes	Generalised rely-guarantee concurrency: An algebraic foundation.	CoRR	2016	DBLP BibTeX RDF
33	Ian J. Hayes	Generalised rely-guarantee concurrency: an algebraic foundation.	Formal Aspects Comput.	2016	DBLP DOI BibTeX RDF
33	Stephan van Staden	On Rely-Guarantee Reasoning.	MPC	2015	DBLP DOI BibTeX RDF
33	Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, Viktor Vafeiadis	Rely/Guarantee Reasoning for Asynchronous Programs.	CONCUR	2015	DBLP DOI BibTeX RDF
33	Annabelle McIver, Tahiry M. Rabehaja, Georg Struth	Probabilistic Rely-guarantee Calculus.	CoRR	2014	DBLP BibTeX RDF
33	Jinjiang Lei, Zongyan Qiu	Rely-Guarantee Based Reasoning for Message-Passing Programs.	Sci. Ann. Comput. Sci.	2014	DBLP DOI BibTeX RDF
33	Hongjin Liang 0001, Xinyu Feng 0001, Ming Fu	Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations.	ACM Trans. Program. Lang. Syst.	2014	DBLP DOI BibTeX RDF
33	Alasdair Armstrong, Victor B. F. Gomes, Georg Struth	Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools.	FM	2014	DBLP DOI BibTeX RDF
33	Filipe Militão, Jonathan Aldrich, Luís Caires	Rely-Guarantee Protocols.	ECOOP	2014	DBLP DOI BibTeX RDF
33	Alasdair Armstrong, Victor B. F. Gomes, Georg Struth	Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools.	CoRR	2013	DBLP BibTeX RDF
33	Ian J. Hayes	Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions.	FTSCS	2013	DBLP DOI BibTeX RDF
33	Colin S. Gordon, Michael D. Ernst, Dan Grossman	Rely-guarantee references for refinement types over aliased mutable data.	PLDI	2013	DBLP DOI BibTeX RDF
33	Xiaofeng Wu, Qiwen Xu, Huibiao Zhu	Formal Analysis of AODV Using Rely-Guarantee.	TASE	2013	DBLP DOI BibTeX RDF
33	Hongjin Liang 0001, Xinyu Feng 0001, Ming Fu	A rely-guarantee-based simulation for verifying concurrent program transformations.	POPL	2012	DBLP DOI BibTeX RDF
33	Said Rabah Azzam, Shikun Zhou	Implementation methodology of Rely/Guarantee plug-in for Protégé.	ICITST	2012	DBLP BibTeX RDF
33	Brijesh Dongol, Ian J. Hayes	Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands.	IFM	2012	DBLP DOI BibTeX RDF
33	William Mansky, Elsa L. Gunter	Using Locales to Define a Rely-Guarantee Temporal Logic.	ITP	2012	DBLP DOI BibTeX RDF
33	Huibiao Zhu, Qiwen Xu, Chris Ma, Shengchao Qin, Zongyan Qiu	The Rely/Guarantee Approach to Verifying Concurrent BPEL Programs.	SEFM	2012	DBLP DOI BibTeX RDF
33	Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Wolfgang Reif	Interleaved Programs and Rely-Guarantee Reasoning with ITL.	TIME	2011	DBLP DOI BibTeX RDF
33	Richard Bornat, Hasan Amjad	Inter-process buffers in separation logic with rely-guarantee.	Formal Aspects Comput.	2010	DBLP DOI BibTeX RDF
33	Tom Ridge	A Rely-Guarantee Proof System for x86-TSO.	VSTTE	2010	DBLP DOI BibTeX RDF
33	John Wickerson, Mike Dodds, Matthew J. Parkinson	Explicit Stabilisation for Modular Rely-Guarantee Reasoning.	ESOP	2010	DBLP DOI BibTeX RDF
33	Kenneth George Pierce	Enhancing the usability of rely-guarantee conditions for atomicity refinement.		2009	RDF
33	Hasan Amjad, Richard Bornat	Model Checking for Stability Analysis in Rely-Guarantee Proofs.	VERIFY	2008	DBLP BibTeX RDF
33	Joey W. Coleman, Cliff B. Jones	A Structural Proof of the Soundness of Rely/guarantee Rules.	J. Log. Comput.	2007	DBLP DOI BibTeX RDF
33	Joshua D. Guttman, F. Javier Thayer, Jay A. Carlson, Jonathan C. Herzog, John D. Ramsdell, Brian T. Sniffen	Trust Management in Strand Spaces: A Rely-Guarantee Method.	ESOP	2004	DBLP DOI BibTeX RDF
33	Leonor Prensa Nieto	Verification of parallel programs with the Owicki-Gries and Rely-Guarantee methods in Isabelle, HOL.		2002	RDF
33	Carlos H. C. Duarte, T. S. E. Maibaum	A rely-guarantee discipline for open distributed systems design.	Inf. Process. Lett.	2000	DBLP DOI BibTeX RDF
33	Pierre Collette, Cliff B. Jones	Enhancing the tractability of rely/guarantee specifications in the development of interfering operations.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
33	Qiwen Xu, Willem P. de Roever, Jifeng He 0001	The Rely-Guarantee Method for Verifying Shared Variable Concurrent Programs.	Formal Aspects Comput.	1997	DBLP DOI BibTeX RDF
15	Ketil Stølen	An Attempt to Reason about Shared-State Concurrency in the Style of VDM.	VDM Europe (1)	1991	DBLP DOI BibTeX RDF
15	Frank S. de Boer, Ulrich Hannemann, Willem P. de Roever	Hoare-Style Compositional Proof Systems for Reactive Shared Variable Concurency.	FSTTCS	1997	DBLP DOI BibTeX RDF
15	Pierre Collette	Application of the Composition Principle to Unity-like Specifications.	TAPSOFT	1993	DBLP DOI BibTeX RDF
11	Xinyu Feng 0001, Rodrigo Ferreira, Zhong Shao	On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning.	ESOP	2007	DBLP DOI BibTeX RDF
11	Cristiano Calcagno, Matthew J. Parkinson, Viktor Vafeiadis	Modular Safety Checking for Fine-Grained Concurrency.	SAS	2007	DBLP DOI BibTeX RDF
7	C. A. R. Hoare, Bernhard Möller, Georg Struth, Ian Wehrman	Foundations of Concurrent Kleene Algebra.	RelMiCS	2009	DBLP DOI BibTeX RDF
7	Tayfun Elmas, Shaz Qadeer, Serdar Tasiran	A calculus of atomic actions.	POPL	2009	DBLP DOI BibTeX RDF	abstraction, concurrent programs, reduction, atomicity
7	Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis	Proving that non-blocking algorithms don't block.	POPL	2009	DBLP DOI BibTeX RDF	formal verification, concurrent programming, termination, liveness
7	C. A. R. Hoare, Bernhard Möller, Georg Struth, Ian Wehrman	Concurrent Kleene Algebra.	CONCUR	2009	DBLP DOI BibTeX RDF
7	Viktor Vafeiadis	Shape-Value Abstraction for Verifying Linearizability.	VMCAI	2009	DBLP DOI BibTeX RDF
7	Jonathan Hayman, Glynn Winskel	Independence and Concurrent Separation Logic.	LICS	2006	DBLP DOI BibTeX RDF
7	Arnaud Bailly, Mireille Clerbout, Isabelle Simplot-Ryl	Component Composition Preserving Behavioural Contracts Based on Communication Traces.	CIAA	2005	DBLP DOI BibTeX RDF
7	Carlo A. Furia, Matteo Rossi 0001, Dino Mandrioli, Angelo Morzenti	Automated Compositional Proofs for Real-Time Systems.	FASE	2005	DBLP DOI BibTeX RDF