Colloquium Computer Science - Dr. Rodrigo Otoni, University of Groningen

Title: Automated Reasoning for Software-Intensive Systems

Abstract:

Software is extensively used in the design and operation of all kinds of modern systems. Due to their ever-growing complexity, software-intensive systems now often rely on automated reasoning to ensure correctness. In this talk, automated reasoning will be presented through the lens of model checking and a number of use cases will be discussed. These will range from the verification of algorithms underpinning our current distributed systems, such as those ensuring consensus in the presence of Byzantine failures, to the synthesis of more energy-efficient arithmetic circuits, which are employed at scale in neural networks. The use of automated reasoning in the novel domains of smart contracts and quantum networks will also be covered, as well as the certification of reasoning results. The talk concludes with an outlook on future research.