Login

David Pereira (Publications)

David Pereira (Publications)

David Pereira (Publications)

PhD MAPi, Portugal
Research Associate

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.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Journal Papers
Runtime verification of autopilot systems using a fragment of MTL-∫ CISTER-TR-170802 
André Pedro, Jorge Sousa Pinto, David Pereira, Luis Miguel PinhoInternational Journal on Software Tools for Technology Transfer (STTT), Springer Berlin Heidelberg. 21, Aug, 2017, pp 1-17.
End-to-End Response Time of 61499 Distributed Applications over Switched Ethernet CISTER-TR-170502 
Per Lindgren, Johan Eriksson, Marcus Lindner, Andreas Lindner, David Pereira, Luis Miguel PinhoIEEE Transactions on Industrial Informatics (TII), IEEE. Feb 2017, Volume 13, Issue 1, pp 287-297.
Conference or Workshop Papers
Formal Verification of AADL Models Using UPPAAL CISTER-TR-171101 
Fernando Gonçalves, David Pereira, Eduardo Tovar, Leandro BeckerVII Brazilian Symposium on Computing Systems Engineering (SBESC 2017). 7 to 10, Nov, 2017, Session 10: Development and Tools - B, pp 117-124. Curitiba, Brasil.