Personal information

Real-Time Embedded Computing, Runtime and Deductive Software Verification, Formal Languages

Activities

Education and qualifications (3)

Universidade do Porto Faculdade de Ciências: Porto, PT

2007-09 to 2013-04-18 | Doutoramento (Ciência de Computadores)
Education
Source: Self-asserted source
David Pereira

Universidade do Porto Faculdade de Ciências: Porto, PT

2003-09 to 2007-05 | Mestrado (Ciência de Computadores)
Education
Source: Self-asserted source
David Pereira

Universidade do Porto Faculdade de Ciências: Porto, PT

1998-09 to 2003-09 | Licenciatura (Ciência de Computadores)
Education
Source: Self-asserted source
David Pereira

Professional activities (1)

University of Porto: Porto, PT

2013-04-18 | PhD with Honors
Distinction
Source: Self-asserted source
David Pereira

Funding (12)

Route 25 - Agenda for Autonomous, Intelligent, Interoperable and Inclusive Mobility

2022 to 2025 | Contract
Agência para a Competitividade e Inovação IP (Porto, PT)
Source: check_circle
CIÊNCIAVITAE

Aero.Next Portugal

2021 to 2025 | Contract
Agência para a Competitividade e Inovação IP (Porto, PT)
Source: check_circle
CIÊNCIAVITAE

VALU3S - Verification and Validation of Automated Systems’ Safety and Security

2020 to 2023 | Grant
EU Framework Programme for Research and Innovation Euratom (Brussels, BE)
Source: check_circle
CIÊNCIAVITAE

Secure Runtime Verification for Reliable Real-Time Embedded Software

2018-06 to 2021-05 | Contract
Fundação para a Ciência e a Tecnologia (Lisboa, PT)
Source: check_circle
CIÊNCIAVITAE

ENABLE-S3 - European Initiative to Enable Validation for Highly Automated Safe and Secure Systems

2016-05 to 2019-05 | Grant
EU Framework Programme for Research and Innovation Euratom (Brussels, BE)
Source: check_circle
CIÊNCIAVITAE

SafeCOP - Safe Cooperating Cyber-Physical Systems using Wireless Communication

2016-04 to 2019-06 | Grant
EU Framework Programme for Research and Innovation Euratom (Brussels, BE)
Source: check_circle
CIÊNCIAVITAE

EMC² - Embedded multi-core systems for mixed criticality applications in dynamic and changeable real-time environments

2014-04 to 2017-06 | Grant
Fundação para a Ciência e a Tecnologia (Lisboa, PT)
Source: check_circle
CIÊNCIAVITAE

CONCERTO - Guaranteed Component Assembly with Round Trip Analysis for Energy Efficient High-integrity Multi-core Systems

2013-05 to 2016-04 | Grant
Fundação para a Ciência e a Tecnologia (Lisboa, PT)
Source: check_circle
CIÊNCIAVITAE

Virtual Processor-based Multicore Scheduling (ViPCore)

2011-02 to 2014-06 | Grant
Stichting Weten (Amsterdam, NL)
Source: check_circle
CIÊNCIAVITAE
grade
Preferred source (of 2)‎

CANTE: Descriptional and computational complexity of formal languages

2010-05 to present | Grant
Fundação para a Ciência e a Tecnologia (Lisboa, PT)
Source: check_circle
CIÊNCIAVITAE

FAVAS: A FormAl Verification PlAtform for real-time Systems

2010-02 to 2013 | Grant
Universidade do Algarve Faculdade de Ciências e Tecnologia (Faro, PT)
Source: check_circle
CIÊNCIAVITAE

RESCUE, REliable and Safe Code execUtion for Embedded systems

2008-01 to 2011-03 | Grant
Stichting Weten (Amsterdam, NL)
Source: check_circle
CIÊNCIAVITAE
grade
Preferred source (of 2)‎

Works (38)

Exploiting Anytime Algorithms for Collaborative Service Execution in Edge Computing

Computers
2024-05-23 | Journal article
Contributors: Luís Nogueira; Jorge Coelho; David Pereira
Source: check_circle
Crossref
grade
Preferred source (of 2)‎

