Cubicle

swMATH13778MaRDI QIDQ25690FDOQ25690

Author name not available (Why is that?)

Official website: http://link.springer.com/chapter/10.1007/978-3-642-31424-7_55

Described by source

• Cubicle-\(\mathcal{W}\): parameterized model checking on weak memory

Cited In (33)

• Declarative parameterized verification of distributed protocols via the Cubicle model checker
• Sound verification procedures for temporal properties of infinite-state systems
• Checking deadlock-freedom of parametric component-based systems
• SMT-based verification of data-aware processes: a model-theoretic approach
• Universal invariant checking of parametric systems with quantifier-free SMT reasoning
• On the combination of polyhedral abstraction and SMT-based model checking for Petri nets
• An automatic proving approach to parameterized verification
• Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications
• Parameterized model checking on the TSO weak memory model
• On invariant synthesis for parametric systems
• A non-linear arithmetic procedure for control-command software verification
• D-Finder
• TLA
• ASASP
• Verification of composed array-based systems with applications to security-aware workflows
• PlusCal
• Memorax
• CSP-prover
• Mcmt
• ParaVerifier
• H-PILoT
• SAFARI
• Booster
• VERIFAS
• Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
• A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking
• From model completeness to verification of data aware processes
• Model completeness, covers and superposition
• Structural Invariants for the Verification of Systems with Parameterized Architectures
• Parameterized synthesis of self-stabilizing protocols in symmetric networks
• Property-directed inference of universal invariants or proving their absence
• Ivy
• ParaVerifier: an automatic framework for proving parameterized cache coherence protocols

This page was built for software: Cubicle