image placeholder

A paper co-authored by Professor Tevfik Bultan titled Automatic Verification of Interactions in Asynchronous Systems with Unbounded Buffers received the ACM SIGSOFT Distinguished Paper Award at the 29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014). ACM Special Interest Group on Software Engineering (SIGSOFT) is the premier professional organization in the software engineering area, and ASE is one of the major research conferences sponsored by ACM SIGSOFT. This year ASE received 323 paper submissions and the acceptance rate for technical research papers was 20%. The paper co-authored by Professor Bultan was one of the papers chosen by the ASE Program Committee to receive the ACM SIGSOFT Distinguished Paper Award.

The paper was the result of an ongoing collaboration between Professor Bultan and Professor Samik Basu from the Iowa State University that started during Professor Basu's sabbatical visit to UCSB in 2010. Their work focuses on analyzing distributed computer systems that communicate with asynchronous messages. This is the main communication mechanism in modern computing systems, so the research results in this area are applicable to many domains including communication protocol design, distributed system design, distributed programming and web services. A well known negative result in this area from 1980s proves that verification of systems that communicate with asynchronous messages cannot be automated. Intuitively, this is due to the fact that it is not possible to keep track of all messages that are in transit when analyzing such systems, since the number of messages in transit is not bounded.

The paper co-authored by Professors Bultan and Basu defines a class of systems whose communication behavior does not change when the number of messages in transit is bounded. Which means that, systems in this class can be automatically verified. Moreover, the paper demonstrates that it is possible to automatically check if a given system is in this class. Experiments reported in the paper indicate that a significant portion of existing communication protocols fall into this class, so the results are potentially applicable to a large number of distributed systems.