No próximo dia 2 de maio, pelas 13h30 na sala FC6 140 do DCC FCUP, David Pereira irá dar uma palestra intitulada "Correct-by-construction (in-)Equivalence of Regular Expressions through the Coq proof-assistant".
A palestra é organizada pelo LIACC e pelo DCC-FCUP.
Short Bio:
David completed his PhD in Computer Science in 2013 in the field of Formal Verification of Software under the scope of the MAP-i Doctoral Program in Computer Science. Since 2013, David is PhD researcher in CISTER-ISEP, and develops his activities in the area of Formal Logics and Domain Specific Languages for supporting Runtime Verification for Cyber Physical Systems (CPS). David participated in several key EU, industry-driven projects, and has beeen involved in the creation of the Vortex CoLab since 2018, supporting the embedded systems & formal verification R&D lines of the lab.
Title
"Correct-by-construction (in-)Equivalence of Regular Expressions through the Coq proof-assistant"
Abstract
In this talk, we will revisit a Coq development that led to the implementation of a correct-by-construction procedure to decide the (in-)equivalence of regular expressions using the concept of partial derivatives. The focus will be on the main technical challenges that the authors faced during development, notably those posed by the Coq proof system, and present the solutions that were devised and that resulted in an efficient procedure which can be extracted and integrated into larger software developments.