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 |
|