Ruben Martins

Biography

Ruben Martins is an Assistant Research Professor at Carnegie Mellon University. His interests lie in the intersection of constraint programming with program synthesis, analysis, and verification. His recent research focuses on pushing the boundaries of program synthesis and enabling the technology to make programming and formal methods tools more accessible. Ruben received his Ph.D. with honors from the Technical University of Lisbon, Portugal (2013). He was a postdoctoral researcher at the University of Oxford, UK (2014-2015) and a postdoctoral researcher at UT Austin (2015-2017). He has published in top-tier venues, including POPL, PLDI, FSE, SAT, and CP. He has won a distinguished paper award at PLDI 2018 for his work on program synthesis, FSE 2021 for his work on optimization, and SAT 2022 for his work on verified encodings. He has also developed several award-winning constraint solvers. He is the leading developer of Open-WBO: an open-source Maximum Satisfiability (MaxSAT) solver that won several gold medals in MaxSAT competitions. Open-WBO is used to solve many real-world discrete optimization problems, including finding an optimal seating arrangement for his wedding.

Publications

• 2024

  Aidan Z. H. Yang, Claire Le Goues, Ruben Martins, Vincent J. Hellendoorn

  Large Language Models for Test-Free Fault Localization

  In International Conference on Software Engineering (ICSE’24), ACM, 2024.

  Anup Agarwal, Venkat Arun, Devdeep Ray, Ruben Martins, Srinivasan Seshan

  Towards provably performant congestion control

  In Network and Distributed System Security Symposium (NSDI’24), USENIX Association, 2024.

  Soojin Moon, Milind Srivastava, Yves Bieri, Ruben Martins, Vyas Sekar

  Pryde: A Modular Generalizable Workflow for Uncovering Evasion Attacks Against Stateful Firewall Deployments

  In Symposium on Security and Privacy (S&P’24), IEEE, 2024.

  Ricardo Brancas, Miguel Terra-Neves, Miguel Ventura, Vasco Manquinho, Ruben Martins

  Towards Reliable SQL Synthesis: Fuzzing-Based Evaluation and Disambiguation

  In International Conference on Fundamental Approaches to Software Engineering (FASE’24), Springer, 2024.
• 2023

  Stephan Gocht, Ruben Martins, Jakob Nordström, Andy Oertel

  Certified CNF Translations for Pseudo-Boolean Solving (Extended Abstract)

  In International Joint Conference on Artificial Intelligence (IJCAI’23), ijcai.org, 2023.

  Daniel Ramos, Hailie Mitchell, Ines Lynce, Vasco Manquinho, Ruben Martins, Claire Le Goues

  MELT: Mining Effective Lightweight Transformations from Pull Requests

  In Automated Software Engineering Conference (ASE’23), IEEE, 2023.

  Pedro Orvalho, Vasco Manquinho, Ruben Martins

  UpMax: User Partitioning for MaxSAT

  In International Conference on Theory and Applications of Satisfiability Testing (SAT’23), LIPIcs, 2023.
• 2022

  Anup Agarwal, Venkat Arun, Devdeep Ray, Ruben Martins, Srinivasan Seshan

  Automating network heuristic design and analysis

  In Workshop on Hot Topics in Networks (HotNets’22), ACM, 2022.

  Stephan Gocht, Ruben Martins, Jakob Nordström, Andy Oertel

  Certified CNF Translations for Pseudo-Boolean Solving

  In International Conference on Theory and Applications of Satisfiability Testing (SAT’22), LIPIcs, 2022. Best Paper Award.

  Francisco Pereira, Gonçalo Matos, Hugo Sadok, Daehyeok Kim, Ruben Martins, Justine Sherry, Fernando Ramos, Luis Pedrosa

  Automatic generation of network function accelerators using component-based synthesis

  In ACM SIGCOMM Symposium on SDN Research (SOSR’22), ACM, 2022.
