MSE Research Fellow, Saloni Sinha, Co-Authors Paper Accepted to ABZ 2024

Saloni Sinha (MSE ’23) and Dr. Eunsuk Kang’s paper, “Formal Modeling and Analysis of Apache Kafka in Alloy 6”, has been accepted to ABZ 2024 – the International Conference on Rigorous State Based Methods. Just last year, Saloni was awarded the 2023 James E. Tomayko Graduate Scholarship in Software Engineering for her performance in the MSE curriculum and she is currently working as an MSE Research Fellow under the supervision of Dr. Kang.

Saloni discovered her interest in formal methods during her coursework in the MSE Professional program, specifically the courses Formal Methods and Advanced Formal Methods, stating that she otherwise would not have come across this area of research. She emphasizes the need for formal modeling techniques to confidently reason about distributed systems which often have complex architectures and involve interaction among multiple concurrent components. She hopes to design distributed systems as an industry professional in the future, using the expertise in formal methods she has acquired during her research.

Sinha and Kang’s paper demonstrates application of formal analysis techniques to a distributed event streaming platform – Kafka – widely used in the industry. The results provide insights into how Kafka achieves a set of desirable properties, and the circumstances under which these properties may not hold. The Alloy model built for this analysis is one of the largest to have been developed so far which goes on to demonstrate Alloy’s capability to model a complex real-world distributed system. Interestingly, Saloni proposed and initiated this work as part of the independent project component of the course Advanced Formal Methods which later evolved into a research project.

Saloni is currently working on optimizing instance generation in Alloy, and applying formal methods to distributed consensus protocols.