Publications
@inproceedings{faial-repair:serpl23,
author = {Gregory Blike and Tiago Cogumbreiro},
title = {Towards Concurrency Repair in {GPU} Kernels with Resource Cost Analysis (Extended Abstract)},
year = {2023},
booktitle = {SERPL},
url = {assets/faial-repair-serpl23.pdf}
}
@inproceedings{faial-proj:serpl23,
author = {Paul Maynard and Tiago Cogumbreiro},
title = {Scaling data-race freedom analysis with array projections (Extended Abstract)},
year = {2023},
booktitle = {SERPL},
url = {assets/faial-proj-serpl23.pdf}
}
@inproceedings{shelley:coordination23,
author = {Mão de Ferro, Carlos and Cogumbreiro, Tiago and Martins, Francisco},
title = {Shelley: a framework for model checking call ordering on hierarchical systems},
booktitle = {COORDINATION},
year = {2023},
publisher = {Springer},
doi = {10.1007/978-3-031-35361-1_5}
}
@inproceedings{shelley-infer:verdi23,
author = {Mão de Ferro, Carlos and Cogumbreiro, Tiago and Martins, Francisco},
title = {Formalizing Model Inference of {MicroPython}},
booktitle = {VERDI},
year = {2023},
publisher = {IEEE},
doi = {10.1109/DSN-W58399.2023.00069},
url = {assets/shellypy-verdi23.pdf},
note = {
\href{https://zenodo.org/records/7892202}{Proof scripts}
}
}
@article{faial-drf:fmsd23,
author = {Cogumbreiro, Tiago and Lange, Julien and Liew Zhen Rong, Dennis and Zicarelli, Hannah},
title = {Memory Access Protocols: Certified Data-Race Freedom for GPU Kernels},
journal = {FMSD},
year = {2023},
doi = {10.1007/s10703-023-00415-0},
url = {assets/faial-fmsd23.pdf},
note = {1 of 7 invited publications from CAV21.
\href{assets/bu-sept-23.pdf}{slides for BU'23} }
}
@inproceedings{data-race-det:ecoop23,
author = {Feiyang Jin and Lechen Yu and Tiago Cogumbreiro and Vivek Sarkar and Jun Shirako },
title = {Dynamic Determinacy Race Detection for Task-Parallel Programs with Promises},
booktitle = {ECOOP},
publisher = {Schloss Dagstuhl},
optpublisher = ,
series = {LIPIcs},
year = {2023},
volume = {263},
doi = {10.4230/LIPIcs.ECOOP.2023.13}
}
@inproceedings{verifying-faial:tfp22,
author = {Udaya Sathiyamoorthy and Tiago Cogumbreiro},
title = {Verifying Static Analysis Tools (Extended Abstract)},
booktitle = {TFP},
year = {2023},
url = {assets/verifying-verifiers-tfp23.pdf},
note = {\href{verifying-verifiers-slides-tfp23.pdf}{Presentation slides}}
}
@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 = {Verification 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{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}
}