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

Seminários por estudantes do Mestrado em Matemática de CIÊNCIAS.

Iconografia representativa da área da inteligência artificial

09 a 11 de julho: Inteligência Artificial - Implicações e Políticas Globais, em debate no Convento da Arrábida.

Logótipo, data e local do evento

Com o tema “Ciência, Inovação e Sociedade”, o encontro será um palco de promoção e discussão do impacto científico, social, cultural e económico da investigação em Portugal.

Seminário por Diogo Fernandes.

Seminário do Laboratório de Instrumentação e Física Experimental de Partículas, por Beatriz Lopes (CERN).

Horta Solar

E se fosse possível experimentar um curso universitário antes de concorrer ao ensino superior? Agora já é!

Título e local do evento

O evento visa promover o diálogo interdisciplinar sobre estruturas de proteínas, doenças conformacionais e tecnologias baseadas em proteínas.

Logótipo CiE

Uma série interdisciplinar de conferências internacionais organizada pela Associação Computabilidade na Europa (ACiE).

Banner Meredith Ringel Morris HCI for AGI

15 de julho, 14h00: CIÊNCIAS recebe Meredith R. Morris, Diretora de Investigação em Interacção Humano-IA na Google DeepMind e Professora Afiliada na Universidade de Washington, para uma palestra imperdível sobre um dos temas mais debatidos e transformadores da atualidade: o caminho rumo à Inteligência Artificial Geral (AGI).

Título e datas do programa de estágios

Preparados para explorar a investigação de perto?

Á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.

Um workshop com o objetivo de reunir académicos que abordam a história da ecologia - e a evolução da própria disciplina - a partir de uma variedade de perspetivas.

Cardume

Seminário no âmbito do Doutoramento em Ciências do Mar, por Inês Pereira.

Pormenor de mecanismo de relógio

Concerto no âmbito do programa Música na Universidade de Lisboa.

Orquestra

Concerto no âmbito do programa Música na Universidade de Lisboa.

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

Aluna a utilizar um computador portátil

A Escola Doutoral Unite! Widening visa apoiar diretamente estudantes de doutoramento que realizem investigação numa das quatro áreas estratégicas selecionadas pelo projeto - as candidaturas decorrem até 26 de julho.

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.

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.

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.

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.

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.

Páginas