Login

David Pereira (Publications)

David Pereira (Publications)

David Pereira (Publications)

PhD MAPi, Portugal
Research Centre Board of Directors Member
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.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Journal Papers
Deciding Kleene Algebra Terms Equivalence in Coq CISTER-TR-141205 
David Pereira, Nelma Moreira, Simão Patrício Melo de SousaJournal of Logical and Algebraic Methods in Programming (JLAMP), Elsevier. May 2015, Volume 84, Issue 3, pp 377-401.
Logic-based schedulability analysis for compositional hard real-time embedded systems CISTER-TR-150411 
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa PintoSIGBED Review (SIGBED Rev.), ACM. Feb 2015, Volume 12, Issue 1, pp 56-64.
Conference or Workshop Papers/Talks
Abstract Timers and their Implementation onto the ARM Cor tex-M family of MCUs CISTER-TR-151202 
Per Lindgren, Emil Fresk, Marcus Lindner, Andreas Lindner, David Pereira, Luis Miguel PinhoEmbedded Operating System Workshop (EWiLi 2015). 8, Oct, 2015. Amsterdam, Netherlands.
Monitoring for a decidable fragment of MTLD CISTER-TR-151009 
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa PintoThe 15th International Conference on Runtime Verification (RV'15). 22 to 25, Sep, 2015. Vienna, Austria.
A Real-Time Semantics for the IEC 61499 standard CISTER-TR-150903 
Per Lindgren, Marcus Lindner, Andreas Lindner, Valeriy Vyatkin, David Pereira, Luis Miguel Pinho20th IEEE International Conference on Emerging Technologies & Factory Automation (ETFA 2015). 8 to 11, Sep, 2015. Luxembourg, Luxembourg.
Run-time Monitoring Architecture for Real-Time Systems CISTER-TR-151207 
Geoffrey Nelissen, David Pereira, Luis Miguel PinhoINForum - Simpósio de Informática (INFORUM 2015). 7 to 8, Sep, 2015. Portugal.
A Formal Perspective on IEC 61499 Execution Control Chart Semantics CISTER-TR-150802 
Per Lindgren, Marcus Lindner, David Pereira, Luis Miguel PinhoIEEE International Symposium on Parallel and Distributed Processing with Applications (ISPA 2015). 20 to 22, Aug, 2015. Helsinki, Finland.
Response Time for IEC 61499 over Ethernet CISTER-TR-150721 
Per Lindgren, Johan Eriksson, Marcus Lindner, Andreas Lindner, David Pereira, Luis Miguel PinhoIEEE International Conference on Industrial Informatics (INDIN 2015). 22 to 24, Jul, 2015. Cambridge, United Kingdom.
Well formed Control-flow for Critical Sections in RTFM-core CISTER-TR-150511 
Per Lindgren, Marcus Lindner, Andreas Lindner, David Pereira, Luis Miguel PinhoIEEE International Conference on Industrial Informatics (INDIN 2015). 22 to 24, Jul, 2015. Cambridge, United Kingdom.
A Novel Run-Time Monitoring Architecture for Safe and Efficient Inline Monitoring CISTER-TR-150308 
Geoffrey Nelissen, David Pereira, Luis Miguel Pinho20th International Conference on Reliable Software Technologies - Ada-Europe 2015 (Ada-Europe 2015). 22 to 26, Jun, 2015. Madrid, Spain.
Toward a Run-Time Verification Framework for Real-Time Safety-Critical Systems CISTER-TR-151011 
Geoffrey Nelissen, David Pereira, Luis Miguel PinhoSEMINAR “ACtion Temps Réel : Infrastructures et Services Systèmes“. 10, Apr, 2015. Brussels, Belgium.
Conference or Workshop Posters/Demos
A Novel Runtime Monitoring Architecture CISTER-TR-150310 
Geoffrey Nelissen, David Pereira, Luis Miguel PinhoPoster presented in 28th GI/ITG International Conference on Architecture of Computing Systems (ARCS 2015). 25 to 28, Mar, 2015, Poster Session. Porto, Portugal.
Formal Contracts for Runtime Verification Support in the Ada Programming Language CISTER-TR-150412 
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa PintoPoster presented in The 28th GI/ITG International Conference on Architecture of Computing Systems (ARCS 2015). 24 to 26, Mar, 2015. Porto, Portugal.