Abstract interpretation of reactive systems

No abstract is available for this paper.

• Publication year

  1997

• Venue

  ACM Transactions on Programming Languages and Systems

• Publication date

  1997-03-03

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/244795.244800
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Sometimes and Not Never Re-revisited: On Branching Versus Linear Time

  1998cited by this paper
• Abstract interpretation and partition refinement for model checking

  1996influential reference
• Abstraktionstechniken für automatische Verifikationsmethoden

  1996cited by this paper
• Statecharts

  1995influential reference
• Model Checking of Non-Finite State Processes by Finite Approximations

  1995cited by this paper
• Property preserving abstractions for the verification of concurrent systems

  1995cited by this paper
• Abstract interpretation of reactive systems : preservation of CTL*

  1995influential reference
• Optimality in Abstractions of Model Checking

  1995cited by this paper
• Verification of a Distributed Cache Memory by Using Abstractions

  1994cited by this paper
• Suspension analyses for concurrent logic programs

  1994cited by this paper
• Model Checking Using Adaptive State and Data Abstraction

  1994cited by this paper
• Abstract interpretation of reactive systems : abstractions preserving ..

  1994cited by this paper
• Abstract interpretation of reactive systems : abstractions preserving $\forall$CTL*, $\exists$CTL* and CTL*

  1994cited by this paper
• Abstractions for Preserving All CTL* Formulae

  1994cited by this paper
• Testing-Based Abstractions for Value-Passing Systems

  1994cited by this paper
• Automatic Veriication of Nite-state Concurrent Systems Using Temporal-logic Speciications. Acm

  1993cited by this paper
• Model checking, abstraction, and compositional verification

  1993cited by this paper
• Generation of Reduced Models for Checking Fragments of CTL

  1993cited by this paper
• A Tool for Symbolic Program Verification and Abstration

  1993cited by this paper
• Modal Logic, Transition Systems and Processes

  1993cited by this paper
• Model checking and abstraction

  1992cited by this paper
• Abstract Interpretation and Application to Logic Programs

  1992cited by this paper
• Minimal State Graph Generation

  1992cited by this paper
• Abstract Interpretation Frameworks

  1992cited by this paper
• CTL* and ECTL* as Fragments of the Modal µ-Calculus

  1992influential reference
• Guest editor's introduction to the special section on the third international conference on computer languages

  1992cited by this paper
• Property Preserving Simulations

  1992cited by this paper
• CTL* and ECTL* as Fragments of the Modal mu-Calculus

  1992cited by this paper
• Automatic Verification Methods for Finite State Systems: International Workshop, Grenoble, France. June 12-14, 1989. Proceedings

  1990cited by this paper
• Trace theory for automatic hierarchical verification of speed-independent circuits

  1989cited by this paper
• Analysis of Discrete Event Coordination

  1989cited by this paper
• Modal Specifications

  1989cited by this paper
• A modal process logic

  1988cited by this paper
• Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits

  1988cited by this paper
• Statecharts: A Visual Formalism for Complex Systems

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

  1986cited by this paper
• Automatic verification of finite-state concurrent systems using temporal logic specifications

  1986cited by this paper
• “Sometimes” and “not never” revisited: on branching versus linear time temporal logic

  1986cited by this paper
• Checking that finite state concurrent programs satisfy their linear specification

  1985cited by this paper
• Property Preserving Homomorphisms of Transition Systems

  1983cited by this paper
• Decentralization of process nets with centralized control

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

  1982cited by this paper
• Results on the Propositional µ-Calculus

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

  1981cited by this paper
• The Algebraic Theory of Automata

  1980cited by this paper
• On Observing Nondeterminism and Concurrency

  1980cited by this paper
• Systematic design of program analysis frameworks

  1979cited by this paper
• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

  1977influential reference
• An Algebraic Definition of Simulation Between Programs

  1971cited by this paper
• Chapter 5 – Coverings of Automata

  1968cited by this paper
• Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi

  1963cited by this paper

• The Modal Logic of Abstraction Refinement

  2026cites this paper
• Model Checking as Program Verification by Abstract Interpretation (Extended Version)

  2025cites this paper
