Small Scale Reflection for the Working Lean User. - Vladimir Gladshtein; George Pîrlea; Ilya Sergey (CoRR, 2024)

Mechanised Hypersafety Proofs about Structured Data: Extended Version. - Vladimir Gladshtein; Qiyuan Zhao; Willow Ahrens; Saman P. Amarasinghe; Ilya Sergey (CoRR, 2024)

Mechanised Hypersafety Proofs about Structured Data. - Vladimir Gladshtein; Qiyuan Zhao; Willow Ahrens; Saman P. Amarasinghe; Ilya Sergey (Proc. ACM Program. Lang., 2024)

LGTM: the Logic for Graceful Tensor Manipulation. - Vladimir Gladshtein; Qiyuan Zhao; Willow Ahrens; Saman P. Amarasinghe; Ilya Sergey (Zenodo, 2024)

LGTM: the Logic for Graceful Tensor Manipulation. - Vladimir Gladshtein; Qiyuan Zhao; Willow Ahrens; Saman P. Amarasinghe; Ilya Sergey (Zenodo, 2024)

Veil: A Framework for Automated and Interactive Verification of Transition Systems. - George Pîrlea; Vladimir Gladshtein; Elad Kinsbruner; Qiyuan Zhao; Ilya Sergey (CAV (3), 2025)