• 2021

  Fahiem Bacchus, Matti Järvisalo, Ruben Martins

  Maximum Satisfiability

  In Handbook of Satisfiability, IOS, 2021.

  Margarida Ferreira, Akshay Narayan, Inês Lynce, Ruben Martins, Justine Sherry

  Counterfeiting Congestion Control Algorithms

  In Workshop on Hot Topics in Networks (HotNets’21), ACM, 2021.

  Changjian Zhang, Ryan Wagner, Pedro Orvalho, David Garlan, Vasco Manquinho, Ruben Martins, Eunsuk Kang

  AlloyMax: Bringing Maximum Satisfaction to Relational Specifications

  In Symposium on the Foundations of Software Engineering (FSE’21), ACM, 2021. Distinguished Paper Award.

  Yoshiki Takashima, Ruben Martins, Limin Jia, Corina S Pasareanu

  SyRust: Automatic Testing of Rust Libraries with Semantic-Aware Program Synthesis

  In Conference on Programming Language Design and Implementation (PLDI’21), ACM, 2021.

  Ansong Ni, Daniel Ramos, Aidan Yang, Inês Lynce, Vasco Manquinho, Ruben Martins, Claire Le Goues

  SOAR: A Synthesis Approach for Data Science API Refactoring

  In International Conference on Software Engineering (ICSE’21), ACM, 2021.

  Margarida Ferreira, Miguel Terra-Neves, Miguel Ventura, Inês Lynce, Ruben Martins

  FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions

  In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’21), Springer, 2021.

  Travis Hance, Marijn Heule, Ruben Martins, Bryan Parno

  Finding Invariants of Distributed Systems: It’s a Small (Enough) World After All

  In Network and Distributed System Security Symposium (NSDI’21), USENIX Association, 2021.

  Ruben Martins, Michael McCall, Dionisio de Niz, Amit Vasudevan, Bjorn Andersson, Mark Klein, John P. Lehoczky, Hyoseung Kim

  Formal Verification of a Mixed-Trust Synchronization Protocol

  In International Conference on Real-Time Networks and Systems (RTNS’21), ACM, 2021.
• 2020

  Joshua Clune, Vijay Ramamurthy, Ruben Martins, Umut A. Acar

  Program equivalence for assisted grading of functional programs

  In Object-oriented Programming, Systems, Languages, and Applications (OOPSLA’20), ACM, 2020.

  Daniel Ramos, Jorge Pereira, Inês Lynce, Vasco Manquinho, Ruben Martins

  UNCHARTIT: An Interactive Framework for Program Recovery from Charts

  In Automated Software Engineering Conference (ASE’20), IEEE, 2020.

  Amit Vasudevan, Petros Maniatis, Ruben Martins

  überSpark: Practical, Provable, End-to-End Guarantees on Commodity Heterogenous Interconnected Computing Platforms

  In ACM SIGOPS Operating Systems Review (OSR’20), ACM, 2020.

  Pedro Orvalho, Miguel Terra-Neves, Miguel Ventura, Ruben Martins, Vasco Manquinho

  SQUARES: A SQL Synthesizer Using Query Reverse Engineering

  In International Conference on Very Large Data Bases (VLDB’20), ACM, 2020.

  Peter Oostema, Ruben Martins, Marijn J. H. Heule

  Coloring Unit-Distance Strips using SAT

  In International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR’20), EPiC Series in Computing, 2020.
• 2019

  Pedro Orvalho, Miguel Terra-Neves, Miguel Ventura, Ruben Martins, Vasco Manquinho

  Encodings for Enumeration-Based Program Synthesis

  In Principles and Practice of Constraint Programming (CP’19), 583-599, Springer, 2019.

  Yanju Chen, Ruben Martins, Yu Feng

  Maximal Multi-layer Specification Synthesis

  In Symposium on the Foundations of Software Engineering (FSE’19), ACM, 2019.

  Ruben Martins, Jia Chen, Yanju Chen, Yu Feng, Isil Dillig

  Trinity: An Extensible Synthesis Framework for Data Science

  In International Conference on Very Large Data Bases (VLDB’19), ACM, 2019.
