Handling global conditions in parameterized system verification

DOI10.1007/3-540-48683-6_14MaRDI QIDQ4817539zbMATH OpenFDO

Authors Ahmed Bouajjani, Marcus Nilsson, Parosh A. Abdulla, Bengt Jonsson

Publication date 24 September 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48683-6_14

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Parameterized Verification of Infinite-State Processes with Global Conditions
• Handling Parameterized Systems with Non-atomic Global Conditions
• Approximated parameterized verification of infinite-state processes with global conditions
• Liveness and acceleration in parameterized verification
• MONOTONIC ABSTRACTION: ON EFFICIENT VERIFICATION OF PARAMETERIZED SYSTEMS

Cited in

(21)

• Approximated parameterized verification of infinite-state processes with global conditions
• Iterating transducers
• Model checking and abstraction to the aid of parameterized systems (a survey)
• Parameterized verification of systems with global synchronization and guards
• Computable fixpoints in well-structured symbolic model checking
• Verification of parametric concurrent systems with prioritised FIFO resource management
• Verification of programs with half-duplex communication
• Verification of \(\mathrm{EB}^3\) specifications using CADP
• Exact acceleration of real-time model checking
• Regular model checking using widening techniques
• Verifying a network invariant for all configurations of the Futurebus+ cache coherence protocol
• Networks of processes with parameterized state space
• Parametrized invariance for infinite state processes
• Bounded communication reachability analysis of process rewrite systems with ordered parallelism
• Parameterized Verification of Infinite-State Processes with Global Conditions
• Handling Parameterized Systems with Non-atomic Global Conditions
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Model checking, synthesis, and learning
• Regular model checking revisited
• Symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates
• Permutation rewriting and algorithmic verification

This page was built for publication: Handling global conditions in parameterized system verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4817539)