Seminars details

  • The Quest for Bullet-proof Software Systems.
  • From social networking to space exploration, software is the mainstay that keeps our world operating. But how do we know that we can trust software? One answer is software reliability testing. Such tests, however, only cover a subset of the possible executions that the software will run in practice. The best solution involves including robust mathematical guarantees in the software development process. ‘Formal methods’ is a field within computer science that advocates this approach, employing rigorous mathematical reasoning and modelling techniques to describe and certify parts of computer infrastructures. In this talk, I will present my research activity in formal methods, with a particular focus on the activity of deductive software verification. In particular, I will detail my contributions towards pushing the boundaries on machine verification of realistic software systems. Finally, I will go though the main challenges I believe are likely to keep software verification community busy in the coming years. BIO: Since June 2022, Mário Pereira is Assistant Professor at NOVA School of Science and Technology, as well as an integrated member of NOVA LINCS. Prior, he held a Marie Skłodowska-Curie individual fellowship (March 2020 - May 2022), where he was the main architect and lead developer of Cameleer, a framework for the deductive verification of OCaml-written code. Pereira completed his PhD in 2018, under the supervision of Jean-Christophe Filliâtre at Université Paris-Saclay. He is an expert in deductive software verification and functional programming. He actively collaborates with worldwide-acknowledged lead researchers in the fields of functional programming and software verification, namely in the development of the GOSPEL specification language and the Why3 verification framework.
  • 13/07/2022 14:00
  • Software Systems
  • Since June 2022, Mário Pereira is Assistant Professor at NOVA School of Science and Technology, as well as an integrated member of NOVA LINCS. Prior, he held a Marie Skłodowska-Curie individual fellowship (March 2020 - May 2022), where he was the main architect and lead developer of Cameleer, a framework for the deductive verification of OCaml-written code. Pereira completed his PhD in 2018, under the supervision of Jean-Christophe Filliâtre at Université Paris-Saclay. He is an expert in deductive software verification and functional programming. He actively collaborates with worldwide-acknowledged lead researchers in the fields of functional programming and software verification, namely in the development of the GOSPEL specification language and the Why3 verification framework.
  • https://videoconf-colibri.zoom.us/j/92950889155?pwd=YXN6MFNwaDVxbGh4RHQ5d3N0VWhLUT09
  • Mário Pereira