A Proof Technique for Rely/Guarantee Properties

No abstract is available for this paper.

• Publication year

  1985

• Venue

  Foundations of Software Technology and Theoretical Computer Science

• Publication date

  1985-12-16

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/3-540-16042-6_21
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Temporal Logic of Programs

  1987cited by this paper
• Probabilistic Analysis of a Network Resource Allocation Algorithm

  1986cited by this paper
• Probabilistic Analysis of a Network Resource Allocation Algorithm. Revision.

  1985cited by this paper
• FOUNDATIONS OF A THEORY OF SPECIFICATION FOR DISTRIBUTED SYSTEMS

  1984cited by this paper
• Now you may compose temporal logic specifications

  1984cited by this paper
• Specifying Concurrent Program Modules

  1983cited by this paper
• Verification of concurrent programs: a temporal proof system

  1983cited by this paper
• Specification and Design of (Parallel) Programs

  1983cited by this paper
• Proving Liveness Properties of Concurrent Programs

  1982cited by this paper
• Proving safety and liveness of communicating processes with examples

  1982cited by this paper
• Proofs of Networks of Processes

  1981cited by this paper
• Developing methods for computer programs including a notion of interference

  1981cited by this paper
• Temporal Logic Specification of Distributed Systems

  1981cited by this paper
• Verifying network protocols using temporal logic

  1980cited by this paper
• "Sometime" is sometimes "not never": on the temporal logic of programs

  1980cited by this paper
• Modular Program Construction Using Abstractions

  1979cited by this paper
• The temporal logic of programs

  1977cited by this paper
• A Discipline of Programming

  1976cited by this paper
• Verifying properties of parallel programs: an axiomatic approach

  1976cited by this paper
• Program development by stepwise refinement

  1971cited by this paper
• An axiomatic basis for computer programming

  1969cited by this paper

• Automatic assume-guarantee reasoning for safety and liveness using passive learning

  2025cites this paper
• Quantified Underapproximation via Labeled Bunches

  2025cites this paper
• Compositional Shielding and Reinforcement Learning for Multi-Agent Systems

  2024cites this paper
• Contract-Based Distributed Synthesis in Two-Objective Parity Games

  2023cites this paper
• Contract-Based Distributed Logical Controller Synthesis

  2023cites this paper
• composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing

  2022cites this paper
• Compositional model checking of SDN platform

  2021cites this paper
• Compositional model checking of an SDN platform

  2021cites this paper
• A Simple Model of Relaxed Memory

  2020cites this paper
• Pomsets with preconditions: a simple model of relaxed memory

  2020cites this paper
• Modular verification of web page layout

  2019cites this paper
• Layering Assume-Guarantee Contracts for Hierarchical System Design

  2018influential citation
• Theory and methodology of assumption/commitment based system interface specification and architectural contracts

  2018cites this paper
• Contracts for System Design

  2018cites this paper
• Assumption Commitment Types for Resource Management in Virtually Timed Ambients

  2018cites this paper
• Theory and methodology of assumption/commitment based system interface specification and architectural contracts

  2017cites this paper
• A Component-Based Simplex Architecture for High-Assurance Cyber-Physical Systems

  2017cites this paper
• Explorer A Compositional Protocol Verification Using Relativized

  2017cites this paper
• Compositional verification of component-based real-time systems and applications. (Vérification compositionnelle des systèmes temps-réel à base de composants et applications)

  2016cites this paper
• A program logic for concurrent objects under fair scheduling

  2016cites this paper
• Symbolic construction of GR(1) contracts for synchronous systems with full information

  2015cites this paper
• Contracts for Systems Design: Theory

  2015cites this paper
• Compositional Contract Abstraction for System Design

  2014cites this paper
• Modular Synthesis of Sketches Using Models

  2014cites this paper
• Supporting the Specification and Runtime Validation of Asynchronous Calling Patterns in Reactive Systems

  2014cites this paper
• Dependable reuse & guarded integration of automotive software components

  2013cites this paper
• Compositional Synthesis of Controllers from Scenario-Based Assume-Guarantee Specifications

  2013influential citation
• Compositional and Scheduler-Independent information flow security

  2013cites this paper
• Bridging the chasm between MDE and the world of compilation

  2012cites this paper
• Component Assemblies in the Context of Manycore

  2011cites this paper
• Compositional reasoning using intervals and time reversal

  2011cites this paper
• A Theory of Synchronous Relational Interfaces

  2011influential citation
• Assumptions and Guarantees for Compositional Noninterference

  2011cites this paper
• Assume-Guarantee Tools for Component-Based Software Verification

  2010cites this paper
• The Theory of Timed I/O Automata, Second Edition

  2010cites this paper
• On the completeness of compositional reasoning methods

  2010cites this paper
• Incremental Invariant Generation for Compositional Design

  2010cites this paper
• Incremental Component-based Construction and Deadlock Checking

  2009cites this paper