• Practical Abstractions for Model Checking Continuous-Time Multi-Agent Systems

  2025cites this paper
• Coherent modal transition systems refinement

  2024cites this paper
• Systems of fixpoint equations: Abstraction, games, up-to techniques and local algorithms

  2024cites this paper
• Non-reducible Modal Transition Systems

  2023cites this paper
• Abstract Domains for Database Manipulating Processes

  2023cites this paper
• Simulation Relations and Applications in Formal Methods

  2022cites this paper
• Practical Abstraction for Model Checking of Multi-Agent Systems

  2022cites this paper
• Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs

  2022cites this paper
• the complexity of semantic self-minimization

  2022cites this paper
• Property-directed reachability as abstract interpretation in the monotone theory

  2021cites this paper
• Optimal Modular Control of Discrete Event Systems with Distinguishers and Approximations

  2021cites this paper
• Learning Semantic Representations to Verify Hardware Designs

  2021cites this paper
• Inference of Progressive Loop Invariants for Array Programs

  2020cites this paper
• Abstraction, Up-to Techniques and Games for Systems of Fixpoint Equations

  2020cites this paper
• Abstraction for Non-ground Answer Set Programs

  2019cites this paper
• Verification of embedded software models by combining abstract interpretation, symbolic execution and stability analysis

  2019cites this paper
• A Compass to Controlled Graph Rewriting

  2019cites this paper
• Verification of parallelising transformations of KPN models

  2019cites this paper
• Abstraction and Abstraction Refinement

  2018cites this paper
• Code Obfuscation Against Abstract Model Checking Attacks

  2018cites this paper
• Multi-valued Simulation and Abstraction Using Lattice Operations

  2017cites this paper
• Efficient abstraction algorithms for accelerating reconfiguration of VLSI arrays

  2017cites this paper
• 30 Years of Modal Transition Systems: Survey of Extensions and Analysis

  2017cites this paper
• Análisis de aplicaciones móviles utilizando métodos formales

  2017cites this paper
• An Abstraction-Refinement Methodology for Reasoning about Network Games

  2017cites this paper
• Comprehensive failure characterization

  2017cites this paper
• Aalborg Universitet 20 Years of Modal and Mixed Specifications

  2016influential citation
• Efficient family-based model checking via variability abstractions

  2016cites this paper
• Verification methodologies for fault-tolerant Network-on-Chip systems

  2016cites this paper
• Model checking linear temporal logic of rewriting formulas under localized fairness

  2015cites this paper
• Lattice-Based Semantics for Combinatorial Model Evolution

  2015cites this paper
• Family-Based Model Checking Without a Family-Based Model Checker

  2015cites this paper
• Refinement checking on parametric modal transition systems

  2015cites this paper
• ABSTRACTIONS ANDREDUCTIONS INMODEL CHECKING

  2015cites this paper
• Modal Transition Systems as the Basis for Interface Theories and Product Lines

  2015cites this paper
• Universit a degli Studi di Udine Dipartimento di Matematica e Informatica Dottorato di Ricerca in Informatica

  2014cites this paper
• Bounded model checking for asynchronous concurrent systems

  2014cites this paper
• May/Must Abstraction-Based Software Model Checking for Sound Verification and Falsification

  2014cites this paper
• An Abstract Interpretation Framework for Diagnosis and Verification of Timed Concurrent Constraint Languages

  2014cites this paper
• Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom

  2014cites this paper
• Quantitative Analysis of Lattice-valued Kripke Structures

  2014cites this paper
• Dimming Relations for the Efficient Analysis of Concurrent Systems via Action Abstraction

  2014cites this paper
• Mixed Simulation of Multi-valued Models

  2014cites this paper
• Making abstract models complete †

  2014cites this paper
• An Algorithm for Compositional Nonblocking Verification of Extended Finite-State Machines

  2014cites this paper
• On Refinements of Boolean and Parametric Modal Transition Systems

  2013cites this paper
• Model Checking GSM-Based Multi-Agent Systems

  2013cites this paper
• Parameterized model checking of fault-tolerant distributed algorithms by abstraction

  2013cites this paper
