Showing cs.PLShow all
2 papers · 1 filter
cs.PL2026
Weakly Non-Negative Supermartingales for Omega-Regular Verification
Toru Takisaka, Hongjie Qing, Libo Zhang
Martingale-based methods are central to probabilistic program verification, but strong global non-negativity requirements can exclude simple certificates from tractable template cl…
cs.PL2024
Lexicographic Ranking Supermartingales with Lazy Lower Bounds
Toru Takisaka, Libo Zhang, Changjiang Wang +1
Lexicographic Ranking SuperMartingale (LexRSM) is a probabilistic extension of Lexicographic Ranking Function (LexRF), which is a widely accepted technique for verifying program te…