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.
10 Publications
2024 | Published | Journal Article | IST-REx-ID: 17495 | 
RefinedRust: A type system for high-assurance verification of rust programs
L. Gäher, M.J. Sammler, R. Jung, R. Krebbers, D. Dreyer, Proceedings of the ACM on Programming Languages 8 (2024) 1115–1139.
[Published Version]
View
| DOI
| Download Published Version (ext.)
L. Gäher, M.J. Sammler, R. Jung, R. Krebbers, D. Dreyer, Proceedings of the ACM on Programming Languages 8 (2024) 1115–1139.
2024 | Published | Journal Article | IST-REx-ID: 17497 |
Quiver: Guided abductive inference of separation logic specifications in coq
S. Spies, L. Gäher, M.J. Sammler, D. Dreyer, Proceedings of the ACM on Programming Languages 8 (2024) 889–913.
[Published Version]
View
| DOI
| Download Published Version (ext.)
S. Spies, L. Gäher, M.J. Sammler, D. Dreyer, Proceedings of the ACM on Programming Languages 8 (2024) 889–913.
2023 | Published | Journal Article | IST-REx-ID: 17498 |
Melocoton: A program logic for verified interoperability between OCaml and C
A. Guéneau, J. Hostert, S. Spies, M.J. Sammler, L. Birkedal, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 716–744.
[Published Version]
View
| DOI
| Download Published Version (ext.)
A. Guéneau, J. Hostert, S. Spies, M.J. Sammler, L. Birkedal, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 716–744.
2023 | Published | Journal Article | IST-REx-ID: 17499 |
Conditional contextual refinement
Y. Song, M. Cho, D. Lee, C.-K. Hur, M.J. Sammler, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 1121–1151.
[Published Version]
View
| DOI
| Download Published Version (ext.)
Y. Song, M. Cho, D. Lee, C.-K. Hur, M.J. Sammler, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 1121–1151.
2023 | Published | Journal Article | IST-REx-ID: 17500 |
DimSum: A decentralized approach to multi-language semantics and verification
M.J. Sammler, S. Spies, Y. Song, E. D’Osualdo, R. Krebbers, D. Garg, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 775–805.
[Published Version]
View
| DOI
| Download Published Version (ext.)
M.J. Sammler, S. Spies, Y. Song, E. D’Osualdo, R. Krebbers, D. Garg, D. Dreyer, Proceedings of the ACM on Programming Languages 7 (2023) 775–805.
2022 | Published | Journal Article | IST-REx-ID: 17501 |
BFF: Foundational and automated verification of bitfield-manipulating programs
F. Zhu, M.J. Sammler, R. Lepigre, D. Dreyer, D. Garg, Proceedings of the ACM on Programming Languages 6 (2022) 1613–1638.
[Published Version]
View
| DOI
| Download Published Version (ext.)
F. Zhu, M.J. Sammler, R. Lepigre, D. Dreyer, D. Garg, Proceedings of the ACM on Programming Languages 6 (2022) 1613–1638.
2022 | Published | Journal Article | IST-REx-ID: 17503 |
VIP: Verifying real-world C idioms with integer-pointer casts
R. Lepigre, M.J. Sammler, K. Memarian, R. Krebbers, D. Dreyer, P. Sewell, Proceedings of the ACM on Programming Languages 6 (2022) 1–32.
[Published Version]
View
| DOI
| Download Published Version (ext.)
R. Lepigre, M.J. Sammler, K. Memarian, R. Krebbers, D. Dreyer, P. Sewell, Proceedings of the ACM on Programming Languages 6 (2022) 1–32.
2022 | Published | Journal Article | IST-REx-ID: 17504 |
Simuliris: A separation logic framework for verifying concurrent program optimizations
L. Gäher, M.J. Sammler, S. Spies, R. Jung, H.-H. Dang, R. Krebbers, J. Kang, D. Dreyer, Proceedings of the ACM on Programming Languages 6 (2022) 1–31.
[Published Version]
View
| DOI
| Download Published Version (ext.)
L. Gäher, M.J. Sammler, S. Spies, R. Jung, H.-H. Dang, R. Krebbers, J. Kang, D. Dreyer, Proceedings of the ACM on Programming Languages 6 (2022) 1–31.
2019 | Published | Journal Article | IST-REx-ID: 17506 |
The high-level benefits of low-level sandboxing
M.J. Sammler, D. Garg, D. Dreyer, T. Litak, Proceedings of the ACM on Programming Languages 4 (2019) 1–32.
[Published Version]
View
| DOI
| Download Published Version (ext.)
M.J. Sammler, D. Garg, D. Dreyer, T. Litak, Proceedings of the ACM on Programming Languages 4 (2019) 1–32.
2019 | Published | Journal Article | IST-REx-ID: 6380 |
Efficient parameterized algorithms for data packing
K. Chatterjee, A.K. Goharshady, N. Okati, A. Pavlogiannis, Proceedings of the ACM on Programming Languages 3 (2019).
[Published Version]
View
| Files available
| DOI
K. Chatterjee, A.K. Goharshady, N. Okati, A. Pavlogiannis, Proceedings of the ACM on Programming Languages 3 (2019).