Please note that ISTA Research Explorer no longer supports Internet Explorer versions 8 or 9 (or earlier).
We recommend upgrading to the latest Internet Explorer, Google Chrome, or Firefox.
11 Publications
2025 | Published | Journal Article | IST-REx-ID: 19936 |

Bedarkar, Kimaya, et al. “RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers.” Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI, Association for Computing Machinery, 2025, pp. 73–97, doi:10.1145/3729249.
[Published Version]
View
| Files available
| DOI
2024 | Published | Journal Article | IST-REx-ID: 17495 |

Gäher, Lennard, et al. “RefinedRust: A Type System for High-Assurance Verification of Rust Programs.” Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, Association for Computing Machinery, 2024, pp. 1115–39, doi:10.1145/3656422.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2024 | Published | Journal Article | IST-REx-ID: 17497 |

Spies, Simon, et al. “Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq.” Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, Association for Computing Machinery, 2024, pp. 889–913, doi:10.1145/3656413.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2023 | Published | Journal Article | IST-REx-ID: 17498 |

Guéneau, Armaël, et al. “Melocoton: A Program Logic for Verified Interoperability between OCaml and C.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, Association for Computing Machinery, 2023, pp. 716–44, doi:10.1145/3622823.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2023 | Published | Journal Article | IST-REx-ID: 17499 |

Song, Youngju, et al. “Conditional Contextual Refinement.” Proceedings of the ACM on Programming Languages, vol. 7, no. POPL, Association for Computing Machinery, 2023, pp. 1121–51, doi:10.1145/3571232.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2023 | Published | Journal Article | IST-REx-ID: 17500 |

Sammler, Michael Joachim, et al. “DimSum: A Decentralized Approach to Multi-Language Semantics and Verification.” Proceedings of the ACM on Programming Languages, vol. 7, no. POPL, Association for Computing Machinery, 2023, pp. 775–805, doi:10.1145/3571220.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2022 | Published | Journal Article | IST-REx-ID: 17501 |

Zhu, Fengmin, et al. “BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs.” Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2, Association for Computing Machinery, 2022, pp. 1613–38, doi:10.1145/3563345.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2022 | Published | Journal Article | IST-REx-ID: 17503 |

Lepigre, Rodolphe, et al. “VIP: Verifying Real-World C Idioms with Integer-Pointer Casts.” Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, Association for Computing Machinery, 2022, pp. 1–32, doi:10.1145/3498681.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2022 | Published | Journal Article | IST-REx-ID: 17504 |

Gäher, Lennard, et al. “Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations.” Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, Association for Computing Machinery, 2022, pp. 1–31, doi:10.1145/3498689.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2019 | Published | Journal Article | IST-REx-ID: 17506 |

Sammler, Michael Joachim, et al. “The High-Level Benefits of Low-Level Sandboxing.” Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, Association for Computing Machinery, 2019, pp. 1–32, doi:10.1145/3371100.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2019 | Published | Journal Article | IST-REx-ID: 6380 |

Chatterjee, Krishnendu, et al. “Efficient Parameterized Algorithms for Data Packing.” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, 53, ACM, 2019, doi:10.1145/3290366.
[Published Version]
View
| Files available
| DOI