-
Sound and partially-complete static analysis of data-races in GPU programs.
Dennis Liew, Tiago Cogumbreiro, Julien Lange.
PACMPL, 8(OOPSLA2), 2024.
Slides Artifact PDF DOI
- Hidden assumptions in static verification of data-race free GPU programs. Tiago Cogumbreiro, Julien Lange.
Slides PDF- RegularIMP: an imperative calculus to describe regular languages (Extended Abstract). Soroush Aghajani, Emma Kelminson, Tiago Cogumbreiro. In TFPIE, 2024
PDF- Towards Concurrency Repair in GPU Kernels with Resource Cost Analysis (Extended Abstract). Gregory Blike, Tiago Cogumbreiro. In SERPL, 2023
Slides PDF- Scaling data-race freedom analysis with array projections (Extended Abstract). Paul Maynard, Tiago Cogumbreiro. In SERPL, 2023
PDF- Shelley: a framework for model checking call ordering on hierarchical systems. Carlos Mão de Ferro, Tiago Cogumbreiro, Francisco Martins. In COORDINATION. Springer, 2023.
DOI- Formalizing Model Inference of MicroPython. Carlos Mão de Ferro, Tiago Cogumbreiro, Francisco Martins. In VERDI. IEEE, 2023.
Artifact PDF DOI- Memory Access Protocols: Certified Data-Race Freedom for GPU Kernels. Tiago Cogumbreiro, Julien Lange, Dennis Liew, Hannah Zicarelli. FMSD, 2023. invited paper (CAV'21 special issue)
Slides PDF DOI- Dynamic Determinacy Race Detection for Task-Parallel Programs with Promises. Feiyang Jin, Lechen Yu, Tiago Cogumbreiro, Vivek Sarkar, Jun Shirako. In ECOOP, volume 263 of LIPIcs. Schloss Dagstuhl, 2023.
DOI- Verifying Static Analysis Tools (Extended Abstract). Udaya Sathiyamoorthy, Tiago Cogumbreiro. In TFP, 2023
Slides PDF- Towards a Mechanized Theory of Computation for Education (Extended Abstract). Tiago Cogumbreiro, Yannick Forster. In TYPES, 2022
Slides Slides (RHUL'22) PDF- Gidayu: visualizing automata and their computations. Tiago Cogumbreiro, Gregory Blike. In ITiCSE. ACM, 2022.
Slides PDF DOI- Provable GPU Data-Races in Static Race Detection. Dennis Liew, Tiago Cogumbreiro, Julien Lange. In PLACES, volume 356 of EPTCS, page 36–45. 2022.
Slides PDF DOI- Verification of GPU Programs: Evaluation Challenges (Extended Abstract). Hannah Zicarelli, Tiago Cogumbreiro. In PLACES, 2022
Slides PDF- Checking Data-Race Freedom of GPU Kernels, Compositionally. Tiago Cogumbreiro, Julien Lange, Dennis Lew, Hannah Zicarelli. In CAV, volume 12759, page 403–426. Springer, 2021. 1 of 5 top papers invited for FMSD'23
Artifact Slides Video Slides (Brunel'21) PDF DOI- Transitive Joins: A Sound and Efficient Online Deadlock-avoidance Policy. Caleb Voss, Tiago Cogumbreiro, Vivek Sarkar. In PPoPP, page 378–390. ACM, 2019.
DOI- Dynamic Deadlock Verification for General Barrier Synchronisation. Tiago Cogumbreiro, Raymond Hu, Francisco Martins, Nobuko Yoshida. TOPLAS, 41(1):1–38, 2018.
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, Max Grossman. PACMPL, 1(OOPSLA), 2017.
Artifact Slides Video PDF DOI- Formalization of Habanero Phasers using Coq. Tiago Cogumbreiro, Jun Shirako, Vivek Sarkar. JLAMP, 90:50–60, 2017.
Artifact PDF DOI- Design and verification of distributed phasers. Karthik Murthy, Sri Raj Paul, Kuldeep S. Meel, Tiago Cogumbreiro, John M. Mellor-Crummey. In EuroPAR, volume 9833 of LNCS, page 405–418. Springer, 2016.
DOI- Formalization of phase ordering. Tiago Cogumbreiro, Jun Shirako, Vivek Sarkar. In PLACES, volume 211 of EPTCS, page 13–24. 2016.
Artifact PDF DOI- Dynamic deadlock verification for general barrier synchronisation. Tiago Cogumbreiro, Raymond Hu, Francisco Martins, Nobuko Yoshida. In PPoPP, page 150–160. ACM, 2015.
Artifact Proofs PDF DOI- Armus: dynamic deadlock verification for barriers. Tiago Cogumbreiro, Raymond Hu, Francisco Martins, Nobuko Yoshida. In X10. 2014.
PDF- Coordinating phased activities while maintaining progress. Tiago Cogumbreiro, Francisco Martins, Vasco T. Vasconcelos. In COORDINATION, volume 7890, page 31–44. Springer, 2013.
PDF DOI- Types for X10 Clocks. Francisco Martins, Vasco T. Vasconcelos, Tiago Cogumbreiro. In PLACES, volume 69 of EPTCS, page 111–129. 2010.
PDF DOI- Type inference for deadlock detection in a multithreaded typed assembly language. Vasco T. Vasconcelos, Francisco Martins, Tiago Cogumbreiro. In PLACES, volume 17 of EPTCS, page 95–109. 2009.
PDF DOI- Compiling the π-calculus into a multithreaded typed assembly language. Tiago Cogumbreiro, Francisco Martins, Vasco T. Vasconcelos. In PLACES, volume 241 of ENTCS, page 57–84. 2008.
PDF DOITeaching
- Office: (M03-0201-16) Room 0201-16, 3rd floor, McCormack
- Office hours: 4:00pm - 5:00pm Monday/Tuesday/Wednesday (in-person)
Research
- You can meet my collaborators at the Software Verification Lab
Experience
- (2018–ongoing) Assistant professor at UMass Boston
- (2017–2018) Postdoctoral researcher at Georgia Tech, advised by Vivek Sarkar
- (2015–2017) Postdoctoral researcher at Rice University, advised by Vivek Sarkar
- (2014) Research assistant at Imperial College London, advised by Nobuko Yoshida
- (2012) Visiting scholar at Rice University, advised by Vivek Sarkar
- (2008-2013) Research assistant at FCUL
- (2007) Research assistant at FCT/UNL
Education
- (2015) Ph.D. ULisboa, advised by Francisco Martins, [PDF]
- (2009) M.Sc. ULisboa, advised by Francisco Martins, [PDF]
- (2007) B.Sc. Universidade dos Açores, [PDF 1] [PDF 2]
- Hidden assumptions in static verification of data-race free GPU programs. Tiago Cogumbreiro, Julien Lange.