Software Verification Lab

We make your programs run right

Picture by mollymccord (CC BY 2.0)

The Software Verification Laboratory at UMass Boston develops foundational research and tools that improve the correctness of programs.

We live in a world where parallel computers have become the norm. Programs must exploit parallel computing to harness performance benefits from current and future hardware. Our research improves the quality of parallel programs by introducing techniques that identify, reduce, or prevent programming errors.

Are you a student at UMass Boston? Ask us about our academic research opportunities, both at the undergraduate and at the graduate level. We strongly encourage underrepresented groups to apply. We have opportunities on software engineering, testing, compiler construction, program analysis, parallel programming.

Projects

Safer GPU programming

Localizing bugs caused by data-races & over-synchronization

Software:

Safer parallel runtimes

Proving the correctness of parallel runtimes and testing implementations

Software:

Publications

  • Provable GPU Data-Races in Static Race Detection. Dennis Liew, Tiago Cogumbreiro, and Julien Lange. In PLACES, EPTCS, 2022. [ presentation slides ]. [ bib | DOI | .pdf ]
  • Verification 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]. [ bib | DOI | .pdf ]
  • 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. In TOPLAS. ACM, 2018. Accepted. Preprint PDF.bib ]
  • 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. [ bib | DOI | .pdf ]
  • 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 | .pdf ]
  • 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 | http ]
  • 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 | .pdf ]
  • 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 | .pdf ]
  • 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 | .pdf ]
  • Types for X10 Clocks. Francisco Martins, Vasco T. Vasconcelos, and Tiago Cogumbreiro. In PLACES, volume 69 of EPTCS, page 111–129, 2010. [ bib | DOI | .pdf ]
  • 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 | .pdf ]
  • 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 | .pdf ]

People