Sound verification procedures for temporal properties of infinite-state systems

DOI10.1007/978-3-030-81688-9_16zbMath1493.68219OpenAlexW3180354117MaRDI QIDQ832273

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Uses Software

• Coq
• Rodin
• Ivy
• Cubicle
• nuXmv
• Verdi
• IronFleet
• Ivy

Cites Work

• A decidable and expressive fragment of Many-Sorted first-order linear temporal logic
• Decidable fragments of first-order temporal logics
• Cubicle-\(\mathcal{W}\): parameterized model checking on weak memory
• On finite domains in first-order linear temporal logic
• Parameterized model checking on the TSO weak memory model
• Monodic Fragments of First-Order Temporal Logics: 2000–2001 A.D.
• An improved algorithm for decentralized extrema-finding in circular configurations of processes
• Proving Liveness of Parameterized Programs
• Thread modularity at many levels: a pearl in compositional verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Sound verification procedures for temporal properties of infinite-state systems