• Symbolic Model Checking for Incomplete Designs with Flexible Modeling of Unknowns

  2013cites this paper
• Performance guarantees for C-WMD robot missions

  2013cites this paper
• Synthesis and control of infinite-state systems with partial observability

  2013cites this paper
• An analysis for proving probabilistic termination of biological systems

  2013cites this paper
• Foundations of the Bandera Abstraction Tools

  2013cites this paper
• On the Use of Model Checking for the Bounded and Unbounded Verification of Nonblocking Concurrent Data Structures

  2013cites this paper
• Automated program generation Bridging the gap between model and implementation

  2012cites this paper
• Temporal-logic property preservation under Z refinement

  2012cites this paper
• Formal development of control software in the medical systems domain

  2012cites this paper
• A Theory of History Dependent Abstractions for Learning Interface Automata

  2012cites this paper
• Probabilistic model checking of biological systems with uncertain kinetic rates

  2012cites this paper
• Expressiveness and Completeness in Abstraction

  2012cites this paper
• Model Checking LTLR Formulas under Localized Fairness

  2012cites this paper
• Weak Alphabet Merging of Partial Behavior Models

  2012cites this paper
• A logical verification methodology for service-oriented computing

  2012cites this paper
• Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms

  2012cites this paper
• Inverse-limit and topological aspects of abstract interpretation

  2012cites this paper
• On Conditions for Modular Verification in Systems of Synchronising Components

  2012cites this paper
• Logics and Algorithms for Verification of Concurrent Systems

  2012cites this paper
• Auto-Generation of Test Cases for Infinite States Reactive Systems Based on Symbolic Execution and Formula Rewriting

  2012cites this paper
• Matching and Merging of Variant Feature Specifications

  2012cites this paper
• Supporting incremental behaviour model elaboration

  2012cites this paper
• Abstract Model Repair

  2012cites this paper
• Model Checking on Hybrid Automata

  2012cites this paper
• Verification of P2P live streaming systems using symmetry-based semiautomatic abstractions

  2012cites this paper
• An abstract interpretation framework for semantics and diagnosis of Lazy functional-logic languages

  2012cites this paper
• Modal Process Rewrite Systems

  2012cites this paper
• Improving Reachability Analysis of Infinite State Systems by Specialization

  2011cites this paper
• Abstract Probabilistic Semantics for the Analysis of Biological Systems Models PhD Program in Computer Science and Engineering XXIII Cycle

  2011cites this paper
• A Modal Interface Theory for Component-based Design

  2011cites this paper
• Modal abstractions of concurrent behavior

  2011cites this paper
• Categorical logics for contravariant simulations, partial bisimulations, modal refinements and mixed transition systems ⋆

  2011cites this paper
• Component-based systems : from design to implementation

  2011cites this paper
• Finite-state abstractions for probabilistic computation tree logic

  2011cites this paper
• Parameterized verification of deadlock freedom in symmetric cache coherence protocols

  2011cites this paper
• Specification guidelines to avoid the state space explosion problem

  2011cites this paper
• Component-based systems : from design to implementation. (Systèmes à base de composants : du design à l'implémentation)

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

  2011cites this paper
• State/Event-Based LTL Model Checking under Parametric Generalized Fairness

  2011cites this paper
• Modular Verification of Biological Systems

  2011influential citation
• Soundness verification for conceptual workflow nets with data: Early detection of errors with the most precision possible

  2011cites this paper
• On the consistency, expressiveness, and precision of partial modeling formalisms

  2011cites this paper
• Workflow Soundness Revisited: Checking Correctness in the Presence of Data While Staying Conceptual

  2010cites this paper
• Modular Verification of Interactive Systems with an Application to Biology

  2010influential citation
• Robust Vacuity for Branching Temporal Logic

  2010cites this paper
• Modelling Distributed Systems

  2010cites this paper
• Modelling and Analysis of Real Time Systems with Logic Programming and Constraints

  2010influential citation
• Process Algebra for Modal Transition Systemses

  2010cites this paper
• Modular Verication of Interactive Systems with Application to Biology

  2010cites this paper
• Improved model checking of hierarchical systems

  2010cites this paper