Frederico Ramos

Lisbon, Portugal

Greetings, my name is Frederico Ramos and I am a PhD student in computer science at Instituto Superior Técnico (IST) under the supervision of Prof. José Fragoso Santos and Prof. Pedro Adão. I am currently working on the synthesis of tool-independent summaries for symbolic execution. My main research interests are cybersecurity, formal methods and programming languages.

I am also a junior researcher at INESC-ID, studying the application of software verification tools to student’s code as part of their learning process in undergraduate courses.

In December 2021 I completed my MSc in Computer Science and Engineering at IST. My dissertation, entitled Toward Tool-Independent Summaries for Symbolic Execution, was supervised by Prof. José Fragoso Santos and Prof. Pedro Adão.

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

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

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.