Login

David Pereira (Publications)

David Pereira (Publications)

David Pereira (Publications)

PhD MAPi, Portugal
Research Centre BoD 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.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Thesis
Towards Certified Program Logics for the Verification of Imperative Programs CISTER-TR-130408 
David PereiraPhD Thesis. 2013. Porto, Portugal.
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. Aug 2018, Volume 20, Issue 4, pp 379-395.
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.
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
Towards improved Validation of Autonomous Systems for Smart Farming CISTER-TR-180302 
Martijn Rooker, Pablo Horstrand, Aythami Salvador Rodriguez, Sebastian Lopez, Roberto Sarmiento, Jose Lopez, Ray Alejandro Lattarulo, Joshue Manuel Perez Rastelli, Zora Slavik, David Pereira, Markku Pusenius, Tapio LeppälampiSmart Farming Workshop (Smart Farming 2018). 10, Apr, 2018, Workshop. Porto, Portugal.SmartFarming Workshop was held as part of the CPS Week 2018, Porto - Portugal, April 10th - 13th, 2018.
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.
SMT-based Schedulability Analysis using RMTL-∫ CISTER-TR-161101 
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa PintoIEEE Real-Time Systems Symposium (RTSS 2016). 29, Nov to 2, Dec, 2016, CRTS. Porto, Portugal.
REVERT: Runtime Verification for Real-Time Systems CISTER-TR-161006 
Sangeeth Kochanthara, Geoffrey Nelissen, David Pereira, Rahul Purandare
ABSTRACTPDFPDF Additional Files: PDFPoster Abstract, PDFPoster
Work in Progress Session, IEEE Real-Time Systems Symposium (RTSS 2016). 29, Nov to 2, Dec, 2016. Porto, Portugal.
REVERT: A Monitor Generation Tool for Real-Time Systems CISTER-TR-161007 
Sangeeth Kochanthara, Geoffrey Nelissen, David Pereira, Rahul Purandare
ABSTRACTPDFPDF Additional Files: PDFPoster
IEEE Real-Time Systems Symposium (RTSS 2016). 29, Nov to 2, Dec, 2016, RTSS@Work. Porto, Portugal.
Towards Certified Compilation of RTFM-core Applications CISTER-TR-161105 
Per Lindgren, Marcus Lindner, David Pereira, Luis Miguel Pinho21st International Conference on Emerging Technologies and Factory Automation (ETFA 2016). 6 to 9, Sep, 2016. Berlin, Germany.
Contract Based Verification of IEC 61499 CISTER-TR-161106 
Per Lindgren, Marcus Lindner, David Pereira, Luis Miguel Pinho14th International Conference on Industrial Informatics (INDIN 2016). 18 to 21, Jul, 2016, Factory Automation. Poitiers, France.
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.
Towards a Runtime Verification Framework for the Ada Programming Language CISTER-TR-140305 
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa PintoLecture Notes in Computer Science, Reliable Software Technologies – Ada-Europe 2014 (LNCS), Springer International Publishing. 23 to 27, Aug, 2014, 8454, pp 58-73.
RTFM-lang Static Semantics for Systems with Mixed Criticality CISTER-TR-140625 
Per Lindgren, Johan Eriksson, Marcus Lindner, David Pereira, Luis Miguel PinhoProc of Workshop on Mixed Criticality for Industrial Systems (WMCIS’2014), Ada User Journal, 35(2):128–132, 2014. (WMCIS 2014). 23 to 26, Jun, 2014. Paris, France.
A Compositional Monitoring Framework for Hard Real-Time Systems CISTER-TR-140104 
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa PintoNASA Formal Methods Symposium 2014 (NFM14), Springer International Publishing. 29, Apr, 2014, LNCS 8430, pp 16-30. Houston, TX, U.S.A..
Logic-based Schedulability Analysis for Compositional Hard Real-Time Embedded Systems CISTER-TR-131201 
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa Pinto6th International Workshop on Compositional Theory and Technology for Real-Time Embedded Systems (CRTS 2013). 3, Dec, 2013. Vancouver, Canada.Co-located within the IEEE Real-Time Systems Symposium (RTSS'13).
Conference or Workshop Posters/Demos
Run-Time Monitoring Environments for Real-Time and Safety Critical Systems CISTER-TR-160208 
Geoffrey Nelissen, Humberto Carvalho, David Pereira, Eduardo TovarDemo in Demo Session, 22nd IEEE Real-Time Embedded Technology & Applications Symposium (RTAS 2016). 11 to 14, Apr, 2016. Austria.
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.
Verification of Hard Real-Time Systems CISTER-TR-140608 
David Pereira, André Pedro, Luis Miguel PinhoPoster presented in CISTER 1st Industrial Workshop on Real-Time and Embedded Systems (CiWork 2013). 18, Jun, 2013. Porto, Portugal.
Towards Specification and Verification Frameworks for Concurrent Real-Time Systems CISTER-TR-130109 
David Pereira, André Pedro, Luis Miguel Pinho, Jorge Sousa PintoPoster presented in High Integrity Language Technology ACM SIGAda’s Annual International Conference (HILT 2012). 2 to 6, Dec, 2012. Boston, U.S.A..
Technical Reports
Design and Implementation of Secret Key Agreement for Platoon-based Vehicular Cyber-Physical Systems CISTER-TR-181013 
Kai Li, Wei Ni, Yousef Emami, Yiran Shen, Ricardo Severino, David Pereira, Eduardo TovarAccepted in 2018.