Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
We present a principled approach for connecting neural network verifiers to interactive theorem provers and demonstrate its utility in Neural-Cyber-Physical-Systems verificaiton.
5. May 2026
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)
3. Apr 2026