Towards a Deductive Verification Infrastructure for Weighted Programming
This work presents a deductive verification framework based on a weighted assertion language and an intermediate verification language, whose weight domains are ordered structures with implication and coimplication, which let verification conditions express lower- and upper-bound obligations internally.