Login

David Pereira (Publications)

David Pereira (Publications)

David Pereira (Publications)

PhD MAPi, Portugal
Lecturer, Integrated PhD Researcher

David Pereira was born in Porto, Portugal, in 1980. In 2003 he received his degree in Computer Science at University of Porto. In 2007 he finished his Master's degree in Computer Science also in University of Porto, in the areas of formal logics for specifying and reasoning about intelligent agents. He has a PhD in Computer Science, in the MAP-i PhD program, organized by the Universities of Minho, of Porto and of Aveiro. His research is focused in the mechanization of Kleene algebra and Kleene algebra with tests in the Coq theorem prover (see http://coq.inria.fr/). He also mechanized a deductive proof system for dealing with the partial correctness of parallel programs, under the spirit of Rely/Guarantee thinking. The aim is to apply such mechanizations to conduct partial verification of correctness of both sequential and parallel imperative programs.

Besides being a happy Coq user and adept of formal program verification, David is keen to apply is formal methods background into the realm of programming languages for real-time programs, namely the well-know and powerful ADA.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Conference or Workshop Papers/Talks
Real-time MTL with durations as SMT with applications to schedulability analysis CISTER-TR-200703 
André Pedro, Martin Leucker, David Pereira, Jorge Sousa Pinto14th International Symposium on Theoretical Aspects of Software Engineering (TASE 2020). 11 to 13, Dec, 2020. Hangzhou, China.
Work-In-Progress: a DSL for the safe deployment of Runtime Monitors in Cyber-Physical Systems CISTER-TR-201002 
Giann Nandi, David Pereira, José Proença, Eduardo Tovar
ABSTRACTPDFPDF Additional Files: PDFPoster
Work in Progress Session, 41st IEEE Real-Time Systems Symposium (RTSS 2020). 1 to 4, Dec, 2020, pp 395-398. Online.