Secure integration of extremely resource-constrained nodes on distributed ROS2 applications

Open Research Europe
2023-07-14 | Journal article
Contributors: Giann Spilere Nandi; David Pereira; José Proença; Eduardo Tovar; Antonio Rodriguez; Pablo Garrido
Source: check_circle
Crossref
grade
Preferred source (of 2)‎

Verification of Multiple Models of a Safety-Critical Motor Controller in Railway Systems

2022 | Book chapter
Contributors: José Proença; Sina Borrami; Jorge Sanchez de Nova; David Pereira; Giann Spilere Nandi
Source: check_circle
Crossref
grade
Preferred source (of 2)‎

Real-time MTL with durations as SMT with applications to schedulability analysis

TASE 2020 - The 14th International Symposium on Theoretical Aspects of Software Engineering
2020-07-15 | Conference paper
SOURCE-WORK-ID:

cv-prod-id-1829980

Contributors: andré de matos pedro; Martin Leucker; PEREIRA, DAVID; Jorge Sousa Pinto
Source: check_circle
CIÊNCIAVITAE

Design and implementation of secret key agreement for platoon-based vehicular cyber-physical systems

ACM Transactions on Cyber-Physical Systems
2019 | Journal article
EID:

2-s2.0-85075638537

Contributors: Li, K.; Ni, W.; Emami, Y.; Shen, Y.; Severino, R.; Pereira, D.; Tovar, E.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

Security in wireless sensor networks: A formal verification of protocols

IEEE International Conference on Industrial Informatics (INDIN)
2019 | Conference paper
EID:

2-s2.0-85079062203

Contributors: Nandi, G.S.; Pereira, D.; Vigil, M.; Moraes, R.; Morales, A.S.; Araujo, G.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

Validation of Automated Farming

Validation and Verification of Automated Systems
2019 | Book chapter
SOURCE-WORK-ID:

cv-prod-id-1818866

Contributors: Rooker, M.; López, J. F.; Horstrand, P.; Pusenius, M.; Leppälampi, T.; Lattarulo, R.; Pérez, J.; et al.
Source: check_circle
CIÊNCIAVITAE

Runtime verification of autopilot systems using a fragment of MTL- ∫

International Journal on Software Tools for Technology Transfer
2018 | Journal article
EID:

2-s2.0-85028004115

Contributors: de Matos Pedro, A.; Pinto, J.S.; Pereira, D.; Pinho, L.M.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

End-to-End Response Time of IEC 61499 Distributed Applications over Switched Ethernet

IEEE Transactions on Industrial Informatics
2017 | Journal article
EID:

2-s2.0-85013444377

Contributors: Lindgren, P.; Eriksson, J.; Lindner, M.; Lindner, A.; Pereira, D.; Pinho, L.M.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

Formal Verification of AADL Models Using UPPAAL

2017 VII Brazilian Symposium on Computing Systems Engineering (SBESC)
2017 | Conference paper
Source: Self-asserted source
David Pereira
grade
Preferred source (of 3)‎

SMT-based Schedulability Analysis using RMTL- R

2017 | Conference paper
SOURCE-WORK-ID:

cv-prod-id-906512

Part of ISSN: 1551-3688
OTHER-ID:

André de Matos Pedro, David Pereira, Luís Miguel Pinho, and Jorge Sousa Pinto. 2017. SMT-based schedulability analysis using RMTL-¿. SIGBED Rev. 14, 3 (November 2017), 40-42.

Contributors: Pedro, André; Pereira, David; Pinho, Luís Miguel; Sousa Pinto, Jorge; Pedro, André Matos; Pinto, Jorge Sousa
Source: check_circle
CIÊNCIAVITAE

A Comparison of Formal Verification Approaches for IEC 61499

IEEE International Conference on Emerging Technologies and Factory Automation, ETFA
2016 | Conference paper
EID:

2-s2.0-84996483346

Contributors: Blech, J.O.; Lindgren, P.; Pereira, D.; Vyatkin, V.; Zoitl, A.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

Contract based verification of IEC 61499

IEEE International Conference on Industrial Informatics (INDIN)
2016 | Conference paper
EID:

