Publications

@inproceedings{verus-sys,
  author = {Lattuada, Andrea and Hance, Travis and Bosamiya, Jay and Brun, Matthias and Cho, Chanhee and LeBlanc, Hayley and Srinivasan, Pranav and Achermann, Reto and Chajed, Tej and Hawblitzel, Chris and Howell, Jon and Lorch, Jay and Padon, Oded and Parno, Bryan},
  title = {{Verus}: A Practical Foundation for Systems Verification},
  booktitle = {Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)},
  year = {2024},
  month = nov,
  month_numeric = {11}
}

@inproceedings{shake,
  author = {Zhou, Yi and Bosamiya, Jay and Li, Jessica and Heule, Marijn and Parno, Bryan},
  title = {Context Pruning for More Robust {SMT}-based Program Verification},
  booktitle = {Proceedings of the Formal Methods in Computer-Aided Design (FMCAD)},
  year = {2024},
  month = oct,
  month_numeric = {10}
}

@inproceedings{proof-plumber,
  author = {Cho, Chanhee and Zhou, Yi and Bosamiya, Jay and Parno, Bryan},
  title = {A Framework for Debugging Automated Program Verification Proofs via Proof Actions},
  booktitle = {Proceedings of the Conference on Computer Aided Verification (CAV)},
  year = {2024},
  month = jul,
  month_numeric = {7}
}

@phdthesis{bosamiya-thesis,
  author = {Bosamiya, Jay},
  title = {A Principled Approach Towards Unapologetic Security},
  school = {Carnegie Mellon University},
  year = {2024},
  month = may,
  month_numeric = {5}
}

@inproceedings{mariposa,
  author = {Zhou, Yi and Bosamiya, Jay and Takashima, Yoshiki and Li, Jessica and Heule, Marijn and Parno, Bryan},
  title = {Mariposa: Measuring {SMT} Instability in Automated Program Verification},
  booktitle = {Proceedings of the Formal Methods in Computer-Aided Design (FMCAD)},
  year = {2023},
  month = oct,
  month_numeric = {10}
}

@inproceedings{mswasm,
  author = {Michael, Alexandra E. and Gollamudi, Anitha and Bosamiya, Jay and Johnson, Evan and Denlinger, Aidan and Disselkoen, Craig and Watt, Conrad and Parno, Bryan and Patrignani, Marco and Vassena, Marco and Stefan, Deian},
  title = {{MSWasm}: Soundly Enforcing Memory-Safe Execution of Unsafe Code},
  booktitle = {Proceedings of the ACM Symposium on Principles of Programming Languages (POPL)},
  year = {2023},
  month = jan,
  month_numeric = {1}
}

@inproceedings{provably-safe-sandboxing-wasm,
  author = {Bosamiya, Jay and Lim, Wen Shih and Parno, Bryan},
  title = {Provably-Safe Multilingual Software Sandboxing using {WebAssembly}},
  booktitle = {Proceedings of the USENIX Security Symposium},
  year = {2022},
  month = aug,
  month_numeric = {8}
}

@inproceedings{everquic,
  author = {Delignat-Lavaud, Antoine and Fournet, Cedric and Parno, Bryan and Protzenko, Jonathan and Ramananandro, Tahina and Bosamiya, Jay and Lallemand, Joseph and Rakotonirina, Itsaka and Zhou, Yi},
  title = {A Security Model and Fully Verified Implementation for the {IETF} {QUIC} Record Layer},
  booktitle = {Proceedings of the IEEE Symposium on Security and Privacy},
  year = {2021},
  month = may,
  month_numeric = {5}
}

@inproceedings{caps,
  author = {Matsumoto, Stephanos and Bosamiya, Jay and Dai, Yucheng and van Oorschot, Paul and Parno, Bryan},
  title = {{CAPS}: Smoothly Transitioning to a More Resilient Web {PKI}},
  booktitle = {Proceedings of the ACSA Annual Computer Security Applications Conference (ACSAC)},
  year = {2020},
  month = dec,
  month_numeric = {12}
}

@inproceedings{transformers,
  author = {Bosamiya, Jay and Gibson, Sydney and Li, Yao and Parno, Bryan and Hawblitzel, Chris},
  title = {Verified Transformations and {Hoare} Logic: Beautiful Proofs for Ugly Assembly Language},
  booktitle = {Proceedings of the Conference on Verified Software: Theories, Tools, and Experiments (VSTTE)},
  year = {2020},
  month = jul,
  month_numeric = {7}
}