Computer Science Seminar - Dr. Rodrigo Benedito Otoni, Universit of Svizzera

Titel: Automated Verification of Distributed Software Systems

Abstract:

Modern distributed software systems have a level of complexity that makes manual development and maintenance quite intricate and error-prone. To address this issue, automated verification techniques can be employed to identify vulnerabilities and, if none are present, ensure their absence. In this talk, two symbolic model checking approaches based on first-order logic reasoning will be presented, which support the verification of distributed algorithms specifications and smart contracts implementations. The first approach targets the TLA+ language and exploits satisfiability modulo theories (SMT) solving to enable the efficient verification of complex algorithms such as those ensuring consensus in the presence of Byzantine failures. The second approach targets the Solidity language and exploits constrained Horn clauses (CHC) solving to enable the precise verification of real-world contracts deployed in the Ethereum blockchain. The talk concludes with an outlook on synergistic automated reasoning research tracks.