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.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Thesis
Towards Certified Program Logics for the Verification of Imperative Programs CISTER-TR-130408 
David PereiraPhD Thesis. 2013. Porto, Portugal.
Journal Papers
Design and Implementation of Secret Key Agreement for Platoon-based Vehicular Cyber-physical Systems CISTER-TR-191103 
Kai Li, Wei Ni, Yousef Emami, Yiran Shen, Ricardo Severino, David Pereira, Eduardo TovarACM Transactions on Cyber-Physical Systems, Article No 22, ACM. 22, Nov, 2019, Volume 4, Issue 2, pp 22:1-22:20.
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/Talks
Reducing the gap between theory and practice in real-time systems with MARS CISTER-TR-240602 
Giann Nandi, David Pereira, José Proença, Eduardo Tovar, Luis Miguel NogueiraDependable Systems and Networks (DSN 2024). 24 to 27, Jun, 2024, Doctoral Forum. Brisbane, Australia.
Secure integration of extremely resource-constrained nodes on distributed ROS2 applications CISTER-TR-230703 
Giann Nandi, David Pereira, José Proença, Eduardo Tovar, Aythami Salvador RodriguezOpen Research Europe (ORE). 14, Jul, 2023. Online, Albania.
Spreadsheet-based Configuration of Families of Real-Time Specifications CISTER-TR-230407 
José Proença, Sina Borrami, Jorge Sanchez de Nova, David Pereira, Giann NandiProceedings of the First Workshop on Trends in Configurable Systems Analysis (TiCSA 2023). 23, Apr, 2023. Paris, France.
MARS: a toolset for the safe and secure deployment of heterogeneous distributed systems CISTER-TR-221101 
Giann Nandi, David Pereira, José Proença, José Santos, Lourenço A. Rodrigues, André Lourenço, Eduardo TovarReal-Time Systems Symposium (RTSS). 5 to 8, Dec, 2022, Explainability of Real-Time Systems and their Analysis. Houston, U.S.A..
Verification of multiple models of a safety-critical motor controller in railway systems CISTER-TR-220504 
José Proença, Sina Borrami, Jorge Sanchez de Nova, David Pereira, Giann NandiReliability, Safety, and Security of Railway Systems (RSSRail 2022). 1 to 2, Jun, 2022, Safety and new technologies, pp 83-94. Paris, France.
A Proposal for the Classification of Methods for Verification and Validation of Safety, Cybersecurity, and Privacy of Automated Systems CISTER-TR-210905 
Giann Nandi, Jose Luis de la Vara, Thomas Bauer, Bernhard Fischer, Mustafa Karaca, Henrique Madeira, Martin Matschnig, Silvia Mazzini, Fabio Patrone, David Pereira, José Proença, Rupert Sclick, Stefano Tonetta, Ugur Yayan, Behrooz Sangchoolie14th International Conference on the Quality of Information and Communications Technology (QUATIC 2021). 8, Sep, 2021. Portugal.
Towards the safe deployment of runtime monitors in mode-change supported Cyber-Physical Systems CISTER-TR-210612 
Giann Nandi, David Pereira, José Proença, Eduardo Tovar4th Doctoral Congress in Engineering (DCE 2021). 28 to 29, Jun, 2021, Symposium on Electrical and Computer Engineering. Porto, Portugal.
Towards the safe deployment of runtime monitors in mode-change supported Cyber-Physical Systems CISTER-TR-210608 
Giann Nandi, David Pereira, José Proença, Eduardo Tovar4th Doctoral Congress in Engineering (DCE 21). 28 to 29, Jun, 2021, Symposium on Electrical and Computer Engineering. Porto, Portugal.
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.
A Domain Specific Language for Automotive Systems Integration CISTER-TR-190806 
Renato Oliveira, David Pereira, Cláudio Maia, Pedro José Santos45th Annual Conference of the IEEE Industrial Electronics Society (IECON 2019). 14 to 17, Oct, 2019, SS Emerging Solutions for Vehicular Embedded Systems, pp 4483-4488. Lisbon, Portugal.
Security in Wireless Sensor Networks: A formal verification of protocols CISTER-TR-190506 
Giann Nandi, David Pereira, Martín Vigil, Ricardo Moraes, Analúcia Schiaffino Morales, Gustavo Araújo17th IEEE International Conference on Industrial Informatics (INDIN 2019). 22 to 25, Jul, 2019, Safety and Security in Industrial Applications, pp 425-431. Helsinki-Espoo, Finland.
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: 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.
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.
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
Verificattion of Multiple Models of a Safety-Critical Motor Controller in Railway Systems CISTER-TR-220611 
José Proença, Sina Borrami, Jorge Sanchez de Nova, David Pereira, Giann Nandi13, Jun, 2022.
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 Tovar2018.