Sound verification procedures for temporal properties of infinite-state systems
From MaRDI portal
(Redirected from Publication:832273)
Recommendations
- A decidable and expressive fragment of many-sorted first-order linear temporal logic
- A bounded domain property for an expressive fragment of first-order linear temporal logic
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- \textsc{tlpvs}: A \textsc{pvs}-based \textsc{ltl} verification system
- scientific article; zbMATH DE number 1377375
Cites work
- scientific article; zbMATH DE number 1701752 (Why is no real title available?)
- scientific article; zbMATH DE number 1796136 (Why is no real title available?)
- A decidable and expressive fragment of many-sorted first-order linear temporal logic
- An improved algorithm for decentralized extrema-finding in circular configurations of processes
- Convergent and commutative replicated data types
- Cubicle-\(\mathcal{W}\): parameterized model checking on weak memory
- Decidable fragments of first-order temporal logics
- Modeling in Event B. System and software engineering.
- Monodic fragments of first-order temporal logics: 2000--2001 A.D.
- On finite domains in first-order linear temporal logic
- Parameterized model checking on the TSO weak memory model
- Proving liveness of parameterized programs
- Thread modularity at many levels: a pearl in compositional verification
Cited in
(2)
This page was built for publication: Sound verification procedures for temporal properties of infinite-state systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832273)
