program equivalence

Proving Functional Program Equivalence via Directed Lemma Synthesis

Proving equivalence between functional programs is a fundamental problem in program verification, which often amounts to reasoning …

Yican Sun, Ruyi Ji, Jian Fang, Xuanlin Jiang, Mingshuai Chen, Yingfei Xiong

Does a Program Yield the Right Distribution?

We study discrete probabilistic programs with potentially unbounded looping behaviors over an infinite state space. We present, to the …

Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler