https://www.sandia.gov/app/uploads/sites/222/2023/03/hulette_nsv15_digital.pdf Theorem-Proving Analysis of Digital Control Logic Interacting with Continuous Dynamics