Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems

DOI10.1007/s10472-016-9531-9zbMath1419.68064MaRDI QIDQ2408742

César Sánchez, Alejandro D. Sánchez

Publication date: 13 October 2017

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-016-9531-9

zbMATH Keywords

formal verification; formal methods; temporal logic; verification conditions; liveness properties; parametrized systems; deductive method; concurrent data types

Mathematics Subject Classification ID

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

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Uses Software

• AProVE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Parametrized invariance for infinite state processes
• Alternating finite automata on \(\omega\)-words
• Reasoning about networks with many identical finite state processes
• Proving properties of a ring of finite-state machines
• A logic of reachable patterns in linked data-structures
• Verification of parameterized concurrent programs by modular reasoning about data and control
• Generalized temporal verification diagrams
• A Logic-Based Framework for Reasoning about Composite Data Structures
• Proving that programs eventually do something good
• Back to the future
• Proving Termination of Programs Automatically with AProVE
• Formal Verification of Skiplists with Arbitrary Many Levels
• Thread Quantification for Concurrent Shape Analysis
• Temporal Verification of Reactive Systems: Response
• Combining Theories with Shared Set Operations
• Formal verification of parallel programs
• A new solution of Dijkstra's concurrent programming problem
• Proving that non-blocking algorithms don't block
• CONCUR 2004 - Concurrency Theory
• CONCUR 2004 - Concurrency Theory
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Oracle Semantics for Concurrent Separation Logic
• Verification, Model Checking, and Abstract Interpretation
• Foundations of Software Science and Computation Structures
• A general framework for automatic termination analysis od logic programs