Talks@DI/LASIGE

Bridging the design and implementation of distributed systems with program analysis

Sala 6.3.38, FCUL, Lisboa

Por Ivan Beschastnikh (University of British Columbia).

Abstract: Much of today's software runs in a distributed context: mobile apps communicate with the cloud, web apps interface with complex distributed backends, and cloud-based systems use geo-distribution and replication for performance, scalability, and fault tolerance. However, distributed systems that power most of today's infrastructure pose unique challenges for software developers. For example, reasoning about concurrent activities of system nodes and even understanding the system’s communication topology can be difficult.

In this talk I will overview three program analysis techniques developed in my group that address these challenges. First, I will present Dinv, a dynamic analysis technique for inferring likely distributed state properties of distributed systems. By relating state across nodes in the system Dinv infers properties that help reason about system correctness. Second, I will review Dara, a model checker for distributed systems that introduces new techniques to cope with state explosion by combining traditional abstract model checking with dynamic model inference techniques. Finally, I will discuss PGo, a compiler that compiles formal specifications written in PlusCal/TLA+ into runnable distributed system implementations in the Go language. All three projects employ program analysis in the context of distributed systems and aim to bridge the gap between the design and implementations of such systems.

Short Bio: Ivan Beschastnikh is an Assistant Professor in the Department of Computer Science at the University of British Columbia. He finished his PhD at the University of Washington in 2013 and received his formative training at the University of Chicago. He has broad research interests that touch on systems and software engineering. His recent projects span distributed systems, program analysis, networks, and security.

Visit his homepage to learn more: http://www.cs.ubc.ca/~bestchai/

14h00
Departamento de Informática / LaSIGE - Laboratório de Sistemas Informáticos de Grande Escala
Jovem investigadora a utilizar um laptop na esplanada de um café

Concurso aberto até 31 de dezembro de 2023.

Título "Gostarias de realizar uma mobilidade Erasmus+" e iconografia representativa de candidaturas e sessões de esclarecimento, sobre um fundo verde

Candidaturas até 31 de dezembro de 2023.

Logótipo da Rede Alumni, slogan "Celebrate your connection", título da call e fotografia de túnel luminoso (em tons de azul)

Call para mentores e mentorandos a decorrer até 02 de janeiro.

Título/data/local do evento e fotografias das oradoras

Formação de Comunicação em Ciência(s), por Marta Daniela Santos (Direção de Comunicação e Imagem) e Rita Tomé (Tec Labs).

Logótipo do curso

Curso técnico-científico, com inscrições até 31 de dezembro.

Logótipo do evento (morcego e flor) e das entidades organizadoras, sobre fotografia de mosaicos representando uma paisagem tropical

The conference promises to be a gathering of researchers and enthusiasts from around the world. It will be an excellent opportunity to learn, exchange experiences and ideas, establish partnerships, and contribute to the advancement of tropical ecological science.

Páginas