Heterogeneous Dynamic Logic: Provability Modulo Program Theories
We introduce Heterogeneous Dynamic Logic (HDL), a framework for combining reasoning principles from distinct (dynamic) program logics in a modular and compositional way. HDL mirrors the architecture of satisfiability modulo theories (SMT)
11. Jul 2025
An Incremental Abstraction Scheme for Solving Hard SMT-Instances over Bit-Vectors
We define four concrete approximation steps for the multiplication, division and remainder operators and combine them into an incremental abstraction scheme.
23. Aug 2020