About me

I obtained a degree in Computer Science at the Universidad Nacional de Rosario, Argentina, and a Master in Software and Systems at the Universidad Politécnica de Madrid (UPM), Spain. I completed my PhD at the IMDEA Software Institute, Spain, under the supervision of César Sánchez, and continued there as a postdoctoral researcher. I am currently the Technical Lead of the development team at an AI-based agricultural company.

Curriculum Vitæ

Here you can download the most updated version of my cv.

Research Interests

I'm interested in Formal Methods and Software Engineering in general, and in particular, Runtime Verification and Reactive Synthesis.

Publications

• Andoni Rodríguez, Felipe Gorostiaga, César Sánchez:
  Counter Example Guided Reactive Synthesis for LTL Modulo Theories
• Matías Brizzio, Felipe Gorostiaga, César Sánchez, Renzo Degiovanni:
  Mode-based reactive synthesis
• Felipe Gorostiaga, Martín Ceresa, César Sánchez:
  MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs
• Andoni Rodríguez, Felipe Gorostiaga, César Sánchez:
  Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
• Margarita Capretto, Martín Ceresa, Felipe Gorostiaga, Fernando Macias, Paloma Pedregal, César Sánchez:
  Offchain Runtime Verification (for The Tezos Blockchain)
• Felipe Gorostiaga, César Sánchez:
  General monitorability of totally ordered verdict domains
• Paloma Pedregal, Felipe Gorostiaga, César Sánchez:
  A Stream Runtime Verification Tool with Nested and Retroactive Parametrization
• Felipe Gorostiaga, César Sánchez:
  Runtime verification of real-time event streams using the tool HStriver
• Felipe Gorostiaga, César Sánchez:
  Monitorability of Expressive Verdicts
• Felipe Gorostiaga, César Sánchez:
  HStriver: a very functional extensible tool for the runtime verification of real-time event streams
• Felipe Gorostiaga, César Sánchez:
  Nested Monitors: Monitors as Expressions to Build Monitors
• Sebastián Zudaire, Felipe Gorostiaga, César Sánchez, Gerardo Schneider, Sebastián Uchitel:
  Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Executions
• Felipe Gorostiaga, César Sánchez:
  Stream runtime verification of real-time event streams with the Striver language
• Felipe Gorostiaga, César Sánchez:
  HLola: a Very Functional Tool for Extensible Stream Runtime Verification
• Martín Ceresa, Felipe Gorostiaga, César Sánchez:
  Declarative Stream Runtime Verification (hLola)
• Felipe Gorostiaga, Luis Miguel Danielsson, César Sánchez:
  Unifying the Time-Event Spectrum for Stream Runtime Verification
• Carlos Luna, Gustavo Betarte, Juan Diego Campo, Camila Sanz, Maximiliano Cristiá, Felipe Gorostiaga:
  A formal approach for the verification of the permission-based security model of Android
• Pablo Chico de Guzmán, Felipe Gorostiaga, César Sánchez:
  Pipekit: A Deployment Tool with Advanced Scheduling and Inter-Service Communication for Multi-Tier Applications
• Felipe Gorostiaga, César Sánchez:
  Striver: Stream Runtime Verification for Real-Time Event-Streams
• Pablo Chico de Guzmán, Felipe Gorostiaga, César Sánchez:
  i2kit: A Deployment Tool with the Simplicity of Containers and the Security of Virtual Machines
• Gustavo Betarte, Juan Diego Campo, Maximiliano Cristiá, Felipe Gorostiaga, Carlos Luna, Camila Sanz:
  Towards formal model-based analysis and testing of Android's security mechanisms
• Gustavo Betarte, Juan Diego Campo, Felipe Gorostiaga, Carlos Luna:
  A Certified Reference Validation Mechanism for the Permission Model of Android

Theses

• Author: Felipe Gorostiaga
  Supervisors: Gustavo Betarte, Carlos Luna
  Co-Supervisor: Juan Diego Campo
  Especificación e implementación de un prototipo certificado del sistema de permisos de Android
  (Licentiate degree thesis)
• Author: Felipe Gorostiaga
  Supervisor: Lars-Åke Fredlund
  Co-Supervisor: César Sánchez
  Towards a stream-based monitoring language for asynchronous systems
  (Master's degree thesis)
• Author: Felipe Gorostiaga
  Supervisor: César Sánchez
  Theory and Practice of Stream Runtime Verification for Sequences and Real-Time Event Based Systems
  (PhD thesis)