2 papers
cs.SE2026
Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST
Prokhor Shlyakhtun, Alexander Gryzlov, Vladimir Kukharenko +5
We report on the verification of memory safety for decoder components of liblzma, the compression library underlying xz-utils: the LZMA2 state machine, the LZMA1 decoder it control…
cs.LO2025
Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
Marcos Grandury, Aleksandar Nanevski, Alexander Gryzlov
Verifying graph algorithms has long been considered challenging in separation logic, mainly due to structural sharing between graph subcomponents. We show that these challenges can…