Compositional State Space Generation from Lotos Programs

No abstract is available for this paper.

• Publication year

  1997

• Venue

  International Conference on Tools and Algorithms for Construction and Analysis of Systems

• Publication date

  1997-04-02

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/BFb0035392
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Theories of Programming Languages: Communicating Sequential Processes

  1998cited by this paper
• Specification and Verification of Various Distributed Leader Election Algorithms for Unidirectional Ring Networks

  1997cited by this paper
• Compositionality in State Space Verification Methods

  1996cited by this paper
• CADP - A Protocol Validation and Verification Toolbox

  1996cited by this paper
• Compositional reachability analysis of finite-state distributed systems with user-specified constraints

  1995cited by this paper
• Symbolic Equivalence Checking

  1993cited by this paper
• Enhancing compositional reachability analysis with context constraints

  1993cited by this paper
• Specification Styles in Distributed Systems Design and Verification

  1991cited by this paper
• Calculus of Communicating Systems

  1991cited by this paper
• Design and validation of computer protocols

  1991cited by this paper
• An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence

  1990cited by this paper
• An Implementation of an Efficient Algorithm for Bisimulation Equivalence

  1990cited by this paper
• The Concurrency Workbench

  1990cited by this paper
• Back and Forth Bisimulations

  1990cited by this paper
• MEC: A System for Constructing and Analysis Transition Systems

  1990cited by this paper
• Auto/Autograph

  1990cited by this paper
• Branching Time and Abstraction in Bisimulation Semantics (Extended Abstract)

  1989cited by this paper
• On the Use of Specifiation Styles in the Design of Distributed Systems (Abstract)

  1989cited by this paper
• Three Partition Refinement Algorithms

  1987cited by this paper
• A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour

  1985cited by this paper
• CCS expressions, finite state processes, and three problems of equivalence

  1983cited by this paper
• Communicating sequential processes

  1983cited by this paper
• Application and Theory of Petri Nets

  1982cited by this paper
• Concurrency and Automata on Infinite Sequences

  1981cited by this paper
• A Calculus of Communicating Systems

  1980cited by this paper

• Compositional Model Checking of Consensus Protocols via Interaction-Preserving Abstraction

  2022cites this paper
• Calculating

  2021cites this paper
• Is CADP an Applicable Formal Method?

  2021cites this paper
• Testing Software and Systems: 32nd IFIP WG 6.1 International Conference, ICTSS 2020, Naples, Italy, December 9–11, 2020, Proceedings

  2020cites this paper
• Automated Transition Coverage in Behavioural Conformance Testing

  2020cites this paper
• Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities

  2020cites this paper
• Compositional model checking with divergence preserving branching bisimilarity is lively

  2020cites this paper
• Verification of concurrent systems in a model-driven engineering workflow

  2019cites this paper
• Compositional verification of concurrent systems by combining bisimulations

  2019cites this paper
• Compositional Verification in Action

  2018influential citation
• Formal Methods for Industrial Critical Systems

  2018cites this paper
• Model-Checking Synthesizable SystemVerilog Descriptions of Asynchronous Circuits

  2018cites this paper
• Compositional Model Checking Is Lively

  2017cites this paper
• Formal Aspects of Component Software

  2017cites this paper
• A Model-Based Approach to Combining Static and Dynamic Verification Techniques

  2016cites this paper
• An I/O Efficient Model Checking Algorithm for Large-Scale Systems

  2015cites this paper
• Compositional specification and reachability checking of net systems

  2015cites this paper
• Compositional Model Checking of Concurrent Systems

  2015cites this paper
• Formal Methods for Functional Verification of Cache-Coherent System-on-Chip. (Méthodes Formelles pour la vérification fonctionnelle des systèmes sur puce cache cohérent)

  2015cites this paper
• Compositional verification of asynchronous concurrent systems using CADP

  2015influential citation
• Modular Minimization of Finite State Machines

  2015cites this paper
• Local state space construction for compositional verification of concurrent systems

  2014cites this paper
• Modular µ-Calculus Model-Checking with Formula-Dependent Hierarchical Abstractions

  2014cites this paper
• Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols

  2013cites this paper
• CADP 2011: a toolbox for the construction and analysis of distributed processes

  2012cites this paper
• A Compositional Minimization Approach for Large Asynchronous Design Verification

  2012cites this paper
• Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems

  2012cites this paper
• Semantics and Analysis of Scenario-Aware Dataflow Specifications

  2011cites this paper
• Smart Reduction

  2011cites this paper
• Efficient, deterministic and deadlock-free concurrency

  2011cites this paper
• Compositional Reachability Analysis for Efficient Modular Verification of Asynchronous Designs

  2010cites this paper
• State space reductions for scalable verification of asynchronous designs

  2010cites this paper
• Modélisation et analyse des performances de la bibliothèque MPI en tenant compte de l'architecture matérielle

  2010cites this paper
• Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement

  2010cites this paper
• Modélisation et analyse des performances de la bibliothèque MPI en tenant compte de l'architecture matérielle. (Modeling and performance analysis of the MPI library by taking into account the hardware architecture)

  2010cites this paper
• Approximation and Refinement Techniques for Hard Model-checking Problems

  2009cites this paper
• Fighting State Space Explosion: Review and Evaluation

  2009cites this paper
• A coordinated reachability analysis method for modular verification of asynchronous designs

  2009cites this paper
• Partial Order Reductions Using Compositional Confluence Detection

  2009cites this paper
• An Efficient LOTOS-Based Framework for Describing and Solving (Temporal) CSPs

  2009cites this paper
• Automated Interface Refinement for Compositional Verification

  2009cites this paper
• Compositional deadlock detection for rendezvous communication

  2009cites this paper
• A Compositional Method With Failure-Preserving Abstraction for Asynchronous Design Verification

  2008cites this paper
• Assume-Guarantee Verification for Interface Automata

  2008cites this paper
• Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning

  2008cites this paper
• Refining Interface Alphabets for Compositional Verification

  2007cites this paper
• A Compositional Approach to Asynchronous Design Verification with Automated State Space Reduction

  2007cites this paper
• Automatic interface generation for compositional verification

  2007cites this paper
• Learning to Divide and Conquer

  2007cites this paper
• Automatic Interface Generation for Enumerative Model Checking Computer Science Annual Workshop 2006

  2007influential citation
• The saturation algorithm for symbolic state-space exploration

  2006cites this paper
• Interfaces for Compositional Verication

  2006cites this paper
• Towards a Compositional SPIN

  2006cites this paper
• Proceedings of CSAW'06

  2006cites this paper
• Reduction and Abstraction Techniques for Model Checking

  2006cites this paper
• Refined Interfaces for Compositional Verification

  2006influential citation
• Automatic interface generation for enumerative model checking

  2006cites this paper
• On-the-fly State Space Reductions

  2005cites this paper
• Improving Lotos simulation using constraint propagation

  2005cites this paper
• Exp.Open 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-y Verication Methods

  2005influential citation
• Component Verification with Automatically Generated Assumptions

  2005cites this paper
• Exp.Open 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-The-Fly Verification Methods

  2005cites this paper
• Project-Team VASY Validation of Systems

  2004cites this paper
• Behaviour Analysis of Distributed Systems Using the Tracta Approach

  2004cites this paper
• A Learning Framework for Automatic Assume-Guarantee Verification

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

  2003cites this paper
• Learning Assumptions for Compositional Verification

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

  2003cites this paper
• Calculating-Confluence Compositionally

  2003cites this paper
• Äääöòòòò ××ùñôøøóò× Óö Óñôó××øøóòòð Îöö¬ Blockin Blockinøøóò

  2003cites this paper
• Compositional Verification Using CADP of the ScalAgent Deployment Protocol for Software Components

  2003cites this paper
• Computer-aided verification : how to trust a machine with your life

  2003cites this paper
• Validation of Systems

  2003cites this paper
• Compositional Verication using CADP of the ScalAgent Deployment Protocol for Software Components

  2003cites this paper
• Compositional Verification Using SVL Scripts

  2002cites this paper
• Assumption generation for software component verification

  2002cites this paper
• Formally verified, rapid prototyping for Air Traffic Control

  2002cites this paper
• Analysis of erroneous actions in the design of critical systems

  2001cites this paper
• An overview of CADP 2001

  2001cites this paper
• System design of a CC-NUMA multiprocessor architecture using formal specification, model-checking, co-simulation, and test generation

  2001cites this paper
• SVL: A Scripting Language for Compositional Verification

  2001cites this paper
• Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications

  2001cites this paper
• Declarative support for prototyping interactive systems

  2001cites this paper
• Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems

  2000cites this paper
• Model checking for concurrent software architectures

  1999cites this paper
• Behavioral analysis of software architectures using LTSA

  1999cites this paper
• \next" Heuristic for On-the--y Model Checking

  1999cites this paper
• Behaviour Analysis of Software Architectures

  1999cites this paper
• Modelling for Mere Mortals

  1999cites this paper
• "Next" Heuristic for On-the-Fly Model Checking

  1999cites this paper
• Advanced modelling and verification techniques applied to a cluster file system

  1999cites this paper
• for Concurrent Software Architectures

  1999cites this paper
• IF: An intermediate representation for SDL and its applications

  1999cites this paper
• Analysis of Software Architectures

  1999cites this paper
• IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems

  1999cites this paper
• Software architecture directed behaviour analysis

  1998influential citation
• Testing concurrency and communication in distributed objects

  1998cites this paper
• OPEN/CÆSAR: An OPen Software Architecture for Verification, Simulation, and Testing

  1998cites this paper
• Protocol verification with the ALDÉBARAN toolset

  1997influential citation
• Cadp'97 { Status, Applications and Perspectives

  1997cites this paper