Frederico Ramos

Lisbon, Portugal

Welcome. My name is Frederico, and I am a PhD student in Computer Science at Instituto Superior Técnico (IST), supervised by Prof. José Fragoso Santos and Prof. Pedro Adão. I also work as a researcher in the ARSR Group at INESC-ID.

My research focuses on optimizing symbolic execution through techniques such as symbolic summaries, memory models, and path merging, with a current emphasis on C and JavaScript. These approaches aim to make analyses more scalable and precise.

I am broadly interested in formal methods, and programming languages, exploring how these areas intersect to improve software reliability and security.

Selected Talks and Publications

ECOOP’23

Toward Tool-Independent Summaries for Symbolic Execution

Frederico Ramos, Nuno Sabino, Pedro Adão, and 2 more authors

In 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States, 2023

DOI HTML PDF
ISSTA’23

MetaData262: Automatic Test Suite Selection for Partial JavaScript Implementations

Frederico Ramos, Diogo Costa Reis, Miguel Trigo, and 2 more authors

In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023, Seattle, WA, USA, July 17-21, 2023

DOI HTML PDF
Meta

Talk: Tool-Independent Summaries for Symbolic Execution

Frederico Ramos

In Meta, London Office,, Sep 2022
KLEE’22

Poster: Empirical Study of C Analysis Tools on Student Code

In 3rd International KLEE Workshop on Symbolic Execution, Imperial College of London,, Sep 2022
Master Thesis

Toward Tool-Independent Summaries for Symbolic Execution

Frederico Ramos

Nov 2021

Abs HTML PDF

Symbolic execution is a program analysis technique that has been successfully used to find various types of bugs in industrial codebases. Despite being extensively used in practice, this technique suffers from two main limitations when applied to real-world code: path explosion and interactions with the runtime environment. To address both of these problems, current symbolic execution engines make use of symbolic summaries. These interact with the symbolic state of a given program so as to simulate the behaviour of both external and internal functions without having to symbolically execute them. Symbolic summaries can therefore be used to mitigate the number of paths explored and also allow for the analysis of external calls. Despite their advantages, there is a clear lack of mechanisms for sharing symbolic summaries across different tools and for their uniform validation. In this thesis we introduce a methodology for implementing tool-independent symbolic summaries for the C programming language. This methodology consists of an API containing a set of symbolic reflec- tion primitives for explicit manipulation of C symbolic states. Symbolic summaries implemented using our API can be shared across different symbolic execution tools, provided that these tools implement the proposed API. Additionally, due to being written directly in C, these summaries can themselves be symbolically executed as standard C code. Hence, we also introduce a summary validation tool that can systematically evaluate the correctness of a symbolic summary with respect to its concrete reference implementation.