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-XzbMATH Open1242.68284OpenAlexW2056997919MaRDI QIDQ437040FDOQ437040
Authors: Freek Verbeek, Julien Schmaltz 
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
Recommendations
- A formal proof of a necessary and sufficient condition for deadlock-free adaptive networks
- A foundation for designing deadlock-free routing algorithms in wormhole networks
- Deadlock-Free Message Routing in Multiprocessor Interconnection Networks
- Requirements for Deadlock-Free, Adaptive Packet Routing
- The pursuit of deadlock freedom
Graph theory (including graph drawing) in computer science (68R10) Network design and communication in computer systems (68M10)
Cites Work
- Title not available (Why is that?)
- Partial functions in ACL2
- Structured theory development for a mechanized logic
- Title not available (Why is that?)
- Deadlock-Free Message Routing in Multiprocessor Interconnection Networks
- The addition of bounded quantification and partial functions to a computational logic and its theorem prover
- Optimal fully adaptive minimal wormhole routing for meshes
- Formalizing on chip communications in a functional style
- A functional formalization of on chip communications
Cited In (4)
- Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets
- Scaling up livelock verification for network-on-chip routing algorithms
- Verifying deadlock-freedom of communication fabrics
- A formal proof of a necessary and sufficient condition for deadlock-free adaptive networks
Uses Software
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
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q437040)
