Incremental Invariant Generation for Compositional Design

No abstract is available for this paper.

• Publication year

  2010

• Venue

  2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering

• Publication date

  2010-08-25

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1109/TASE.2010.23
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Model Checking

  2018cited by this paper
• Omega Library

  2011influential reference
• D-Finder: A Tool for Compositional Deadlock Detection and Verification

  2009cited by this paper
• Compositional Verification for Component-Based Systems and Application

  2008influential reference
• Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning

  2008cited by this paper
• A Fast Linear-Arithmetic Solver for DPLL(T)

  2006influential reference
• Modeling Heterogeneous Real-time Components in BIP

  2006influential reference
• A framework for component-based construction

  2005cited by this paper
• Iterating Transducers in the Large (Extended Abstract)

  2003cited by this paper
• Composition for component-based modeling

  2002cited by this paper
• A framework for formal component-based software architecting

  2001cited by this paper
• An automata-theoretic approach to modular model checking

  2000cited by this paper
• NUSMV: a new symbolic model checker

  2000influential reference
• Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems

  2000cited by this paper
• Automatic Generation of Invariants

  1999cited by this paper
• Symbolic Methods for Exploring Infinite State Spaces

  1998cited by this paper
• CUDD: CU Decision Diagram Package Release 2.2.0

  1998cited by this paper
• A Compositional Rule for Hardware Design Refinement

  1997cited by this paper
• Reactive Modules

  1996cited by this paper
• Conjoining specifications

  1995cited by this paper
• The Omega Library

  1994cited by this paper
• All from One, One for All: on Model Checking Using Representatives

  1993cited by this paper
• Partial-Order Methods for Temporal Verification

  1993cited by this paper
• Model checking and modular verification

  1991cited by this paper
• Symbolic Model Checking: 10^20 States and Beyond

  1990cited by this paper
• Symbolic model checking: 1020 states and beyond

  1989cited by this paper
• Compositional model checking

  1989cited by this paper
• In Transition From Global to Modular Temporal Reasoning about Programs

  1989cited by this paper
• Parallel program design - a foundation

  1988cited by this paper
• Temporal Logic of Programs

  1987cited by this paper
• An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)

  1986cited by this paper
• Debugging Ada Tasking Programs

  1985cited by this paper
• A Proof Technique for Rely/Guarantee Properties

  1985cited by this paper
• Specification and verification of concurrent systems in CESAR

  1982cited by this paper

• A formal toolchain for offline and run-time verification of robotic systems

  2022cites this paper
• Component-based verification using incremental design and invariants

  2016cites this paper
• A Verifiable and Correct-by-Construction Controller for Robots in Human Environments

  2015cites this paper
• Correctness of Service Components and Service Component Ensembles

  2015cites this paper
• Petri nets for modeling robots

  2014cites this paper
• Unified Invariants for Cyber-Physical Switched System Stability

  2014cites this paper
• Stability of a Cyber-physical Smart Grid System Using Cooperating Invariants

  2013cites this paper
• Incremental Generation of Linear Invariants for Component-Based Systems

  2013influential citation
• Rigorous design of robot software: A formal component-based approach

  2012influential citation
• Efficient deadlock detection for concurrent systems

  2011influential citation
• D-Finder 2: Towards Efficient Correctness of Incremental Design

  2011cites this paper
• Invariants as a unified knowledge model for Cyber-Physical Systems

  2011cites this paper
• A Formal Approach for Incremental Construction with an Application to Autonomous Robotic Systems

  2011cites this paper
• A Verifiable and Correct-by-Construction Controller for Robot Functional Levels

  2011cites this paper
• Compositional and Incremental Modeling and Analysis for High-Confidence Distributed Embedded Control Systems

  2011cites this paper
• Incremental component-based construction and verification using invariants

  2010cites this paper
• Constructive Verification for Component-based Systems

  2010cites this paper