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.

Research Project: Static Verification for Fearless GPU programming

Help achieve correct and efficient GPU programming, with a static framework that explains sources of performance degradation and repairs concurrency bugs without loss of performance.

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

  • Sound and partially-complete static analysis of data-races in GPU programs. Dennis Liew, Tiago Cogumbreiro, Julien Lange. PACMPL, 8(OOPSLA), 2024.
  • Hidden assumptions in static verification of data-race free GPU programs. Tiago Cogumbreiro, Julien Lange. In VIVEKFEST. 2024.
  • 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
  • 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
  • Checking Data-Race Freedom of GPU Kernels, Compositionally. Tiago Cogumbreiro, Julien Lange, Dennis Liew, 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

Peer-reviewed abstracts

  • RegularIMP: an imperative calculus to describe regular languages. Soroush Aghajani, Emma Kelminson, Tiago Cogumbreiro. In TFPIE. 2024.
    PDF
  • Towards Concurrency Repair in GPU Kernels with Resource Cost Analysis. Gregory Blike, Tiago Cogumbreiro. In SERPL. 2023.
    Slides PDF
  • Scaling data-race freedom analysis with array projections. Paul Maynard, Tiago Cogumbreiro. In SERPL. 2023.
    PDF
  • Verifying Static Analysis Tools. Udaya Sathiyamoorthy, Tiago Cogumbreiro. In TFP. 2023.
    Slides PDF
  • Towards a Mechanized Theory of Computation for Education. Tiago Cogumbreiro, Yannick Forster. In TYPES. 2022.
    Slides Slides (RHUL'22) PDF
  • Verification of GPU Programs: Evaluation Challenges. Hannah Zicarelli, Tiago Cogumbreiro. In PLACES. 2022.
    Slides PDF

People