Sound verification procedures for temporal properties of infinite-state systems
From MaRDI portal
Publication:832273
DOI10.1007/978-3-030-81688-9_16zbMATH Open1493.68219OpenAlexW3180354117MaRDI QIDQ832273FDOQ832273
David Chemouil, Julien Brunel, Quentin Peyras, Jean-Paul Bodeveix
Publication date: 25 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-81688-9_16
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
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Cites Work
- Cubicle-\(\mathcal{W}\): parameterized model checking on weak memory
- Title not available (Why is that?)
- Title not available (Why is that?)
- Decidable fragments of first-order temporal logics
- Title not available (Why is that?)
- An improved algorithm for decentralized extrema-finding in circular configurations of processes
- Title not available (Why is that?)
- On finite domains in first-order linear temporal logic
- Monodic Fragments of First-Order Temporal Logics: 2000–2001 A.D.
- A decidable and expressive fragment of Many-Sorted 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
Uses Software
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)
