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}{Presentation slides},
  \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 = {10.1145/3502718.3524742},
  preprint = {assets/gidayu-iticse22.pdf},
  note = {\href{assets/gidayu-iticse22-slides.pdf}{Presentation slides}}
}
@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},
  note = {\href{assets/provable-races-places22-slides.pdf}{Presentation slides}},
  preprint = {assets/provable-races-places22.pdf}
}
@inproceedings{eval-challenges:places22,
  author = {Zicarelli, Hannah and Cogumbreiro, Tiago},
  title = {Verif‌ication of {GPU} Programs: Evaluation Challenges (Extended Abstract)},
  booktitle = {PLACES},
  year = {2022},
  note = {\href{assets/eval-challenges-places22-slides.pdf}{Presentation slides}},
  url = {assets/eval-challenges-places22.pdf}
}
@inproceedings{faial:cav21,
  author = {Cogumbreiro, Tiago and Lange, Julien and Liew Zhen Rong, 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},
  preprint = {assets/faial-cav21.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 presentation.}
    \href{assets/faial-brunel21-slides.pdf}{Presentation slides @ Brunel'21}
    \href{assets/faial-cav21-slides.pdf}{Presentation slides @ CAV'21}
}
}
@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},
  preprint = {assets/gorn-oopsla17.pdf},
  note = {
    \href{https://gitlab.com/cogumbreiro/gorn/tree/oopsla17}{Source code and proof scripts.}
    \href{assets/gorn-oopsla17-slides.pdf}{Presentation slides.}
    \href{https://www.youtube.com/watch?v=p1SLkd1oKYA}{Video presentation.}
    }
}
@article{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 proof scripts}},
  preprint = {assets/phasers-jlamp17.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}
}
@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}{Proof scripts}},
  preprint = {assets/phase-ordering-places16.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}{Proof scripts}},
  preprint = {assets/armus-ppopp15.pdf}
}
@inproceedings{armus:x1014,
  author = {Tiago Cogumbreiro and Raymond Hu and Francisco Martins and Nobuko Yoshida},
  title = {Armus: dynamic deadlock verification for barriers},
  year = {2014},
  booktitle = {X10},
  preprint = {http://x10.sourceforge.net/documentation/papers/X10Workshop2014/x1014-cogumbreiro.pdf}
}
@inproceedings{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},
  preprint = {assets/phased-acts-coordination13.pdf}
}
@inproceedings{types-for-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},
  preprint = {assets/types-for-clocks-places10.pdf}
}
@inproceedings{mil-infer: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},
  preprint = {assets/mil-infer-places09.pdf},
  doi = {10.4204/EPTCS.17.8}
}
@inproceedings{pi-to-mil: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},
  preprint = {assets/pi-to-mil-places08.pdf}
}