Algorithmic Analysis of Lossy Channel Machines Using Small Models

• Main Author: Sharyari, Ali Jonathan
• Format: Others
• Language: English
• Published: Uppsala universitet, Institutionen för informationsteknologi 2016
• Online Access: http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-301502

Verification of infinite-state systems is in general an undecidable problem, but nevertheless, solid correctness results are important in many real-life applications. It is commonly the case that such algorithms rely on unbounded buffers for their operation, communication protocols being a typical example. Building upon abstract interpretation techniques, this project presents a verification algorithm capable of verifying the correctness of algorithms relying on unbounded lossy buffers. We have implemented our approach and used it to verify a number of well-known communication protocols. The experimental results are mixed, but in most cases comparable to that of other existing tools, justifying further research on the topic.