Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems

DOI10.1007/s10472-016-9531-9zbMath1419.68064OpenAlexW2554441166MaRDI 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 verificationformal methodstemporal logicverification conditionsliveness propertiesparametrized systemsdeductive methodconcurrent data types

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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

This page was built for publication: Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems