Formal framework for automated analysis and verification of distributed reactive applications

As applications become more and more complex, concurrency and communication play increasingly important roles in the design process. In particular, highly distributed applications demand truly scalable communication architectures. There is a real need for reliability and constructivity in the design of such systems. The use of a bottom-up strategy, supported by abstraction and proofs, allows scalable modeling and verification of behavioral properties, and facilitates the derivation of robust systems. The purpose of our research is to produce scalable solutions facilitating the systematic design of complex, reactive, and distributed systems that are guaranteed correct by construction.