Tractable memory safety verification via approximative symbolic execution 2025-04-18 compsci optimisation