Son Ho

16 papers A* 1A 1Journal 11Unranked 2
YearRankTypeTitle / Venue / Authors
2025 — conf
Charon: An Analysis Framework for Rust.
CAV (4)
Son Ho, Guillaume Boisseau, Lucas Franceschino, Yoann Prak, Aymeric Fromherz, Jonathan Protzenko
2024 J jnl
Charon: An Analysis Framework for Rust.
CoRR
Son Ho, Guillaume Boisseau, Lucas Franceschino, Yoann Prak, Aymeric Fromherz, Jonathan Protzenko
2024 — —
Formal Verification of Rust Programs by Functional Translation. (Vérification formelle de programmes Rust par traduction fonctionnelle).
Son Ho
2024 J jnl
Incremental Proof Development in Dafny with Module-Based Induction.
CoRR
Son Ho, Clément Pit-Claudel
2024 J jnl
Sound Borrow-Checking for Rust via Symbolic Semantics.
CoRR
Son Ho, Aymeric Fromherz, Jonathan Protzenko
2024 J jnl
Sound Borrow-Checking for Rust via Symbolic Semantics.
Proc. ACM Program. Lang.
Son Ho, Aymeric Fromherz, Jonathan Protzenko
2023 J jnl
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification.
Proc. ACM Program. Lang.
Son Ho, Aymeric Fromherz, Jonathan Protzenko
2022 J jnl
Aeneas: Rust Verification by Functional Translation.
CoRR
Son Ho, Jonathan Protzenko
2022 J jnl
Aeneas: Rust verification by functional translation.
Proc. ACM Program. Lang.
Son Ho, Jonathan Protzenko
2022 J jnl
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Long Version).
IACR Cryptol. ePrint Arch.
Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan
2022 A* conf
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations.
SP
Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan
2021 J jnl
Zero-cost meta-programmed stateful functors in F.
CoRR
Jonathan Protzenko, Son Ho
2020 J jnl
Proof-Producing Synthesis of CakeML from Monadic HOL Functions.
J. Autom. Reason.
Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, Yong Kiam Tan
2018 — conf
Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications.
VSTTE
Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, Son Ho
2018 A conf
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.
IJCAR
Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish
2006 J jnl
On introducing approximate solution methods in theory of elasticity.
Comput. Appl. Eng. Educ.
Autar K. Kaw, Son Ho