Mooly Sagiv is a professor in the School of Computer Sciences at Tel-Aviv University and a CEO and co-founder of Certora. He is a leading researcher in the area of large scale (inter-procedural) program analysis, and one of the key contributors to shape analysis. His fields of interests include programming languages, compilers, abstract interpretation, profiling, pointer analysis, shape analysis, inter-procedural dataflow analysis, program slicing, and language-based programming environments. Prof. Sagiv is a recipient of a 2013 senior ERC research grant for Verifying and Synthesizing Software Composition. He also served as Member of the Advisory Board of Panaya Inc. and received best-paper awards at PLDI'11 and PLDI'12 for his work on composing concurrent data structures and a ACM SIGSOFT Retrospective Impact Award (2011) for program slicing. He is a recipient of Friedrich Wilhelm Bessel Research Award (2002), He is an ACM fellow and a recipient of Microsoft Research Outstanding Collaborator Award 2016.

AG 1, AG 2, AG 3, INET, AG 4, AG 5, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Saarbrücken

Financial applications such as Landing and Payment protocols, and their realization in decentralized financial (DeFi) applications in Blockchains, comprise a unique domain where bugs in the code may be exploited by anyone to steal assets. This situation provides unique opportunities for formal verification to enable “move fast and break nothing”. Formal verification can be used to detect errors early in the development process and guarantee correctness when a new version of the code is deployed.

I will describe an attempt to automatically verify DeFis and identify potential bugs. The approach is based on breaking the verification of DeFis into decidable verification tasks. Each of these tasks is solved via a decision procedure which automatically generates a formal proof or a test input showing a violation of the specification. In order to overcome undecidability, high level properties are expressed as ghost states and static analysis used to infer how low level programs update ghost states.

--

Please contact MPI-SWS Office Team for Zoom link information

Danielle Dalton

+49 681 9303 9106

--email hidden