RSS Meetup

A Decade Verifying LLVM, or How to Retrofit Soundness in Industrial Software

Sala 6.2.38, Ciências ULisboa

Por Nuno Lopes (IST, ULisboa).

LLVM is one of the most widely used compilers in the world. Its users include Apple, Google, Meta, Microsoft, PlayStation, Qualcomm, and many others.

We started verifying LLVM a decade ago. In the process, we found bugs everywhere: in LLVM, in SMT solvers, in the documentation, and in our own tools. We also found shortcomings in the compiler’s theoretical models, namely of undefined behavior, memory, and concurrency. For example, we showed that it was impossible to run certain classic textbook optimizations together in LLVM. This led us to make fundamental architectural changes in LLVM itself.

Moreover, LLVM keeps changing every day. We caught many regressions along the way.

In this talk, we will cover our attempts to verify LLVM. The tools we built, the bugs we caught, the bugs we missed, the good and the bad surprises, and our contributions to theoretical models of compilers. We will also discuss why and how our automatic formal verification tools are used by compiler engineers on a daily basis.

Bio: Nuno P. Lopes is an associate professor at IST (U Lisbon). Previously, and has previously worked at Apple (US), Microsoft Research (UK and US), and Max Planck Institute (Germany). He is the inventor of 5 US and EU patents and has received 3 best paper awards from leading conferences, the HVC research impact award, and the HiPEAC tech transfer award.

Nuno has been an active open-source software contributor since 2003. His automatic compiler verification tool, Alive2, is used regularly by compiler developers around the world and has been officially adopted by the LLVM compiler.

14h00
LASIGE Computer Science and Engineering Research Centre

Earth Systems Seminar, por David Barriopedro Cepero (Instituto de Geociencias - IGEO, CSIC-UCM).

Uma atividade coordenada por Vítor Lapa Fernandes (aluno de CIÊNCIAS), promotor do projeto vencedor do concurso de bolsas para jovens artistas, ativistas e criadores desenvolvido pelo Festival Política e pelo Instituto Português do Desporto e Juventude.

Projeto de Tese (Doutoramento em Biodiversidade, Genética e Evolução), por Fátima Inácio.

Seminário de Lógica Matemática, por Charles Morgan (UFBA).

Banner do Dia de Ciências 2025

A 29 de abril assinalamos o 114.º aniversário de CIÊNCIAS.

Junte-se a nós no Grande Auditório de CIÊNCIAS para uma tarde de celebração que reúne toda a comunidade da Faculdade.

Seminário do Centro de Física Teórica e Computacional, por Pablo Sartori (Instituto Gulbenkian de Ciência, Oeiras, Portugal).

Pormenor de pintura representativa da cidade de Aden

O curso, com Jorge Flores (CIUHCT), oferece uma visão da história da Ásia a partir de cidades portuárias cruciais nas relações com o Ocidente.

O Tec Labs lançou a marca MindTec com o objetivo de promover um processo participativo de rebranding interno, assente na escuta ativa da sua comunidade. Esta sessão marca o arranque oficial do projeto e será um momento-chave para apresentar os seus objetivos, envolver a comunidade e começar a recolher perceções, expectativas e desafios relacionados com a comunicação no ecossistema.

Fotografia de fábrica a emitir poluição para a atmosfera

The course aims at enabling the participants to use different methods to measure the impacts of pollutants on ecosystems.

Logótipo C-Academy

O curso oferece uma base sólida sobre os fundamentos e práticas essenciais para proteger sistemas e dados num mundo cada vez mais digital - candidaturas até 13 de abril.

Curso destinado a todos que necessitem de realizar análise de dados com recurso ao R.

Banner Dia Aberto de CIÊNCIAS 2025.

Bem-vindos a Ciências ULisboa!

Um concurso de programação dirigido aos alunos do ensino secundário (11.º e 12.º anos), que visa promover a prática e o gosto pela programação.

Fotografia de Chapim-azul

The goal of this course is to provide the participants with the most recent and practical knowledge on the use of Functional Diversity.

O encontro tem como objetivo divulgar e promover os resultados da investigação produzidos nos dois pólos do Centro de Química Estrutural (CIÊNCIAS e IST), estimulando a criatividade, o trabalho interdisciplinar e o espírito científico.

Mão a segurar em globo de vidro

Curso acreditado pelo CCPFC para efeitos de progressão na carreira dos professores na dimensão cientifico-pedagógica dos grupos 230, 420, 510, 520 e 560, com candidaturas até 30 de abril.

Título/data/local do evento, logótipos das entidades organizadoras e fotografia de peixe

The event aims to facilitate the exchange of information and knowledge among professionals to advance the understanding, collaboration and capabilities of aquaculture to respond to the impact of climate change in a rapidly changing global environment.

Uma oportunidade única para interagir com a comunidade global de computação científica, com inscrições (preço reduzido) até 02 de maio.

Logótipo Moodle

Ação de formação para docentes e investigadores de CIÊNCIAS.

Título/data/local do evento e iconografia representativa de energias renováveis

Inscrições até 16 de maio! Junta-te a esta revolução energética e faz a diferença!

Químico a escrever fórmulas num quadro

Curso acreditado para efeitos de progressão na carreira dos professores do Ensino Básico e Secundário do Grupo 510 (CCPFC/ACC-118288/22), com candidaturas até 18 de maio.

Curso destinado a estudantes de Mestrado e de Doutoramento, bem como a profissionais que desenvolvam investigação científica na área da saúde.

Título/data/local do evento e fotografia do mar

Quais são os conceitos-chave para enfrentar os atuais desafios marinhos e costeiros? 

Representação de programação R

This course aims at providing students with basic knowledge of R programming, allowing them to manipulate and visualize data with R.

Título da conferência, sobre um quadro de ardósia

The conference focuses on "Algebra and its role in Computer Science", with special emphasis on the areas of study related to the work of M. V. Volkov, such as semigroups and automata.

Páginas