Demo Data from EDBT 2026 / reviewers in the wild / expert
Nuno Machado
dblp:117/8012
· DBLP profile ↗
14ranked-venue papers
6as first author
2since 2021 · last 2025
0000-0003-1531-1875ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Systems, architecture and hardware · 6 · 2 first-author · 1 since 2021Security and privacy · 4 · 1 first-author · 1 since 2021Software engineering, systems software and programming languages · 4 · 3 first-authorArtificial intelligence and machine learning · 1Graphics, computer vision, multimedia, augmented reality and games · 1Applied, interdisciplinary, general and emerging computing · 1 · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Software engineering, system software, and programming languages
4 papers |
Debugging and program repair · 68% Concurrent programming · 32% | |
| Theoretical computer science
1 paper |
Automated reasoning and model checking · 100% |
Topics — the 7 heaviest of 7, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Debugging and program repair
concurrent program debugging |
1.1 | 4 | 2019 | Concurrency Debugging with MaxSMT · AAAI 2019 Concurrency Debugging with Differential Schedule Projections · ACM Trans. Softw. Eng. Methodol. 2016 Production-guided concurrency debugging · PPoPP 2016 |
Concurrent programming
concurrency bugs |
0.7 | 3 | 2016 | Concurrency Debugging with Differential Schedule Projections · ACM Trans. Softw. Eng. Methodol. 2016 Production-guided concurrency debugging · PPoPP 2016 Concurrency debugging with differential schedule projections · PLDI 2015 |
Automated reasoning and model checking › satisfiability
maximum satisfiability |
0.4 | 1 | 2019 | Concurrency Debugging with MaxSMT · AAAI 2019 |
Automated reasoning and model checking › satisfiability modulo theories
MaxSMT |
0.4 | 1 | 2019 | Concurrency Debugging with MaxSMT · AAAI 2019 |
Debugging and program repair
fault localization |
0.2 | 1 | 2016 | Concurrency Debugging with Differential Schedule Projections · ACM Trans. Softw. Eng. Methodol. 2016 |
Debugging and program repair
bug reproduction |
0.1 | 1 | 2016 | Production-guided concurrency debugging · PPoPP 2016 |
Debugging and program repair
root cause analysis |
0.1 | 1 | 2016 | Concurrency Debugging with Differential Schedule Projections · ACM Trans. Softw. Eng. Methodol. 2016 |
Methods — techniques the papers use, named apart from their topics
SMT solving · 0.8thread path profiling · 0.5symbolic constraint solving · 0.5MaxSMT · 0.4Max-SMT · 0.4schedule perturbation · 0.2production-guided search · 0.2differential schedule projections · 0.2
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | A Multiple BLE Beacon Approach for Tracking in Industrial Environments
Moisés Ramires, Joaquín Torres-Sospedra, Joel Puga, Nuno Machado, Adriano J. C. Moreira, Filipe Meneses |
IPIN | 4 |
| 2021 | Horus: Non-Intrusive Causal Analysis of Distributed Systems LogsabstractLogs are still the primary resource for debugging distributed systems executions. Complexity and heterogeneity of modern distributed systems, however, make log analysis extremely challenging. First, due to the sheer amount of messages, in which the execution paths of distinct system components appear interleaved. Second, due to unsynchronized physical clocks, simply ordering the log messages by timestamp does not suffice to obtain a causal trace of the execution. To address these issues, we present Horus, a system that enables the refinement of distributed system logs in a causally-consistent and scalable fashion. Horus leverages kernel-level probing to capture events for tracking causality between application-level logs from multiple sources. The events are then encoded as a directed acyclic graph and stored in a graph database, thus allowing the use of rich query languages to reason about runtime behavior. Our case study with TrainTicket, a ticket booking application with 40+ microservices, shows that Horus surpasses current widely-adopted log analysis systems in pinpointing the root cause of anomalies in distributed executions. Also, we show that Horus builds a causally-consistent log of a distributed execution with much higher performance (up to 3 orders of magnitude) and scalability than prior state-of-the-art solutions. Finally, we show that Horus' approach to query causality is up to 30 times faster than graph database built-in traversal algorithms. Francisco Neves, Nuno Machado, Ricardo Vilaça, José Pereira 0001 |
DSN | 2 |
| 2020 | Exploiting Symbolic Execution to Accelerate Deterministic DatabasesabstractDeterministic databases (DDs) are a promising approach for replicating data across different replicas. A fundamental component of DDs is a deterministic concurrency control algorithm that, given a set of transactions in a specific order, guarantees that their execution always results in the same serial order. State-of-the-art approaches either rely on single threaded execution or on the knowledge of read- and write-sets of transactions to achieve this goal. The former yields poor performance in multi-core machines while the latter requires either manual inputs from the user - a time-consuming and error prone task - or a reconnaissance phase that increases both the latency and abort rates of transactions. In this paper, we present Prognosticator, a novel deterministic database system. Rather than relying on manual transaction classification or an expert programmer, Prognosticator employs Symbolic Execution to build fine-grained transaction profiles (at the key-level). These profiles are then used by Prognosticator's novel deterministic concurrency control algorithm to execute transactions with a high degree of parallelism.Our experimental evaluation, based on both TPC-C and RUBiS benchmarks, shows that Prognosticator can achieve up to 5× higher throughput with respect to state-of-the-art solutions. Shady Issa, Miguel Viegas, Pedro Raminhas, Nuno Machado, Miguel Matos, Paolo Romano 0002 |
ICDCS | 4 |
| 2019 | Concurrency Debugging with MaxSMTabstractCurrent Maximum Satisfiability (MaxSAT) algorithms based on successive calls to a powerful Satisfiability (SAT) solver are now able to solve real-world instances in many application domains. Moreover, replacing the SAT solver with a Satisfiability Modulo Theories (SMT) solver enables effective MaxSMT algorithms. However, MaxSMT has seldom been used in debugging multi-threaded software.Multi-threaded programs are usually non-deterministic due to the huge number of possible thread operation schedules, which makes them much harder to debug than sequential programs. A recent approach to isolate the root cause of concurrency bugs in multi-threaded software is to produce a report that shows the differences between a failing and a non-failing execution. However, since they rely solely on heuristics, these reports can be unnecessarily large. Hence, reports may contain operations that are not relevant to the bug’s occurrence.This paper proposes the use of MaxSMT for the generation of minimal reports for multi-threaded software with concurrency bugs. The proposed techniques report situations that the existing techniques are not able to identify. Experimental results show that using MaxSMT can significantly improve the accuracy of the generated reports and, consequently, their usefulness in debugging the root cause of concurrency bugs. Miguel Terra-Neves, Nuno Machado, Inês Lynce, Vasco Manquinho |
AAAI | 2 |
| 2019 | Minha: Large-Scale Distributed Systems Testing Made PracticalabstractTesting large-scale distributed system software is still far from practical as the sheer scale needed and the inherent non-determinism make it very expensive to deploy and use realistically large environments, even with cloud computing and state-of-the-art automation. Moreover, observing global states without disturbing the system under test is itself difficult. This is particularly troubling as the gap between distributed algorithms and their implementations can easily introduce subtle bugs that are disclosed only with suitably large scale tests. We address this challenge with Minha, a framework that virtualizes multiple JVM instances in a single JVM, thus simulating a distributed environment where each host runs on a separate machine, accessing dedicated network and CPU resources. The key contributions are the ability to run off-the-shelf concurrent and distributed JVM bytecode programs while at the same time scaling up to thousands of virtual nodes; and enabling global observation within standard software testing frameworks. Our experiments with two distributed systems show the usefulness of Minha in disclosing errors, evaluating global properties, and in scaling tests orders of magnitude with the same hardware resources. Nuno Machado, Francisco Maia 0001, Francisco Neves, Fábio Coelho 0001, José Pereira 0001 |
OPODIS | 1 |
| 2019 | d'Artagnan: A Trusted NoSQL Database on Untrusted CloudsabstractPrivacy sensitive applications that store confidential information such as personal identifiable data or medical records have strict security concerns. These concerns hinder the adoption of the cloud. With cloud providers under the constant threat of malicious attacks, a single successful breach is sufficient to exploit any valuable information and disclose sensitive data. Existing privacy-aware databases mitigate some of these concerns, but sill leak critical information that can potently compromise the entire system's security. This paper proposes d'Artagnan, the first privacy-aware multi-cloud NoSQL database framework that renders database leaks worthless. The framework stores data as encrypted secrets in multiple clouds such that i) a single data breach cannot break the database's confidentiality and ii) queries are processed on the server-side without leaking any sensitive information. d'Artagnan is evaluated with industry-standard benchmark on market-leading cloud providers. Rogerio Pontes, Francisco Maia 0001, Ricardo Vilaça, Nuno Machado |
SRDS | 4 |
| 2018 | Totally Ordered Replication for Massive Scale Key-Value Stores
Nuno Machado, Francisco Maia 0001, Miguel Matos |
DAIS | 2 |
| 2018 | Falcon: A Practical Log-Based Analysis Tool for Distributed SystemsabstractProgrammers and support engineers typically rely on log data to narrow down the root cause of unexpected behaviors in dependable distributed systems. Unfortunately, the inherently distributed nature and complexity of such distributed executions often leads to multiple independent logs, scattered across different physical machines, with thousands or millions entries poorly correlated in terms of event causality. This renders log-based debugging a tedious, time-consuming, and potentially inconclusive task. We present Falcon, a tool aimed at making log-based analysis of distributed systems practical and effective. Falcon's modular architecture, designed as an extensible pipeline, allows it to seamlessly combine several distinct logging sources and generate a coherent space-time diagram of distributed executions. To preserve event causality, even in the presence of logs collected from independent unsynchronized machines, Falcon introduces a novel happens-before symbolic formulation and relies on an off-the-shelf constraint solver to obtain a coherent event schedule. Our case study with the popular distributed coordination service Apache Zookeeper shows that Falcon eases the log-based analysis of complex distributed protocols and is helpful in bridging the gap between protocol design and implementation. Francisco Neves, Nuno Machado, José Pereira 0001 |
DSN | 2 |
| 2018 | CoopREP: Cooperative record and replay of concurrency bugsabstractSummary This paper presents CoopREP, a system that provides support for fault replication of concurrent programs based on cooperative recording and partial log combination. CoopREP uses partial logging to reduce the amount of information that a given program instance is required to store to support deterministic replay. This allows reducing substantially the overhead imposed by the instrumentation of the code, but raises the problem of finding a combination of logs capable of replaying the fault. CoopREP tackles this issue by introducing several innovative statistical analysis techniques aimed at guiding the search of the partial logs to be combined and needed for the replay phase. CoopREP has been evaluated using both standard benchmarks for multithreaded applications and real‐world applications. The results highlight that CoopREP can successfully replay concurrency bugs involving tens of thousands of memory accesses, while reducing recording overhead with respect to state‐of‐the‐art noncooperative logging schemes by up to 13× (and by 2.4× on average). Nuno Machado, Paolo Romano 0002, Luís E. T. Rodrigues |
Softw. Test. Verification Reliab. | 1 |
| 2017 | Automatic technology migration of analog IC designs using generic cell librariesabstractThis paper addresses the problem of automatic technology migration of analog IC designs. The proposed method introduces a new level of abstraction, for EDA tools addressing analog IC design, allowing a systematic and effortless adaption of a design to a new technology. The new abstraction level is based on generic cell libraries, which includes topology and testbenches descriptions for specific circuit classes. In addition to technology independence, reusing the testbenches when adding new topologies for the already implemented circuit classes also improves design productivity. The new method is implemented and tested using a state-of-the-art multi-objective multi-constraint circuit-level optimization tool for circuit sizing, and is validated for the design and optimization of continuous-time comparators, including technology migration between two different design nodes, respectively, XFAB 350 nm technology and ATMEL 150 nm SOI technology. Jose Cachaco, Nuno Machado, Nuno Lourenço 0003, Jorge Guilherme, Nuno Horta |
DATE | 2 |
| 2016 | Production-guided concurrency debuggingabstractConcurrency bugs that stem from schedule-dependent branches are hard to understand and debug, because their root causes imply not only different event orderings, but also changes in the control-flow between failing and non-failing executions. We present Cortex: a system that helps exposing and understanding concurrency bugs that result from schedule-dependent branches, without relying on information from failing executions. Cortex preemptively exposes failing executions by perturbing the order of events and control-flow behavior in non-failing schedules from production runs of a program. By leveraging this information from production runs, Cortex synthesizes executions to guide the search for failing schedules. Production-guided search helps cope with the large execution search space by targeting failing executions that are similar to observed non-failing executions. Evaluation on popular benchmarks shows that Cortex is able to expose failing schedules with only a few perturbations to non-failing executions, and takes a practical amount of time. Nuno Machado, Brandon Lucia, Luís E. T. Rodrigues |
PPoPP | 1 |
| 2016 | Concurrency Debugging with Differential Schedule ProjectionsabstractWe present Symbiosis: a concurrency debugging technique based on novel differential schedule projections (DSPs). A DSP shows the small set of memory operations and dataflows responsible for a failure, as well as a reordering of those elements that avoids the failure. To build a DSP, Symbiosis first generates a full, failing, multithreaded schedule via thread path profiling and symbolic constraint solving. Symbiosis selectively reorders events in the failing schedule to produce a nonfailing, alternate schedule . A DSP reports the ordering and dataflow differences between the failing and nonfailing schedules. Our evaluation on buggy real-world software and benchmarks shows that, in practical time, Symbiosis generates DSPs that both isolate the small fraction of event orders and dataflows responsible for the failure and report which event reorderings prevent failing. In our experiments, DSPs contain 90% fewer events and 96% fewer dataflows than the full failure-inducing schedules. We also conducted a user study that shows that, by allowing developers to focus on only a few events, DSPs reduce the amount of time required to understand the bug’s root cause and find a valid fix. Nuno Machado, Daniel Quinta, Brandon Lucia, Luís E. T. Rodrigues |
ACM Trans. Softw. Eng. Methodol. | 1 |
| 2015 | Concurrency debugging with differential schedule projectionsabstractWe present Symbiosis: a concurrency debugging technique based on novel differential schedule projections (DSPs). A DSP shows the small set of memory operations and data-flows responsible for a failure, as well as a reordering of those elements that avoids the failure. To build a DSP, Symbiosis first generates a full, failing, multithreaded schedule via thread path profiling and symbolic constraint solving. Symbiosis selectively reorders events in the failing schedule to produce a non-failing, alternate schedule. A DSP reports the ordering and data-flow differences between the failing and non-failing schedules. Our evaluation on buggy real-world software and benchmarks shows that, in practical time, Symbiosis generates DSPs that both isolate the small fraction of event orders and data-flows responsible for the failure, and show which event reorderings prevent failing. In our experiments, DSPs contain 81% fewer events and 96% less data-flows than the full failure-inducing schedules. Moreover, by allowing developers to focus on only a few events, DSPs reduce the amount of time required to find a valid fix. Nuno Machado, Brandon Lucia, Luís E. T. Rodrigues |
PLDI | 1 |
| 2012 | Lightweight cooperative logging for fault replication in concurrent programsabstractThis paper presents CoopREP, a system that provides support for fault replication of concurrent programs, based on cooperative recording and partial log combination. CoopREP employs partial recording to reduce the amount of information that a given program instance is required to store in order to support deterministic replay. This allows to substantially reduce the overhead imposed by the instrumentation of the code, but raises the problem of finding the combination of logs capable of replaying the fault. CoopREP tackles this issue by introducing several innovative statistical analysis techniques aimed at guiding the search of partial logs to be combined and used during the replay phase. CoopREP has been evaluated using both standard benchmarks for multi-threaded applications and a real-world application. The results highlight that CoopREP can successfully replay concurrency bugs involving tens of thousands of memory accesses, reducing logging overhead with respect to state of the art non-cooperative logging schemes by up to 50 times in computationally intensive applications. Nuno Machado, Paolo Romano 0002, Luís E. T. Rodrigues |
DSN | 1 |