• 2018

  Inês Lynce, Vasco Manquinho, Ruben Martins

  Parallel Maximum Satisfiability

  In Handbook of Parallel Constraint Reasoning, Springer, 2018.

  Saurabh Joshi, Prateek Kumar, Ruben Martins, Sukrut Rao

  Approximation Strategies for Incomplete MaxSAT

  In Principles and Practice of Constraint Programming (CP’18), 219-228, Springer, 2018.

  Edward Zulkoski, Ruben Martins, Christoph M. Wintersteiger, Robert Robere, Jia Hui Liang, Krzysztof Czarnecki, Vijay Ganesh

  Learning-Sensitive Backdoors with Restarts

  In Principles and Practice of Constraint Programming (CP’18), 453-469, Springer, 2018.

  Edward Zulkoski, Ruben Martins, Christoph M. Wintersteiger, Jia Hui Liang, Krzysztof Czarnecki, Vijay Ganesh

  The Effect of Structural Measures and Merges on SAT Solver Performance

  In Principles and Practice of Constraint Programming (CP’18), 436-452, Springer, 2018.

  Yu Feng, Ruben Martins, Osbert Bastani, Işil Dillig

  Program Synthesis using Conflict-Driven Learning

  In Conference on Programming Language Design and Implementation (PLDI’18), 420-435, ACM, 2018. Distinguished Paper Award.
• 2017

  Yu Feng, Ruben Martins, Jacob Van Geffen, Işil Dillig, Swarat Chaudhuri

  Component-based synthesis of table consolidation and transformation tasks from examples

  In Conference on Programming Language Design and Implementation (PLDI’17), 422-436, ACM, 2017.

  Yu Feng, Ruben Martins, Yuepeng Wang, Işil Dillig, Thomas W. Reps

  Component-based synthesis for complex APIs

  In Symposium on Principles of Programming Languages (POPL’17), 599-612, ACM, 2017.

  Yu Feng, Osbert Bastani, Ruben Martins, Işil Dillig, Saswat Anand

  Automated Synthesis of Semantic Malware Signatures using Maximum Satisfiability

  In Network and Distributed System Security Symposium (NDSS’17), Internet Society, 2017.
• 2016

  Yuepeng Wang, Yu Feng, Ruben Martins, Arati Kaushik, Işil Dillig, Steven P. Reiss

  Hunter: next-generation code reuse for Java

  In International Symposium on Foundations of Software Engineering (FSE’16), 1028-1032, ACM, 2016.

  Martin Brain, Liana Hadarean, Daniel Kroening, Ruben Martins

  Automatic Generation of Propagation Complete SAT Encodings

  In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’16), 536-556, Springer, 2016.
• 2015

  Miguel Neves, Ruben Martins, Mikoláš Janota, Inês Lynce, Vasco Manquinho

  Exploiting Resolution-based Representations for MaxSAT Solving

  In International Conference on Theory and Applications of Satisfiability Testing (SAT’15), Springer, 2015.

  Saurabh Joshi, Ruben Martins, Vasco Manquinho

  Generalized Totalizer Encoding for Pseudo-Boolean Constraints

  In Principles and Practice of Constraint Programming (CP’15), Springer, 2015.

  Samuel Bucheli, Daniel Kroening, Ruben Martins, Ashutosh Natraj

  From AgentSpeak to C for Unmanned Aerial Vehicles

  In Towards Autonomous Robotic Systems (TAROS’15), Springer, 2015.

  Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, Tom Bienmüller

  Successful Use of Incremental BMC in Automotive Industry

  In Formal Methods for Industrial Critical Systems (FMICS’15), Springer, 2015.
• 2014

  Ruben Martins, Saurabh Joshi, Vasco Manquinho, Inês Lynce

  Incremental Cardinality Constraints for MaxSAT

  In Principles and Practice of Constraint Programming (CP’14), Springer, 2014. Most influential paper at CP’14.

  Ruben Martins, Vasco Manquinho, Inês Lynce

  Open-WBO: A Modular MaxSAT Solver

  In International Conference on Theory and Applications of Satisfiability Testing (SAT’14), Springer, 2014.
