Publications

@inproceedings{turing:types22,
  author = {Tiago Cogumbreiro and Yannick Forster},
  title = {Towards a Mechanized Theory~of~Computation for~Education (Extended Abstract)},
  booktitle = {TYPES},
  year = {2022},
  url = {assets/turing-types22.pdf},
  note = {\href{assets/turing-types22-pres.pdf}{Slides for TYPES'22},
  \href{assets/turing-rhul22-pres.pdf}{slides for RHUL'22}}
}
@inproceedings{gidayu:iticse22,
  author = {Cogumbreiro, Tiago and Blike, Gregory},
  title = {Gidayu: visualizing automaton and their computations},
  booktitle = {ITiCSE},
  publisher = ,
  year = {2022},
  doi = {978-1-4503-9201-3/22/07},
  note = {\href{assets/gidayu-iticse22-pres.pdf}{[slides]}},
  url = {assets/gidayu-iticse22.pdf}
}
@inproceedings{provable-data-races:places22,
  author = {Liew, Dennis and Cogumbreiro, Tiago and Lange, Julien},
  title = {Provable {GPU} Data-Races in Static Race Detection},
  booktitle = {PLACES},
  year = {2022},
  series = {EPTCS},
  volume = {356},
  pages = {36-45},
  doi = {10.4204/EPTCS.356.4},
  url = {assets/faial-places22.pdf},
  note = {\href{assets/provable-dr-places22-slides.pdf}{[slides]}}
}
@misc{ver-gpu-progs:places22,
  author = {Hannah Zicarelli and Tiago Cogumbreiro},
  title = {Verification of {GPU} Programs: Evaluation Challenges (Extended Abstract)},
  note = {\href{assets/eval-challenges-places22-slides.pdf}{[slides]}},
  year = {2022},
  url = {assets/verify-gpu-places22.pdf}
}
@inproceedings{faial:cav21,
  author = {Cogumbreiro, Tiago and Lange, Julien and Liew, Dennis and Zicarelli, Hannah},
  title = {Checking Data-Race Freedom of {GPU} Kernels, Compositionally},
  booktitle = {CAV},
  year = {2021},
  pages = {403--426},
  volumne = {12759},
  doi = {10.1007/978-3-030-81685-8_19},
  publisher = {Springer},
  url = {assets/cogumbreiro-etal-faial.pdf},
  note = {\href{https://doi.org/10.5281/zenodo.4711923}{\textbf{Artifact awarded functional, available, reusable}; includes source code and Coq proofs}
   [\href{https://ucl-pplv.github.io/CAV21/poster_P_195/}{video} | \href{assets/faial-cav21-pres.pdf}{slides}]}
}
@inproceedings{transitive-joins:ppopp19,
  author = {Voss, Caleb and Cogumbreiro, Tiago and Sarkar, Vivek},
  title = {Transitive Joins: A Sound and Efficient Online Deadlock-avoidance Policy},
  booktitle = {PPoPP},
  year = {2019},
  isbn = {978-1-4503-6225-2},
  pages = {378--390},
  numpages = {13},
  doi = {10.1145/3293883.3295724},
  acmid = {3295724},
  publisher = {ACM},
  keywords = {deadlock avoidance, futures, task parallelism}
}
@article{armus:toplas19,
  author = {Tiago Cogumbreiro and
  Raymond Hu and
  Francisco Martins and
  Nobuko Yoshida},
  title = {Dynamic Deadlock Verification for General Barrier Synchronisation},
  journal = {TOPLAS},
  optissue_date = {March 2019},
  volume = {41},
  number = {1},
  optmonth = dec,
  year = {2018},
  issn = {0164-0925},
  pages = {1--38},
  articleno = {1},
  numpages = {38},
  doi = {10.1145/3229060},
  publisher = {ACM},
  optaddress = {New York, NY, USA},
  keywords = {Barrier synchronisation, Java, X10, deadlock avoidance, deadlock detection, phasers}
}
@article{gorn:oopsla17,
  author = {Tiago Cogumbreiro and
               Rishi Surendran and
               Francisco Martins and
               Vivek Sarkar and
               Vasco T. Vasconcelos and
               Max Grossman},
  title = {Deadlock Avoidance in Parallel Programs with Futures: Why parallel tasks should not wait for strangers},
  journal = {Proceedings of the ACM on Programming Languages},
  number = {OOPSLA},
  year = {2017},
  publisher = {ACM},
  volume = 1,
  articleno = 103,
  doi = {10.1145/3143359},
  url = {assets/cogumbreiro-gorn.pdf},
  note = {\href{https://gitlab.com/cogumbreiro/gorn/tree/oopsla17}{Source code and Coq proofs}}
}
@article{formalize-habanero-phasers:jlamp17,
  title = {Formalization of {Habanero} Phasers using {Coq}},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  year = {2017},
  issn = {2352-2208},
  volume = {90},
  pages = {50–60},
  publisher = {Elsevier},
  doi = {10.1016/j.jlamp.2017.02.006},
  author = {Tiago Cogumbreiro and Jun Shirako and Vivek Sarkar},
  note = {\href{https://cogumbreiro.github.io/jlamp17/}{Online interpreter and Coq proofs}},
  url = {assets/cogumbreiro-formalizing-phasers.pdf}
}
@inproceedings{dist-phasers:europar16,
  author = {Karthik Murthy and
               Sri Raj Paul and
               Kuldeep S. Meel and
               Tiago Cogumbreiro and
               John M. Mellor{-}Crummey},
  title = {Design and verification of distributed phasers},
  booktitle = {EuroPAR},
  year = {2016},
  pages = {405–418},
  publisher = {Springer},
  series = {LNCS},
  volume = {9833},
  doi = {10.1007/978-3-319-43659-3_30},
  url = {http://link.springer.com/chapter/10.1007%2F978-3-319-43659-3_30}
}
@inproceedings{phase-ordering:places16,
  author = {Tiago Cogumbreiro and
            Jun Shirako and
            Vivek Sarkar},
  title = {Formalization of phase ordering},
  booktitle = {PLACES},
  year = {2016},
  series = {EPTCS},
  volume = {211},
  pages = {13–24},
  doi = {10.4204/EPTCS.211.2},
  note = {\href{https://github.com/cogumbreiro/habanero-coq/tree/places16}{Coq proofs}},
  url = {assets/cogumbreiro-phase-ordering.pdf}
}
@inproceedings{armus:ppopp15,
  author = {Tiago Cogumbreiro and
            Raymond Hu and
            Francisco Martins and
            Nobuko Yoshida},
  title = {Dynamic deadlock verification for general barrier synchronisation},
  booktitle = {PPoPP},
  year = {2015},
  doi = {10.1145/2688500.2688519},
  publisher = {ACM},
  pages = {150–160},
  numpages = {11},
  note = {\href{https://bitbucket.org/cogumbreiro/armus/wiki/PPoPP15}{Source code}. \href{https://bitbucket.org/cogumbreiro/brenner-coq/commits/tag/v1.0}{Coq proofs}},
  url = {assets/cogumbreiro-armus.pdf}
}
@inproceedings{coordinating-phased-acts:coordination13,
  author = {Tiago Cogumbreiro and
               Francisco Martins and
               Vasco Thudichum Vasconcelos},
  title = {Coordinating phased activities while maintaining progress},
  booktitle = {COORDINATION},
  volume = {7890},
  year = {2013},
  pages = {31–44},
  doi = {10.1007/978-3-642-38493-6_3},
  publisher = {Springer},
  url = {assets/cogumbreiro.martins.vasconcelos_coordinating-phased-acts.pdf}
}
@inproceedings{types-x10-clocks:places10,
  author = {Francisco Martins and Vasco T. Vasconcelos and Tiago Cogumbreiro},
  title = {Types for {X10} {C}locks},
  booktitle = {PLACES},
  year = {2010},
  pages = {111–129},
  doi = {10.4204/EPTCS.69.8},
  volume = {69},
  series = {EPTCS},
  url = {assets/martins.vasconcelos.cogumbreiro_types-for-x10-clocks.pdf}
}
@inproceedings{type-inference-mil:places09,
  author = {Vasco T. Vasconcelos and Francisco Martins and Tiago Cogumbreiro},
  title = {Type inference for deadlock detection in a multithreaded typed assembly language},
  booktitle = {PLACES},
  optbooktitle = {PLACES'09},
  year = {2010},
  pages = {95–109},
  volume = 17,
  series = {EPTCS},
  url = {assets/vasconcelos.martins.cogumbreiro_type-inference-mil.pdf},
  doi = {10.4204/EPTCS.17.8}
}
@inproceedings{compiling-pi-into-mtal:places08,
  author = {Tiago Cogumbreiro and Francisco Martins and Vasco T. Vasconcelos},
  title = {Compiling the $pi$-calculus into a multithreaded typed assembly language},
  series = {ENTCS},
  volume = {241},
  pages = {57–84},
  year = {2009},
  booktitle = {PLACES},
  optbooktitle = {PLACES'08},
  issn = {1571-0661},
  doi = {10.1016/j.entcs.2009.06.004},
  url = {assets/cogumbreiro.martins.vasconcelos_compiling-pi-into-mtal.pdf}
}