Campus Event Calendar: Alexander J. Summers (04/27/2023 in E1 5/002)

Campus Event Calendar

Campus Event Calendar:
- All Upcoming:
  - only for D1
  - only for D2
  - only for INET
  - only for D4
  - only for D5
  - only for D6
  - only for RG1
  - Mailing Lists
  - by Speaker
  - by Type
  - by Category
  - by Title
  - Calendar
  - RSS Feed
- History of Events:

Event Entry

What and Who

2vyper: Contracts for Smart Contracts

Alexander J. Summers

University of British Columbia

SWS Colloquium

Alex Summers is an Associate Professor of Computer Science at the University of British Columbia (UBC). Prior to moving to UBC in early 2020 he worked at ETH Zurich as a senior researcher in the Chair of Programming Methodology group run by Peter Müller. Alex works the general area of program correctness, including developing new specification and verification logics and type systems, and developing automated tools for constructing proofs about heap-based and concurrent programs, usually building on SMT solvers. He co-ordinated the Viper project for several years, and started the Prusti project providing user-facing verification for Rust. Alex is broadly interested in software verification for a wide variety of concurrent and imperative programming paradigms, and was awarded the 2015 Dahl-Nygaard Junior Prize for his work in these areas.

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

AG Audience

English

Note: We use this to send email in the morning.

Date, Time and Location

Thursday, 27 April 2023

16:00

60 Minutes

E1 5

002

Saarbrücken

Abstract

Smart contract languages are increasingly popular and numerous, and their programming models and challenges are somewhat unusual. The ubiquitous presence of untrusted external code in such a system makes classical contracts unsuitable for safety verification, while the intentional presence of (potentially-mutating) callbacks via unknown code makes standard static analysis techniques imprecise in general. On the other hand, smart contract languages such as Vyper (for Ethereum) tightly encapsulate direct access to the program's state. In this talk I'll present a methodology for expressing contracts for this language, in a way that supports sound verification of safety properties, with deductive verification tooling (converting Vyper to Viper) to automate the corresponding proofs.

Based on joint work with Christian Bräm, Marco Eilers, Peter Müller and Robin Sierra; see also the accompanying paper at OOPSLA 2021.

---

Please contact Office for Zoom link information.

Contact

Annika Meiser

+49 681 9303 9105

--email hidden

Video Broadcast

Video Broadcast:

Yes

To Location:

Kaiserslautern

To Building:

G26

To Room:

111

Cisco Meeting ID:

System used:

Meeting URL:

Meeting ID:

Passcode:

Code Visible for:

public

Annika Meiser, 04/26/2023 11:43
Annika Meiser, 04/25/2023 14:15 -- Created document.

Imprint / Impressum | Data Protection / Datenschutzhinweis