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
Campus de CIÊNCIAS

No arranque de mais um ano letivo, CIÊNCIAS dá as boas-vindas aos seus novos docentes e investigadores, numa iniciativa organizada em dois momentos distintos.

Pormenor de lâmpada

Candidaturas a decorrer de 01 a 30 de setembro.

Microplásticos no ocerano

O curso procura dar formação sobre a problemática da contaminação por detritos de plástico dos nossos ecossistemas, bem como alertar para os potenciais efeitos deletérios nos organismos, utilizando uma abordagem de ensino científico, com um discurso adequado a formandos sem formação científica - candidaturas até 03 de agosto.

#eusouciencias e imagens ilustrativas de algumas áreas científicas

Vais iniciar a tua caminhada no ensino superior connosco? Preparámos um programa especialmente concebido para te acolher, com atividades que te vão dar a conhecer o campus e a comunidade de CIÊNCIAS.

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

Um simpósio internacional que reúne investigadores especializados em várias disciplinas (taxonomia, ecologia da vegetação, biogeografia, filogeografia, paleoecologia ou conservação da biodiversidade), focados na flora e vegetação terrestre e marinha da região da Macaronésia (Açores, Madeira, Selvagens, Canárias e Cabo Verde).

Quatro investigadores num laboratório

O curso visa capacitar investigadores, docentes e técnicos para integrar os princípios da economia circular em ambientes laboratoriais académicos - candidaturas até 16 de setembro.

Utilizadora de computador portátil numa sala de aula

Esta oficina de formação, já na sua 3.ª edição, capacitará os professores do ensino secundário das ferramentas necessárias para promover a introdução dos estudantes à programação desde o 10.º ano - candidaturas até 15 de setembro.

Três investigadores num laboratório

O curso visa capacitar profissionais para aplicar os princípios da economia circular em ambientes laboratoriais industriais, promovendo práticas sustentáveis e eficientes - candidaturas até 17 de setembro.

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

O curso visa dotar os formandos 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 - candidaturas até 27 de julho.

Iconografia associada à ULisboa

Celebrando o começo de um novo Ano Académico, a Sessão Solene é um importante marco na vida académica da ULisboa, no qual se reúne toda a sua Comunidade.

Logótipo do evento

Um evento promovido pelo Departamento de Física da Faculdade de Ciências da ULisboa, com um duplo objetivo: valorizar a diversidade e excelência da formação dos doutorados e promover um espaço de diálogo direto entre empresas e estudantes.

Cientista a trabalhar com tubos de ensaio

Os participantes neste curso 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 - candidaturas até 27 de julho.

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) - candidaturas até 31 de agosto.

Saída de campo (Geologia)

O curso, com candidaturas até 20 de julho, convida os professores do Ensino Básico e Secundário a explorar a Geologia a partir das rochas que afloram nas imediações da sua escola.

Mão a segurar em globo de vidro

Este curso de formação acreditado convida educadores e outros interessados a aprofundar a sustentabilidade marinha, explorando ferramentas pedagógicas inovadoras e práticas concretas para inspirar a próxima geração - candidaturas até 28 de setembro.

Astronauta, banhado pela luz solar, no meio de uma floresta

Candidaturas até 30 de julho - um evento único, que reunirá estudantes de mestrado e doutoramento com investigadores e líderes da indústria de toda a Europa para uma experiência inesquecível.

Lupa e caneta sobre página com texto e gráfico

O curso visa dar formação inicial a estudantes de pós-graduação sobre o processo de escrita, submissão e publicação de trabalhos científicos, focando principalmente a publicação de artigos científicos em revistas internacionais com revisão por pares.

Iconografia relacionada com a temática do curso

O curso fornece uma exploração aprofundada de isótopos estáveis como uma ferramenta valiosa em Ecologia, usando assinaturas isotópicas para rastrear processos ecológicos e revelando insights sobre o ciclo de nutrientes e água, interações de espécies e condições ambientais em diversos ecossistemas e comunidades.

Composição de três imagens relativas à área da deteção remota

Este curso visa dar formação na área de Deteção Remota, abrangendo desde a Observação da Terra pelos satélites até à utilização de Drones - candidaturas até 18 de outubro.

O evento pretende reunir investigadores que trabalhem sobre temas ligados à indústria e sobre património técnico e industrial, para uma reflexão prospetiva sobre o património industrial e atuais vias de colaboração no seu estudo, salvaguarda e preservação.

Computador portátil a projetar imagem de sequência biológica

O curso visa a aquisição de conhecimentos sobre as ferramentas bioinformáticas disponíveis para efetuar análises de sequências de DNA e proteínas, bem como a autonomia e espírito crítico na utilização dessas ferramentas. Procura igualmente desenvolver competências na utilização de software de bioinformática disponível gratuitamente na Internet e na interpretação do significado biológico dos resultados.

Bola de cristal colocada no solo

O curso tem como objetivo apresentar aos participantes um estado da arte atualizado sobre a diversidade da biota do solo e os papéis funcionais desempenhados pelos organismos do solo nos principais processos ecológicos.

Imagem exemplificativa da área da deteção remota

Este curso avançado tem como objetivo fornecer acesso e ferramentas para a aquisição e processamento de dados de deteção remota para diferentes aplicações, usando imagens multiespectrais de satélite, drone, terrestres e LiDAR, com foco na caracterização da vegetação e da paisagem, bem como das suas mudanças ao longo do tempo.

A conferência visa reunir os principais especialistas no domínio da Imagiologia Médica por Micro-ondas (MMWI) e incluirá palestras, apresentações e pósteres de resumos revistos por pares e artigos de conferências, bem como workshops em áreas satélite de investigação com interesse para a investigação em MMWI.