• Software model checking

  2009cites this paper
• Reasoning about Program Composition

  2009cites this paper
• A Minimized Assumption Generation Method for Component-Based Software Verification

  2009cites this paper
• D-Finder: A Tool for Compositional Deadlock Detection and Verification

  2009cites this paper
• Assume-guarantee verification of evolving component-based software

  2009cites this paper
• Compositional verification of fault-tolerant real-time programs

  2009cites this paper
• An open framework for certified system software

  2008cites this paper
• Compositional Verification for Component-Based Systems and Application

  2008cites this paper
• Automatic symbolic compositional verification by learning assumptions

  2008cites this paper
• Synthesis and compositional verification using language learning

  2007cites this paper
• Interact : un modèle général de contrat pour la garantie des assemblages de composants et services. (Interact : a general contract model for the guarantee of components and services assemblies)

  2007cites this paper
• Thesis Proposal Compositional Fault-tolerant Distributed Object Systems

  2007cites this paper
• The Theory of Timed I/O Automata

  2006cites this paper
• Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition

  2006cites this paper
• Robust composition: towards a unified approach to access control and concurrency control

  2006cites this paper
• Foundations for Circular

  2006cites this paper
• Design by Contract Deontic Design Language for Multiagent Systems

  2005cites this paper
• Modular Verification of Multi-Threaded Assembly Code

  2005cites this paper
• The open family of temporal logics: Annotating temporal operators with input constraints

  2005cites this paper
• Modular verification of concurrent assembly code with dynamic thread creation and termination

  2005cites this paper
• Compositional verification and specification of refinement for reactive systems in a dense time temporal logic

  2005cites this paper
• Symbolic Compositional Verification by Learning Assumptions

  2005cites this paper
• Modular verification of multithreaded programs

  2005cites this paper
• Scalable Specification and Reasoning: Challenges for Program Logic

  2005cites this paper
• SAVCBS 2004 Specification and Verification of Component-Based Systems: Workshop Proceedings

  2004cites this paper
• Modular refinement of hierarchic reactive machines

  2004cites this paper
• Decomposing Verification of Timed I/O Automata

  2004cites this paper
• Lessons Learned from Model Checking a NASA Robot Controller

  2004cites this paper
• Overview of ComFoRT: A Model Checking Reasoning Framework

  2004cites this paper
• Formal verification of timed systems: a survey and perspective

  2004cites this paper
• Encapsulating Concurrency as an Approach to Unification

  2004cites this paper
• Verification of safety properties for concurrent assembly code

  2004cites this paper
• Safety verification of low-level code

  2004cites this paper
• Adding Temporal Annotations and Associated Verification to Ravenscar Profile

  2003cites this paper
• Proof Rules for Automated Compositional Verification through Learning

  2003cites this paper
• Design by contract - Deontic design language forcomponent-based systems

  2003cites this paper
• SAVCBS 2003: Specification and Verification of Component-Based Systems

  2003cites this paper
• A Compositional Protocol Verification Using Relativized Bisimulation

  2003cites this paper
• Compositional verification: an industrial case study

  2003cites this paper
• Thread-Modular Verification for Shared-Memory Programs

  2002cites this paper
• Dependable Distributed Objects

  2001cites this paper
• Thread-Modular Verification For

  2001cites this paper
• Foundations for Circular Compositional Reasoning

  2001cites this paper
• Verifying Network Protocol Implementations by Symbolic Refinement Checking

  2001cites this paper
• Resettable Vector Clocks: A Case Study in Designing Graybox Fault-Tolerance

  2000cites this paper
• Enhancing the tractability of rely/guarantee specifications in the development of interfering operations

  2000cites this paper
• On the completeness of compositional reasoning

  2000cites this paper
• On the Competeness of Compositional Reasoning

  2000cites this paper
• Automated Refinement Checking for Asynchronous Processes

  2000cites this paper
• Modular refinement of hierarchic reactive machines

  2000cites this paper
• Assume-Guarantee Refinement Between Different Time Scales

  1999cites this paper
• Formal Verification of Explicitly Parallel Microprocessors

  1999cites this paper
• Assume-guarantee Reenement between Diierent Time Scales ?

  1999cites this paper
• Automating Modular Verification

  1999cites this paper
• Formal Justification of the Rely-Guarantee Paradigm for Shared-Variable Concurrency: A Semantic Approach

  1999cites this paper
• Automating Modular Veri cation

  1999cites this paper
• Tool Support for System Specification, Development and Verification

  1999cites this paper
• A timed semantics for a hierarchical design notation

  1999cites this paper
• Marsh:min-area retiming with setup and hold constraints

  1999cites this paper
• Assume-Guarantee Re nementBetween Di erent Time Scales ?

  1999cites this paper
• Algorithms and methodology for scalable model checking

  1999cites this paper
• Formal specification and verification of a dataflow processor array

  1999cites this paper