Tiago Cogumbreiro

Tiago is an assistant professor at UMass Boston. Tiago's research helps programmers write software with fewer bugs.

Tiago develops tools that localize errors, proves the correctness of algorithms, and mines how we write code to identify anomalies.

Image source: NASA/Johns Hopkins University Applied Physics Laboratory/Southwest Research Institute

  • Towards Concurrency Repair in GPU Kernels with Resource Cost Analysis (Extended Abstract). Gregory Blike and Tiago Cogumbreiro. In SERPL, 2023. [ bib | .pdf ]
  • Scaling data-race freedom analysis with array projections (Extended Abstract). Paul Maynard and Tiago Cogumbreiro. In SERPL, 2023. [ bib | .pdf ]
  • Shelley: a framework for model checking call ordering on hierarchical systems. Carlos Mão de Ferro, Tiago Cogumbreiro, and Francisco Martins. In COORDINATION. Springer, 2023. [ bib | DOI ]
  • Formalizing Model Inference of MicroPython. Carlos Mão de Ferro, Tiago Cogumbreiro, and Francisco Martins. In VERDI. IEEE, 2023. Proof scripts. [ bib | DOI | .pdf ]
  • Memory Access Protocols: Certified Data-Race Freedom for GPU Kernels. Tiago Cogumbreiro, Julien Lange, Dennis Liew Zhen Rong, and Hannah Zicarelli. FMSD, 2023. 1 of 7 invited publications from CAV21. slides for BU'23. [ bib | DOI | .pdf ]
  • Dynamic Determinacy Race Detection for Task-Parallel Programs with Promises. Feiyang Jin, Lechen Yu, Tiago Cogumbreiro, Vivek Sarkar, and Jun Shirako. In ECOOP, volume 263 of LIPIcs. Schloss Dagstuhl, 2023. [ bib | DOI ]
  • Verifying Static Analysis Tools (Extended Abstract). Udaya Sathiyamoorthy and Tiago Cogumbreiro. In TFP, 2023. Presentation slides. [ bib | .pdf ]
  • Towards a Mechanized Theory of Computation for Education (Extended Abstract). Tiago Cogumbreiro and Yannick Forster. In TYPES, 2022. Presentation slides, slides for RHUL'22. [ bib | .pdf ]
  • Gidayu: visualizing automaton and their computations. Tiago Cogumbreiro and Gregory Blike. In ITiCSE. ACM, 2022. Presentation slides. [ bib | DOI | preprint ]
  • Provable GPU Data-Races in Static Race Detection. Dennis Liew, Tiago Cogumbreiro, and Julien Lange. In PLACES, volume 356 of EPTCS, pages 36--45, 2022. Presentation slides. [ bib | DOI | preprint ]
  • Verif‌ication of GPU Programs: Evaluation Challenges (Extended Abstract). Hannah Zicarelli and Tiago Cogumbreiro. In PLACES, 2022. Presentation slides. [ bib | .pdf ]
  • Checking Data-Race Freedom of GPU Kernels, Compositionally. Tiago Cogumbreiro, Julien Lange, Dennis Liew Zhen Rong, and Hannah Zicarelli. In CAV, pages 403--426. Springer, 2021. Artifact awarded functional, available, reusable; includes source code and Coq proofs. Video presentation. Presentation slides @ Brunel'21 Presentation slides @ CAV'21. [ bib | DOI | preprint ]
  • Transitive Joins: A Sound and Efficient Online Deadlock-avoidance Policy. Caleb Voss, Tiago Cogumbreiro, and Vivek Sarkar. In PPoPP, pages 378--390. ACM, 2019. [ bib | DOI ]
  • Dynamic Deadlock Verification for General Barrier Synchronisation. Tiago Cogumbreiro, Raymond Hu, Francisco Martins, and Nobuko Yoshida. TOPLAS, 41(1):1--38, 2018. [ bib | DOI ]
  • Deadlock Avoidance in Parallel Programs with Futures: Why parallel tasks should not wait for strangers. Tiago Cogumbreiro, Rishi Surendran, Francisco Martins, Vivek Sarkar, Vasco T. Vasconcelos, and Max Grossman. Proceedings of the ACM on Programming Languages, 1(OOPSLA), 2017. Source code and proof scripts. Presentation slides. Video presentation. [ bib | DOI | preprint ]
  • Formalization of Habanero Phasers using Coq. Tiago Cogumbreiro, Jun Shirako, and Vivek Sarkar. Journal of Logical and Algebraic Methods in Programming, 90:50–60, 2017. Online interpreter and proof scripts. [ bib | DOI | preprint ]
  • Design and verification of distributed phasers. Karthik Murthy, Sri Raj Paul, Kuldeep S. Meel, Tiago Cogumbreiro, and John M. Mellor-Crummey. In EuroPAR, volume 9833 of LNCS, page 405–418. Springer, 2016. [ bib | DOI ]
  • Formalization of phase ordering. Tiago Cogumbreiro, Jun Shirako, and Vivek Sarkar. In PLACES, volume 211 of EPTCS, page 13–24, 2016. Proof scripts. [ bib | DOI | preprint ]
  • Dynamic deadlock verification for general barrier synchronisation. Tiago Cogumbreiro, Raymond Hu, Francisco Martins, and Nobuko Yoshida. In PPoPP, page 150–160. ACM, 2015. Source code. Proof scripts. [ bib | DOI | preprint ]
  • Armus: dynamic deadlock verification for barriers. Tiago Cogumbreiro, Raymond Hu, Francisco Martins, and Nobuko Yoshida. In X10, 2014. [ bib | preprint ]
  • Coordinating phased activities while maintaining progress. Tiago Cogumbreiro, Francisco Martins, and Vasco Thudichum Vasconcelos. In COORDINATION, volume 7890, page 31–44. Springer, 2013. [ bib | DOI | preprint ]
  • Types for X10 Clocks. Francisco Martins, Vasco T. Vasconcelos, and Tiago Cogumbreiro. In PLACES, volume 69 of EPTCS, page 111–129, 2010. [ bib | DOI | preprint ]
  • Type inference for deadlock detection in a multithreaded typed assembly language. Vasco T. Vasconcelos, Francisco Martins, and Tiago Cogumbreiro. In PLACES, volume 17 of EPTCS, page 95–109, 2010. [ bib | DOI | preprint ]
  • Compiling the pi-calculus into a multithreaded typed assembly language. Tiago Cogumbreiro, Francisco Martins, and Vasco T. Vasconcelos. In PLACES, volume 241 of ENTCS, page 57–84, 2009. [ bib | DOI | preprint ]

Teaching

CS720 Spring 2024: Logical Foundations
  • Office: (M03-0201-16) Room 0201-16, 3rd floor, McCormack
  • Office hours: 11:00am to 12:30pm Monday; 2:30pm to 4:00pm Tuesday (in-person)

Research

Experience

Education