Cookies Policy
We use cookies to improve our site and your experience. By continuing to browse our site you accept our cookie policy. Find out More
Close
  • Menu
About

About

Education: PhD in Computer Science, Faculdade de Ciências da Universidade do Porto, 2011.

Research interests: concurrency, software verification and testing, unmanned vehicle networks

Selected publications:

Short bio

  • Currently researcher at CRACS/INESC-TEC, Prof. Auxiliar Convidado 25% FCUP
  • 2012-2016: Prof. Auxiliar Convidado c/dedicação exclusiva, FCUL 
  • 2006-2011: PhD student in Computer Science, FCUP
  • 1998-2005: Software engineer/programmer for consulting companies (Portugal and Brazil)
  • 1998: MSc in Advanced Computing, Imperial College London
  • 1997: BSc in Computer Science (pre-Bologne), FCUP

Interest
Topics
Details

Details

  • Name

    Eduardo Brandão Marques
  • Cluster

    Computer Science
  • Role

    Researcher
  • Since

    01st April 2016
001
Publications

2017

Towards a middleware for mobile edge-cloud applications

Authors
Rodrigues, J; Marques, ERB; Lopes, LMB; Silva, F;

Publication
Proceedings of the 2nd Workshop on Middleware for Edge Clouds & Cloudlets - MECC '17

Abstract

2015

Towards programmable coordination of unmanned vehicle networks

Authors
Marques, ERB; Ribeiro, M; Pinto, J; Sousa, JB; Martins, F;

Publication
IFAC Proceedings Volumes (IFAC-PapersOnline)

Abstract
The use of unmanned vehicle networks for diverse applications is becoming widespread. It is generally hard to program unmanned vehicle networks as a "whole", however. The coordination of multiple vehicles requires careful planning through intricate human intervention, and a high degree of informality is implied in what concerns the specification of a "network program" for an application scenario. In this context, we have been developing a programming language for expressing global specifications of coordinated behavior in unmanned vehicle networks, the Networked Vehicles' Language (NVL). In this paper we illustrate the use of the language for a thermal pollution plume tracking scenario employing unmanned underwater vehicles.

2015

NVL: a coordination language for unmanned vehicle networks

Authors
Marques, ERB; Ribeiro, M; Pinto, J; Sousa, JB; Martins, F;

Publication
30TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, VOLS I AND II

Abstract
The coordinated use of multiple unmanned vehicles over a network can be employed for numerous real-world applications. However, multi-vehicle operations are often deployed through a patchwork of separate components that informally "glue" together during operation, as they are hard to program as a "whole". With this aim, we developed the Networked Vehicles' Language (NVL) for coordinated control of unmanned vehicle networks. A single NVL program expresses an on-the-fly selection of multiple vehicles and their allocation to cooperative tasks, subject to time, precedence, and concurrency constraints. We present the language through an example application involving unmanned underwater vehicles (UUVs) and unmanned aerial vehicles (UAVs), the core design and implementation traits, and results from simulation and field test experiments.

2015

Protocol-Based Verification of Message-Passing Parallel Programs

Authors
Lopez, HA; Marques, ERB; Martins, F; Ng, N; Santos, C; Vasconcelos, VT; Yoshida, N;

Publication
ACM SIGPLAN NOTICES

Abstract
We present ParTypes, a type-based methodology for the verification of Message Passing Interface (MPI) programs written in the C programming language. The aim is to statically verify programs against protocol specifications, enforcing properties such as fidelity and absence of deadlocks. We develop a protocol language based on a dependent type system for message-passing parallel programs, which includes various communication operators, such as point-to-point messages, broadcast, reduce, array scatter and gather. For the verification of a program against a given protocol, the protocol is first translated into a representation read by VCC, a software verifier for C. We successfully verified several MPI programs in a running time that is independent of the number of processes or other input parameters. This contrasts with alternative techniques, notably model checking and runtime verification, that suffer from the state-explosion problem or that otherwise depend on parameters to the program itself. We experimentally evaluated our approach against state-of-the-art tools for MPI to conclude that our approach offers a scalable solution.

2014

Cooperari: a tool for cooperative testing of multithreaded Java programs

Authors
Marques, ERB; Martins, F; Simões, M;

Publication
2014 International Conference on Principles and Practices of Programming on the Java Platform Virtual Machines, Languages and Tools, PPPJ '14, Cracow, Poland, September 23-26, 2014

Abstract
Bugs in multithreaded application can be elusive. They are often hard to trace and replicate, given the usual non-determinism and irreproducibility of scheduling decisions at runtime. We present Cooperari, a tool for deterministic testing of multithreaded Java code based on cooperative execution. In a cooperative execution, threads voluntarily suspend (yield) at interference points (e.g., lock acquisition), and code between two consecutive yield points of each thread always executes serially as a transaction. A cooperative scheduler takes over control at yield points and deterministically selects the next thread to run. An application test runs multiple times, until it either fails or the state-space of schedules is deemed as covered by a configurable policy that is responsible for the scheduling decisions. Beyond failed assertions in software tests, deadlocks and races are also detected as soon as they are exposed in the cooperative execution. Cooperari effectively finds, characterizes, and deterministically reproduces bugs that are not detected under unconstrained preemptive semantics, as illustrated by standard benchmark examples.