Constraint-Based Verification of Parameterized Cache Coherence Protocols

No abstract is available for this paper.

• Publication year

  2003

• Venue

  Formal Methods Syst. Des.

• Publication date

  2003-11-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1023/A:1026276129010
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• An approach to automating the verification of compact parallel coordination programs. I

  2018cited by this paper
• Abstract Regular Model Checking

  2004cited by this paper
• Well-structured transition systems everywhere!

  2001cited by this paper
• Ensuring completeness of symbolic verification methods for infinite-state systems

  2001cited by this paper
• Symbolic model checking with rich assertional languages

  2001cited by this paper
• Attacking Symbolic State Explosion

  2001cited by this paper
• Automatic Deductive Verification with Invisible Invariants

  2001cited by this paper
• Constraint-Based Verification of Client-Server Protocols

  2001cited by this paper
• Parameterized Verification with Automatically Computed Inductive Assertions

  2001cited by this paper
• Liveness and Acceleration in Parameterized Verification

  2000cited by this paper
• Automatic Verification of Parameterized Cache Coherence Protocols

  2000cited by this paper
• Cache Memory

  2000influential reference
• FMona: A Tool for Expressing Validation Techniques over Infinite State Systems

  2000cited by this paper
• Better is better than well: on efficient verification of infinite-state systems

  2000cited by this paper
• On the verification of broadcast protocols

  1999influential reference
• Model Checking in CLP

  1999influential reference
• Verification of Infinite State Systems by Compositional Model Checking

  1999cited by this paper
• Characterization of a sequentially consistent memory and verification of a cache memory by abstraction

  1999cited by this paper
• Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems

  1999cited by this paper
• Handling Global Conditions in Parameterized System Verification

  1999cited by this paper
• Constraint-Based Analysis of Broadcast Protocols

  1999influential reference
• Verifying Systems with Replicated Components in Murϕ

  1999cited by this paper
• On model checking for non-deterministic infinite-state systems

  1998influential reference
• Îöööýýòò Ëý×øøñ× Ûûøø Áò¬òòøø Ùø Êêêùððö Ëøøøø Ëôô Blockin Blockin× Èèèööö Ïóðôö¸öòòöö Óóóóðóø Íòòúö××ø Ää Áò×øøøùø Åóòøø¬óöö¸¾¾ ¹¹¼¼¼ Ää Ëëöø¹ììðññò¸ðððùñ

  1998cited by this paper
• Verification techniques for cache coherence protocols

  1997cited by this paper
• Verifying parameterized networks

  1997influential reference
• Automatic verification of parameterized linear networks of processes

  1997cited by this paper
• Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic

  1997influential reference
• Construction of Abstract State Graphs with PVS

  1997cited by this paper
• Symbolic Model Checking with Rich ssertional Languages

  1997influential reference
• Verification of Real-Time Systems using Linear Relation Analysis

  1997cited by this paper
• Automatic generation of functional vectors using the extended finite state machine model

  1996influential reference
• Verifying Systems with Replicated Components in Murphi

  1996cited by this paper
• General decidability theorems for infinite-state systems

  1996influential reference
• A New Approach for the Verification of Cache Coherence Protocols

  1995influential reference
• HYTECH: the next generation

  1995influential reference
• Delay Analysis in Synchronous Programs

  1993cited by this paper
• The cache memory book

  1993influential reference
• Verification of the Futurebus+ cache coherence protocol

  1993cited by this paper
• Reasoning about systems with many processes

  1992cited by this paper
• THEORY OF LINEAR AND INTEGER PROGRAMMING (Wiley-Interscience Series in Discrete Mathematics and Optimization)

  1989influential reference
• Reasoning about networks with many identical finite-state processes

  1986cited by this paper
• Theory of linear and integer programming

  1986cited by this paper
• Cache coherence protocols: evaluation using a multiprocessor simulation model

  1986influential reference
• Petri Nets and Large Finite Sets

  1984cited by this paper
