Algorithmic Analysis of Lossy Channel Machines Using Small Models
Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
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.
Place, publisher, year, edition, pages
2016. , 44 p.
UPTEC IT, ISSN 1401-5749 ; 16006
Engineering and Technology
IdentifiersURN: urn:nbn:se:uu:diva-301502OAI: oai:DiVA.org:uu-301502DiVA: diva2:954769
Master of Science Programme in Information Technology Engineering
Atig, Mohamed FaouziNordén, Lars-Åke