Model Checking Data Flows in Concurrent Network Updates

DOI10.1007/978-3-030-31784-3_30zbMath1437.68115arXiv1907.11061OpenAlexW2981785382MaRDI QIDQ3297609

Manuel Gieseking, Jesko Hecking-Harbusch, Bernd Finkbeiner, Ernst-Ruediger Olderog

Publication date: 20 July 2020

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1907.11061

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)

Related Items (3)

From symbolic constraint automata to Promela ⋮ Model Checking Data Flows in Concurrent Network Updates ⋮ Automatic synthesis of transiently correct network updates via Petri games

Uses Software

• LoLA
• LTSmin
• ABC
• Frenetic
• VeriCon
• ITS-Tools
• AIGER
• Anteater
• AdamMC
• zUpdate
• Kuai
• FatTire

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Petri games: synthesis of distributed systems with causal memory
• Branching processes of Petri nets
• Optimal consistent network updates in polynomial time
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Network-wide configuration synthesis
• Synchronization synthesis for network programs
• Unfoldings: A partial-order approach to model checking.
• Decentralizing SDN Policies
• SAT-Based Model Checking without Unrolling
• Model Checking Data Flows in Concurrent Network Updates
• Frenetic

This page was built for publication: Model Checking Data Flows in Concurrent Network Updates