2-s2.0-85012929062

Contributors: Lindgren, P.; Lindner, M.; Pereira, D.; Pinho, L.M.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

REVERT: Runtime Verification for Real-Time Systems

Proceedings - Real-Time Systems Symposium
2016 | Conference paper
EID:

2-s2.0-85011650189

Contributors: Kochanthara, S.; Nelissen, G.; Pereira, D.; Purandare, R.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

Towards certified compilation of RTFM-core applications

IEEE International Conference on Emerging Technologies and Factory Automation, ETFA
2016 | Conference paper
EID:

2-s2.0-84996490222

Contributors: Lindgren, P.; Lindner, M.; Pereira, D.; Pinho, L.M.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

A Formal Perspective on IEC 61499 Execution Control Chart Semantics

Proceedings - 14th IEEE International Conference on Trust, Security and Privacy in Computing and Communications, TrustCom 2015
2015 | Conference paper
EID:

2-s2.0-84969257751

Contributors: Lindgren, P.; Lindner, M.; Pereira, D.; Pinho, L.M.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

A novel run-time monitoring architecture for safe and efficient inline monitoring

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2015 | Book
EID:

2-s2.0-84947911174

Contributors: Nelissen, G.; Pereira, D.; Pinho, L.M.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

A Novel Run-Time Monitoring Architecture for Safe and Efficient Inline Monitoring

2015 | Conference paper
SOURCE-WORK-ID:

cv-prod-id-906513

Contributors: Nelissen, Geoffrey; Pereira, David; Pinho, Luís Miguel
Source: check_circle
CIÊNCIAVITAE

A Novel Runtime Monitoring Architecture

2015 | Other
SOURCE-WORK-ID:

cv-prod-id-906516

Contributors: Nelissen, Geoffrey; Pereira, David; Pinho, Luís Miguel
Source: check_circle
CIÊNCIAVITAE

A real-time semantics for the IEC 61499 standard

IEEE International Conference on Emerging Technologies and Factory Automation, ETFA
2015 | Conference paper
EID:

2-s2.0-84952918103

Contributors: Lindgren, P.; Lindner, M.; Lindner, A.; Vyatkin, V.; Pereira, D.; Pinho, L.M.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

Abstract Timers and their Implementation onto the ARM Cortex-M family of MCUs

CEUR Workshop Proceedings
2015 | Conference paper
EID:

2-s2.0-84949883481

Contributors: Lindgren, P.; Fresk, E.; Lindner, M.; Lulea, A.L.; Pereira, D.; Pinho, L.M.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

Deciding Kleene algebra terms equivalence in Coq

Journal of Logical and Algebraic Methods in Programming
2015 | Journal article
EID:

2-s2.0-84938689336

Contributors: Moreira, N.; Pereira, D.; Melo De Sousa, S.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 3)‎

Logic-based schedulability analysis for compositional hard real-time embedded systems

2015 | Journal article
SOURCE-WORK-ID:

cv-prod-id-906518

OTHER-ID:

A. M. Pedro, D. Pereira, L. M. Pinho, and J. S. Pinto. Logic-based schedulability analysis for compositional hard real-time embedded systems. In M. Behnam and G. Buttazzo, editors, Proceedings of the 6th International Workshop on Compositional Theory and

OTHER-ID:

A. M. Pedro, D. Pereira, L. M. Pinho, and J. S. Pinto. Logic-based schedulability analysis for compositional hard real-time embedded systems. In M. Behnam and G. Buttazzo, editors, Proceedings of the 6th International Workshop on Compositional Theory and

Part of ISSN: 1551-3688
Contributors: Pedro, André; Pereira, David; Pinho, Luís Miguel; Pinto, Jorge Sousa; Pedro, André Matos
Source: check_circle
CIÊNCIAVITAE

Monitoring for a decidable fragment of mtl-∫

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2015 | Book
EID:

2-s2.0-84950324017

Contributors: Pedro, A.M.; Pereira, D.; Pinho, L.M.; Pinto, J.S.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

Response time for IEC 61499 over Ethernet

Proceeding - 2015 IEEE International Conference on Industrial Informatics, INDIN 2015
2015 | Conference paper
EID:

