3 papers
cs.SE2025
Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)
Reiner Hähnle, Cosimo Laneve, Adele Veschetti
Stipula is a domain-specific programming language designed to model legal contracts with enforceable properties, especially those involving asset transfers and obligations. This pa…
cs.LO2025
A Sequent Calculus For Trace Formula Implication
Niklas Heidler, Reiner Hähnle
Specification languages are essential in deductive program verification, but they are usually based on first-order logic, hence less expressive than the programs they specify. Rece…
cs.LO2024
An Expressive Trace Logic for Recursive Programs
Dilian Gurov, Reiner Hähnle
We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed-points, for precise specification of programs with recursive procedures.…