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 using programming synthesis to improve programmer’s productivity and to automate data science-related tasks. 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, CP, and has won a distinguished paper award at PLDI 2018 for his work on program synthesis. He has also developed several award-winning constraint solvers and is the main 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 optimizations problems including finding an optimal seating arrangement for his own wedding.
PhD in Information Systems and Computer Engineering, 2013
University of Lisbon
M.Sc. and B.Sc. in Mathematics and Applications, 2008
University of Lisbon
Paper accepted at HotNets'21: Counterfeiting Congestion Control Algorithms. Margarida Ferreira, Akshay Narayan, Inês Lynce, Ruben Martins, Justine Sherry.
Distinguished paper award at FSE'21: AlloyMax: Bringing Maximum Satisfaction to Relational Specifications. Changjian Zhang, Ryan Wagner, Pedro Orvalho, David Garlan, Vasco Manquinho, Ruben Martins, Eunsuk Kang. ISR press release.
Amazon Research Award on Improving performance and trust of MaxSAT solvers. CMU press release.
Paper accepted at PLDI'21: SyRust: Automatic Testing of Rust Libraries with Semantic-Aware Program Synthesis. Yoshiki Takashima, Ruben Martins, Limin Jia, Corina S Pasareanu. CyLab press release.
Paper accepted at ICSE'21: SOAR: A Synthesis Approach for Data Science API Refactoring. Ansong Ni, Daniel Ramos, Aidan Yang, Inês Lynce, Vasco Manquinho, Ruben Martins, Claire Le Goues.
New chapter on MaxSAT in the Handbook of Satisfiability, 2nd edition, Chapter 24: Maximum Satisfiability. Fahiem Bacchus, Matti Järvisalo, Ruben Martins.
PhD Students:
Alumni:
I am always happy to work with undergraduate students at CMU for either SCS Independent Studies or during the Summer or the REUSE program.
Previous students that I mentored at CMU:
Contact me if you are an undergraduate student that wants to work on program verification or program synthesis for either SCS Independent studies or a summer internship.
Spring 2021 - 15-414/614 Bug Catching: Automated Program Verification with Frank Pfenning. This course teaches students how to write bug-free code through the process of software verification, which aims to prove the correctness of a program with respect to a mathematical specification
Fall 2020 - 15-816 Advanced Topics in Logic: Automated Reasoning and Satisfiability with Marijn Heule. This course teaches students about automated reasoning techniques and their applications from the verification of hardware and software to solve open problems in mathematics.
Fall 2019 - 15-816 Advanced Topics in Logic: Automated Reasoning and Satisfiability with Marijn Heule. This course teaches students about automated reasoning techniques and their applications from the verification of hardware and software to solve open problems in mathematics.
Fall 2018 - 15-414/614 Bug Catching: Automated Program Verification with Matt Fredrikson. This course teaches students how to write bug-free code through the process of software verification, which aims to prove the correctness of a program with respect to a mathematical specification