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
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