2-s2.0-84949520365

Contributors: Lindgren, P.; Eriksson, J.; Lindner, M.; Lindner, A.; Pereira, D.; Pinho, L.M.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

RTFM-core: Language and implementation

Proceedings of the 2015 10th IEEE Conference on Industrial Electronics and Applications, ICIEA 2015
2015 | Conference paper
EID:

2-s2.0-84960919182

Contributors: Lindgren, P.; Lindner, M.; Lindner, A.; Pereira, D.; Pinho, L.M.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

Run-time Monitoring Architecture for RealTime Systems

2015 | Conference paper
SOURCE-WORK-ID:

cv-prod-id-906511

Contributors: Nelissen, Geoffrey; Pereira, David; Pinho, Luís Miguel
Source: check_circle
CIÊNCIAVITAE

Well-formed control flow for critical sections in RTFM-core

Proceeding - 2015 IEEE International Conference on Industrial Informatics, INDIN 2015
2015 | Conference paper
EID:

2-s2.0-84949489320

Contributors: Lindgren, P.; Lindner, M.; Lindner, A.; Pereira, D.; Pinho, L.M.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

A compositional monitoring framework for hard real-time systems

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2014 | Book
EID:

2-s2.0-84901660486

Contributors: De Matos Pedro, A.; Pereira, D.; Pinho, L.M.; Pinto, J.S.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

RTFM-lang static semantics for systems with mixed criticality

Ada User Journal
2014 | Journal article
EID:

2-s2.0-84905508995

Contributors: Lindgren, P.; Eriksson, J.; Lindner, M.; Pereira, D.; Pinho, L.M.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

Towards a runtime verification framework for the Ada programming language

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2014 | Book
EID:

2-s2.0-84903629798

Contributors: De Matos Pedro, A.; Pereira, D.; Pinho, L.M.; Pinto, J.S.
Source: Self-asserted source
David Pereira via Scopus - Elsevier
grade
Preferred source (of 2)‎

Towards certified program logics for the verification of imperative programs

2013 | Dissertation or Thesis
SOURCE-WORK-ID:

cv-prod-id-906517

Contributors: David Miguel Ramalho Pereira
Source: check_circle
CIÊNCIAVITAE

Deciding regular expressions (in-)equivalence in Coq

Lecture Notes in Computer Science
2012 | Conference paper
Source: Self-asserted source
David Pereira
grade
Preferred source (of 3)‎

Towards specification and verification frameworks for concurrent real-time systems

2012 | Other
SOURCE-WORK-ID:

cv-prod-id-906521

OTHER-ID:

D. Pereira, A. Pedro, L. M. Pinho, and J. S. Pinto. Towards specification and verification frameworks for concurrent real-time systems. Poster presented at High Integrity Language Technology, ACM SIGAdas Annual International Conference (HILT2012), 2012.

OTHER-ID:

D. Pereira, A. Pedro, L. M. Pinho, and J. S. Pinto. Towards specification and verification frameworks for concurrent real-time systems. Poster presented at High Integrity Language Technology, ACM SIGAda’s Annual International Conference (HILT’2012), 2012.

Contributors: Pereira, David; Pedro, André Matos; Pinho, Luís Miguel; Pinto, Jorge Sousa
Source: check_circle
CIÊNCIAVITAE

Partial derivative automata formalized in coq

Lecture Notes in Computer Science
2011 | Conference paper
Source: Self-asserted source
David Pereira
grade
Preferred source (of 3)‎

Formal modelling of emotions in BDI agents

Lecture Notes in Computer Science
2008 | Conference paper
Source: Self-asserted source
David Pereira
grade
Preferred source (of 3)‎

KAT and PHL in Coq

Computer Science and Information Systems
2008 | Journal article
Source: Self-asserted source
David Pereira
grade
Preferred source (of 3)‎

Towards an Architecture for Emotional BDI Agents

EPIA'05: Proceedings of the EPIA'05 12th Portuguese Conference on Artificial Intelligence
2005 | Conference paper
Source: Self-asserted source
David Pereira
grade
Preferred source (of 2)‎