Adhikary, SunandanSunandanAdhikaryGurung, AmitAmitGurungThakkar, JayJayThakkarDa Costa, Antonio BrutoAntonio BrutoDa CostaDey, SoumyajitSoumyajitDeyHazra, AritraAritraHazraDasgupta, PallabPallabDasgupta2025-08-312025-08-312021-09-0110.1109/LES.2020.30355602-s2.0-85096090629http://repository.iitgn.ac.in/handle/IITG2025/23717A large fraction of bugs discovered in the design flow of embedded control software (ECS) arises from the control software s interaction with the plant it controls. Traditional formal analysis approaches using interleaved controller-plant reach-set analysis grossly overapproximate the reachable states and does not scale. In this letter, we examine a verification approach that considers a control system with the (possibly nonlinear) plant dynamics and mode switches specified along with the actual control software implementation. Given this input, we generate a bounded-Time safety verification problem encoded as satisfiability modulo theories (SMTs) constraints. We leverage δ-decidability over Reals to achieve scalability while verifying the control software.falseControl software verification | Sampled data systems. | δ-ApproximationArticle19430671139-141September 20211arJournal1