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
Logótipo do Verão na ULisboa, sobre um fundo azul

Candidaturas a partir de 07 de abril!

Representação de programação R

This course aims at providing students with statistical knowledge and tools to manipulate, analyse and visualise biological data with R. Introduction to modeling, simulations and Bayesian statistics.

Título/data do evento e vários objetos museológicos

This course aims to provide an updated vision of the potential of museum collections for biodiversity research. More specifically, aims to present case studies on the value of museums and the use of collections and specimens in the 21st century, using new technologies and analytical methods.

Computability in Europe (CiE) is an interdisciplinary series of international conferences organised by the Association Computability in Europe (ACiE).

Título e datas do programa de estágios

Ready to explore research up close? Our 2025 Internship Program is now accepting applications!

Águas subterrâneas

Curso acreditado para efeitos de progressão na carreira dos professores na dimensão cientifico-pedagógica dos grupos 420 e 520, com candidaturas até 02 de junho.

A 10.ª edição do Ser Cientista realiza-se entre 21 e 25 de julho - vem investigar connosco!

Logótipo do evento, sobre fotografia dos Açores

An international symposium that convenes researchers specializing in various disciplines focused on the terrestrial and marine flora and vegetation of the Macaronesian region (Azores, Madeira, Selvagens, Canary Islands, and Cabo Verde).

Composição de imagens relativas à área das ciências forenses

O curso visa dotar os formandos, com formação universitária nas mais diversas áreas do saber, com os conhecimento necessários à integração de equipas profissionais multidisciplinares nas áreas Médico-Legais e Forenses, em Laboratórios ou Serviços Médico-Legais e Forenses.

Cientista a trabalhar com tubos de ensaio

Este curso forma profissionais para atividade na área das Análises Clínicas ou Patologia Clínica. Irão adquirir os conhecimentos essenciais à integração de equipas profissionais multidisciplinares na área das Análises Clínicas/Patologia Clínica, em laboratórios privados, públicos, hospitalares ou do Estado.

Gotas de água

O curso visa capacitar os formandos para a aplicação dos índices de qualidade ecológica utilizados na avaliação da qualidade ambiental em sistemas de transição, no âmbito da Diretiva Quadro da Água (DQA).

The conference aims to bring together key experts in the Medical Microwave Imaging (MMWI) field and will include invited talks, presentations and posters of peer-reviewed abstracts and conference papers, and workshops in satellite areas of research that are of interest to MMWI research.

Páginas