• 2013

  Ruben Martins, Vasco Manquinho, Inês Lynce

  Community-based Partitioning for MaxSAT Solving

  In International Conference on Theory and Applications of Satisfiability Testing (SAT’13), Springer, 2013.
• 2012

  Ruben Martins, Ana Graça

  Boolean Satisfiability and Optimization: Games, Puzzles and Genetics (in Portuguese)

  In Números, Cirurgias e Nós de Gravata, 252-270, IST Press, 2012.

  Ruben Martins, Vasco Manquinho, Inês Lynce

  On Partitioning for Maximum Satisfiability

  In European Conference on Artificial Intelligence (ECAI’12), IOS Press, 2012.

  Ruben Martins, Vasco Manquinho, Inês Lynce

  Clause Sharing in Parallel MaxSAT

  In Learning and Intelligent Optimization (LION’12), Springer, 2012.
• 2011

  Ruben Martins, Vasco Manquinho, Inês Lynce

  Exploiting Cardinality Encodings in Parallel Maximum Satisfiability

  In International Conference on Tools with Artificial Intelligence (ICTAI’11), IEEE, 2011.
• 2010

  Vasco Manquinho, Ruben Martins, Inês Lynce

  Improving Unsatisfiability-based Algorithms for Boolean Optimization

  In International Conference on Theory and Applications of Satisfiability Testing (SAT’10), Springer, 2010.

  Ruben Martins, Vasco Manquinho, Inês Lynce

  Improving Search Space Splitting for Parallel SAT Solving

  In International Conference on Tools with Artificial Intelligence (ICTAI’10), IEEE, 2010.

Students

• Daniel Ramos (S3D, Dual Degree CMU-Portugal, co-advised with Claire Le Goues and Vasco Manquinho)
• Margarida Ferreira (CSD, Dual Degree CMU-Portugal, co-advised with Ines Lynce)
• Ricardo Brancas (CSD, Affiliated CMU-Portugal, co-advised with Vasco Manquinho)
• Aidan Yang (S3D, co-advised with Claire Le Goues)
• Sophia Kolak (S3D, co-advised with Claire Le Goues)

I am always happy to do research with undergraduate students at CMU for either senior thesis, SCS Independent Studies, 07-400, during the Summer or the REUSE program. I am also happy to work with Master's students for Independent Studies in the Computer Sciences (15-689) or for Master research theses (15-698).

Previous students that I mentored at CMU:

• Joao Sa (CMU-Portugal Visiting MSc Student, Fall 2023)
• Aditi Pande (07-400, Spring 2023)
• Stephanie Eristoff (07-400, Spring 2023)
• Hailie Mitchell (REUSE, Summer 2022)
• Andreia Pereira (Visiting MSc Student, Spring 2022)
• Pedro Nunes (Visiting MSc Student, Spring 2022)
• Joshua Clune (Research Project, 2019-2020)
• Harutyun Rehanyan (REUSE, Summer 2020)
• Aidan Yang (REUSE, Summer 2020)
• Audrey Seo (REUSE, Summer 2019)
• Daniel Gibert Llaurado (Visiting PhD Student, Fall 2019)
• Aaron Meyers (Internship, Summer 2019)
• Pedro Miguel Orvalho (Visiting MSc student, Spring 2019)
• Rodrigo Bernado (Visiting MSc Student, Spring 2019)
• Yinglan Chen (SCS Independent Studies, Spring 2019)
• Clara Sellke (SCS Independent Studies, Fall 2018)
• Naveen Pai (SCS Independent Studies, Fall 2018)
• David Chen (SCS Independent Studies, Fall 2018)
• Zachary Susag (REUSE, Summer 2018)
• Avital Rabinovitch (Internship, Summer 2018)
• Kaige Liu (SCS Independent Studies, Spring 2018)
• Anlun Xu (SCS Independent Studies, Spring 2018)
• Tianlei Pan (SCS Independent Studies, Spring 2018)
• Mayank Jai (SCS Independent Studies, Spring 2018)

Contact me if you are an undergraduate or master student that wants to work on constraint solving, program verification or program synthesis.

Teaching