• A low-overhead coherence solution for multiprocessors with private cache memories

  1984cited by this paper
• Parallel Program Schemata

  1969cited by this paper

• Verification of the Release-Acquire Semantics

  2025cites this paper
• Parameterized Verification of Leader/Follower Systems via Arithmetic Constraints

  2024cites this paper
• Regular Model Checking Upside-Down: An Invariant-Based Approach

  2022cites this paper
• Parameterized verification of leader/follower systems via first-order temporal logic

  2021cites this paper
• An Overview of Verification and Validation Challenges for Inspection Robots

  2021cites this paper
• Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker

  2021cites this paper
• Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems

  2020cites this paper
• Synthesizing safe coalition strategies

  2020cites this paper
• Multi-scale verification of distributed synchronisation

  2020cites this paper
• Boosting Sequential Consistency Checking Using Saturation

  2020cites this paper
• A formal model of data access for multicore architectures with multilevel caches

  2019cites this paper
• Gradual Consistency Checking

  2019cites this paper
• Formal Modeling and Verification of a Victim DRAM Cache

  2019cites this paper
• Concurrent Parameterized Games

  2019cites this paper
• Declarative Parameterized Verification of Topology-Sensitive Distributed Protocols

  2018cites this paper
• Multi-scale verification of distributed synchronisation

  2018cites this paper
• Second Order Quantifier Elimination: Towards Verification Applications

  2017cites this paper
• Counter Simulations via Higher Order Quantifier Elimination: a preliminary report

  2017cites this paper
• A Formal Model of Parallel Execution on Multicore Architectures with Multilevel Caches

  2017cites this paper
• Adding Data Registers to Parameterized Networks with Broadcast

  2016cites this paper
• An operational semantics of cache coherent multicore architectures

  2016cites this paper
• Counter Abstractions in Model Checking of Distributed Broadcast Algorithms: Some Case Studies

  2016cites this paper
• A unified view of parameterized verification of abstract models of broadcast communication

  2016cites this paper
• Parameterized verification

  2016cites this paper
• Specification, verification, and synthesis using extended state machines with callbacks

  2016cites this paper
• A Maude Framework for Cache Coherent Multicore Architectures

  2016cites this paper
• Productive Design of Extensible On-Chip Memory Hierarchies

  2016cites this paper
• ω-Petri Nets: Algorithms and Complexity

  2015cites this paper
• First-order logic for safety verification of hedge rewriting systems

  2015cites this paper
• Model Checking TLR* Guarantee Formulas on Infinite Systems

  2014cites this paper
• Inference of polynomial invariants for imperative programs

  2014cites this paper
• Parameterized Verification and Model Checking for Distributed Broadcast Protocols

  2014cites this paper
• ω-Petri Nets

  2013cites this paper
• VFCC: A verification framework of cache coherence using parallel simulation

  2013cites this paper
• Parameterized Verification of Broadcast Networks of Register Automata

  2013cites this paper
• Push-Down Automata with Gap-Order Constraints

  2013cites this paper
• Finite Reasons for Safety

  2013cites this paper
• Decidability and Complexity Results for Verification of Asynchronous Broadcast Networks

  2013cites this paper
• Elimination Techniques for Program Analysis

  2013influential citation
• Formal verification of on-chip communication fabrics

  2013cites this paper
• Finite Models vs Tree Automata in Safety Verification

  2012cites this paper
• State space reduction in modeling checking parameterized cache coherence protocol by two-dimensional abstraction

  2012cites this paper
• Three Case Studies on Verification of Infinite-State Systems

  2012cites this paper
• A lightweight regular model checking approach for parameterized systems

  2012cites this paper
• Towards the formal verification of cache coherency at the architectural level

  2012cites this paper
• Analysing robot swarm behaviour via probabilistic model checking

  2012cites this paper
• Automatic verification of counter systems via domain-specific multi-result supercompilation

  2012cites this paper
• Inference of polynomial invariants for imperative programs: A farewell to Gröbner bases

  2012cites this paper
• Implementing a domain- specific multi-result supercompiler by means of the MRSC toolkit

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

  2011cites this paper
• Automatic Verification of Directory-Based Consistency Protocols with Graph Constraints

  2011cites this paper
• First-order finite satisfiability vs tree automata in safety verification

  2011cites this paper
• Parameterized Cache Coherence Protocol Verification using Invariant

  2011cites this paper
• Attacking the Dimensionality Problem of Parameterized Systems via Bounded Reachability Graphs

  2011cites this paper
• Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation

  2010cites this paper
• Finite Model Finding for Parameterized Verification

  2010cites this paper
• GENERALIZATION STRATEGIES FOR THE VERIFICATION OF INFINITE STATE SYSTEMS R . 10-21 , 2010

  2010cites this paper
• Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol

  2010cites this paper
• Specification-based Verification in a Distributed Shared Memory Simulation Model

  2010influential citation
• Reachability as Derivability, Finite Countermodels and Verification

  2010influential citation
• Algorithmic multiparameterised verification of safety properties:process algebraic approach

  2010cites this paper
• Automatic Verification of Directory-Based Consistency Protocols

  2009cites this paper
• Temporal Verification of Fault-Tolerant Protocols

  2009cites this paper
• Approximated Context-Sensitive Analysis for Parameterized Verification

  2009cites this paper
• Action Language verifier: an infinite-state model checker for reactive software specifications

  2009influential citation
• A Java Supercompiler and Its Application to Verification of Cache-Coherence Protocols

  2009cites this paper
• Concurrency control generation for dynamic threads using Discrete-Event Systems

  2009cites this paper
• Heuristic Symbolic Verification of Safety Properties for Parameterized Systems: Heuristic Symbolic Verification of Safety Properties for Parameterized Systems

  2009cites this paper
• Verification as Specialization of Interpreters with Respect to Data

  2008cites this paper
• Reachability Analysis in Verification via Supercompilation

  2008cites this paper
• Formal verification along with design for transactional models

  2008cites this paper
• Tests and Proofs : Papers Presented at the Second International Conference TAP 2008 Prato , Italy , April 2008

  2008cites this paper
• Istituto Di Analisi Dei Sistemi Ed Informatica Consiglio Nazionale Delle Ricerche

  2008cites this paper
• Verifying Parameterized Protocols by Transforming Strati ed Logic Programs ( Preliminary Version )

  2008cites this paper
• Practical First-Order Temporal Reasoning

  2008influential citation
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation

  2007influential citation
• Verification of infinite state systems using Presburger arithmetic

  2007influential citation
• Rewriting systems with data a framework for reasoning about systems with unbounded structures over infinite data domains

  2007cites this paper
• Rewriting Systems with Data

  2007cites this paper
• Efficient First-Order Temporal Logic for Infinite-State Systems

  2007cites this paper
• Transformational Veri(cid:28)cation of Parameterized Protocols Using Array Formulas

  2005cites this paper
• Towards Verification via Supercompilation

  2005cites this paper
• The Affine Hull of a Binary Automaton is Computable in Polynomial Time

  2004cites this paper
• Monodic ASMs and Temporal Verification

  2004cites this paper
• Temporal verification with transition invariants

  2004cites this paper
• Speci cation-Based Parameter-Model Interaction: Towards a Correct Re ection of Memory Characteristics in a DSM Cluster Simulation

  2003cites this paper
• Constraint-Based Model Checking for Parameterized Synchronous Systems

  2002cites this paper
• Under Consideration for Publication in Theory and Practice of Logic Programming Generalization Strategies for the Verification of Infinite State Systems

  year unknowncites this paper
• Automatic Verification of Counter Systems via Domain- Specific Multi-result Supercompilation Automatic Verification of Counter Systems via Domain-specific Multi-result Supercompilation. Keldysh Automatic Verification of Counter Systems via Domain-specific Multi-result Supercompilation Moscow 2012

  year unknowncites this paper