@misc{ho2024charon,
      title={Charon: An Analysis Framework for Rust}, 
      author={Son Ho and Guillaume Boisseau and Lucas Franceschino and Yoann Prak and Aymeric Fromherz and Jonathan Protzenko},
      year={2024},
      eprint={2410.18042},
      archivePrefix={arXiv},
      primaryClass={cs.PL},
      url={https://arxiv.org/abs/2410.18042}, 
}

@article{ho2024rust,
  author = {Ho, Son and Fromherz, Aymeric and Protzenko, Jonathan},
  title = {Sound Borrow-Checking for Rust via Symbolic Semantics},
  year = {2024},
  issue_date = {August 2024},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {8},
  number = {ICFP},
  url = {https://doi.org/10.1145/3674640},
  doi = {10.1145/3674640},
  journal = {Proc. ACM Program. Lang.},
  month = {aug},
  articleno = {251},
  numpages = {29},
  keywords = {Rust, Semantics, Verification}
}

@article{ho2022aeneas,
  author = {Ho, Son and Protzenko, Jonathan},
  title = {Aeneas: Rust verification by functional translation},
  year = {2022},
  issue_date = {August 2022},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {6},
  number = {ICFP},
  url = {https://doi.org/10.1145/3547647},
  doi = {10.1145/3547647},
  journal = {Proc. ACM Program. Lang.},
  month = {aug},
  articleno = {116},
  numpages = {31},
  keywords = {verification, functional translation, Rust}
}