Composition: A Way to Make Proofs Harder

No abstract is available for this paper.

• Publication year

  1997

• Venue

  The Composer

• Publication date

  1997-09-08

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/3-540-49213-5_15
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• How to Write a Proof

  1995cited by this paper
• Conjoining specifications

  1995cited by this paper
• The temporal logic of actions

  1994cited by this paper
• Lazy caching

  1993cited by this paper
• Verification of a Multiplier: 64 Bits and Beyond

  1993cited by this paper
• The existence of refinement mappings

  1988cited by this paper
• Defining Liveness

  1984cited by this paper
• A Personal Summary of the Gries—Owicki Theory

  1982cited by this paper
• Proving the Correctness of Multiprocess Programs

  1977cited by this paper
• Proving Assertions about Parallel Programs

  1975cited by this paper

• Composition and Declassification in Possibilistic Information Flow Security

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

  2018cites this paper
• Hiding variables when decomposing specifications into GR(1) contracts

  2017cites this paper
• Programming and proving with distributed protocols

  2017cites this paper
• 1 Programming and Proving with Distributed Protocols

  2017cites this paper
• Control design for hybrid systems with TuLiP: The Temporal Logic Planning toolbox

  2016cites this paper
• Hoare-style specifications as correctness conditions for non-linearizable concurrent objects

  2015cites this paper
• Refinement and Composition in Formal Modeling of Temporal Systems

  2015cites this paper
• Verifying a simplification of mutual exclusion by Lycklama–Hadzilacos

  2013influential citation
• Dependable reuse & guarded integration of automotive software components

  2013cites this paper
• Model Checking in Bits and Pieces

  2013cites this paper
• Modeling Techniques for High Dependability Protocols and Architecture

  2012cites this paper
• Una contribución a las técnicas avanzadas de verificación de procesos de negocio y sistemas software abiertos

  2011cites this paper
• Ten Years of Analyzing Actors: Rebeca Experience

  2011cites this paper
• Event-B development of the FindP program

  2010cites this paper
• Using Compositionality to Formally Model and Analyze Systems Built of a High Number of Components

  2010cites this paper
• Event-B Decomposition for Parallel Programs

  2010cites this paper
• Event-B development of the FindP program

  2009cites this paper
• ACM SIGACT News Distributed Computing Column 30 On Distributed Computing Principles in Systems Research

  2008cites this paper
• Modularity: a first class concept to address distributed systems

  2008cites this paper
• Óñôóòòòø Òò Áòøøööö Êê¬òòññòø Ò Ðó×××¹ëý×øøñ Ëô Blockin Blockin¬ Blockin Blockinøøóò×

  2007cites this paper
• Proving linearisability of lock-free algorithms

  2007cites this paper
• Behavioral Compatibility Without State Explosion: Design and Verification of a Component-Based Elevator Control System

  2006cites this paper
• Proving correctness of highly-concurrent linearisable objects

  2006cites this paper
• Compositional Semantics of an Actor-Based Language Using Constraint Automata

  2006cites this paper
• Compositionality Made Up

  2006cites this paper
• Composing invariants

  2006cites this paper
• Rebeca: Theory, Applications, and Tools

  2006cites this paper
• Mechanizing compositional reasoning for concurrent systems: some lessons

  2005cites this paper
• Formal derivation of concurrent non-blocking algorithms for real-time systems Confirmation report

  2005cites this paper
• Model Checking, Automated Abstraction, and Compositional Verification of Rebeca Models

  2005cites this paper
• Automated compositional proofs for real-time systems

  2005cites this paper
• A. Common Notation

  2005cites this paper
• Compositional temporal logic based on partial order

  2004cites this paper
• Specification transformers: a predicate transformer approach to composition

  2004cites this paper
• Abstractions for Fault-Tolerant Distributed System Verification

  2004cites this paper
• Modeling and Verification of Reactive Systems using Rebeca

  2004cites this paper
• Decomposing Correctness Proofs of Fault-Tolerant Algorithms ?

  2004cites this paper
• Modeling and Verification of Reactive Systems using Rebeca

  2004cites this paper
• Composition of Temporal Logic Specifications

  2004cites this paper
• FORMAL SPECIFICATION AND VERIFICATION OF CONCURRENT AND REACTIVE SYSTEMS

  2004cites this paper
• Logic of involved variables - system specification with temporal logic of distributed actions

  2003cites this paper
• Distributed Object and Component-based Software Systems

  2003cites this paper
• Compositional Proofs for Real-Time Modular Systems

  2003cites this paper
• Mechanizing compositional reasoning for concurrent systems : some lessons

  2003cites this paper
• Composing Distributed Systems from Reusable Aspects of Behavior

  2002cites this paper
• Managing software evolution with a formalized abstraction hierarchy

  2002cites this paper
• Composing distributed systems from reusable aspects of behavior

  2002cites this paper
• High-Level Specifications: Lessons from Industry

  2002cites this paper
• An Approach to Composition Motivated by wp

  2002cites this paper
• An Extension to State Machine Modeling: The Concept of Coupled State Machines

  2001cites this paper
• Evolution based on Formalized Abstraction Hierarchy

  2001cites this paper
• SAVCBS 2001 Proceedings Specification and Verification of Component-Based Systems Workshop at OOPSLA 2001

  2001cites this paper
• Aspect-oriented specification architectures for distributed real-time systems

  2001cites this paper
• Toward Ontology-Based Component Composition

  2001cites this paper
• Facilities of practice reflecting abstractions of theory, and vice versa

  2001cites this paper
• Reasoning about Composition: A Predicate Transformer Approach

  2001cites this paper
• Dependable Distributed Objects

  2001cites this paper
• Reasoning about Composition : A Predicate Transformer Approach [ Position Paper ]

  2001cites this paper
• DESIGN AS THE DISCOVERY OF A MATHEMATICAL THEOREM WHAT DESIGNERS SHOULD KNOW ABOUT THE ART OF MATHEMATICS

  2000cites this paper
• Distributed system design with message sequence charts

  2000cites this paper
• Separating Product Variance and Domain Concepts in the Specification of Software Product Lines

  2000cites this paper
• Design Approach for Real-Time Reactive Systems

  1999cites this paper
• Distributed service composition

  1999cites this paper
• Component and Interface Renement in Closed-System Specications

  1999cites this paper
• Component and Interface Refinement in Closed-System Specifications

  1999cites this paper
• The two dimensions of an architecture

  1998cites this paper
• Harnessing the Power of Interaction

  1998cites this paper
• Decomposing Correctness Proofs of Fault-Tolerant Algorithms ( DRAFT ) ∗

  year unknowncites this paper