Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks

DOI10.1007/s10817-010-9206-xzbMath1242.68284OpenAlexW2056997919MaRDI QIDQ437040

Julien Schmaltz, Freek Verbeek

Publication date: 17 July 2012

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-010-9206-x

zbMATH Keywords

deadlock-free routingACL2interactive theorem proving

Mathematics Subject Classification ID

Network design and communication in computer systems (68M10) Graph theory (including graph drawing) in computer science (68R10)

Related Items (2)

Scaling up livelock verification for network-on-chip routing algorithms ⋮ Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets

Uses Software

• ACL2
• NQTHM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A functional formalization of on chip communications
• The addition of bounded quantification and partial functions to a computational logic and its theorem prover
• Partial functions in ACL2
• Structured theory development for a mechanized logic
• Optimal fully adaptive minimal wormhole routing for meshes
• Deadlock-Free Message Routing in Multiprocessor Interconnection Networks

This page was built for publication: Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks