scientific article
From MaRDI portal
Publication:2769579
zbMath0978.68539MaRDI QIDQ2769579
Sitvanit Ruah, Lenore D. Zuck, Amir Pnueli
Publication date: 5 February 2002
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2031/20310082
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (25)
Structural Invariants for the Verification of Systems with Parameterized Architectures ⋮ Sound verification procedures for temporal properties of infinite-state systems ⋮ Compositional analysis for verification of parameterized systems ⋮ Model checking and abstraction to the aid of parameterized systems (a survey) ⋮ Control of parameterized discrete event systems ⋮ Compositional Reasoning ⋮ Model Checking Parameterized Systems ⋮ Compositional verification of smart contracts through communication abstraction ⋮ Synthesis of large dynamic concurrent programs from dynamic specifications ⋮ Unnamed Item ⋮ Verification of SMT systems with quantifiers ⋮ Synthesizing history and prophecy variables for symbolic model checking ⋮ Invariants for Parameterised Boolean Equation Systems ⋮ Parametrized invariance for infinite state processes ⋮ Checking deadlock-freedom of parametric component-based systems ⋮ Invariants for parameterised Boolean equation systems ⋮ Verification of parametric concurrent systems with prioritised FIFO resource management ⋮ Liveness by Invisible Invariants ⋮ Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems ⋮ Universal invariant checking of parametric systems with quantifier-free SMT reasoning ⋮ Automatic Verification of Directory-Based Consistency Protocols ⋮ Abstract Counterexamples for Non-disjunctive Abstractions ⋮ Local proofs for global safety properties ⋮ Automated formal analysis and verification: an overview ⋮ Specification and verification of concurrent programs through refinements
Uses Software
This page was built for publication:
