2026· International Conference on Interactive Theorem Proving· pp. 29:1-29:21· 0 citations· 50 references
Computer Science
TL;DR
This paper develops mechanized foundations for writing formal correctness proofs for both HeyVL encodings and PP verification techniques that are grounded in the basics of probability theory and formalizes Markov decision processes (MDPs).
Alerus is a framework for verifying probabilistic Rust programs based on Verus, a verification tool for Rust that supports SMT-based automation and separation-logic-inspired reasoning features and extends Verus with support for probabilistic reasoning while retaining these expressive features.
Alexander Y. Bai, Joseph Tassarotti· arXiv.org· 0 citations
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.
Emma Ahrens, Samuel Rode, Philipp Schröer et al.· 0 citations
A formalization of B3 ’s semantics, a VC Generator for the language, and a soundness proof that these two correspond are presented, which is a methodology to split the IVL’s semantic encodings into two layers of abstraction to cover realistic aspects of the semantics, while keeping the proofs amenable to automation.
V. Gladshtein, K. Leino· International Conference on...· 0 citations
SymCert is presented, a framework implemented in Lean for building verified SMT-based analyses of Cedar policies that provide a verified symbolic compiler and authorizer for reducing policies to SMT formulas, a hierarchy enforcer for ensuring well-formedness of counterexamples, and a counterex-ample extractor for provi...
It is concluded that foundational mechanized proofs can now be bought at the price of tokens, and that this shift can reshape how verification frameworks are architected.
FLEX is presented, a foundational Constrained Horn Clause (CHC) solver implemented in LEAN, that reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code, via three contributions.
J. Khan, Petros Markopoulos, Nicolás Lehmann et al.· arXiv.org· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
