The Application of SMT Solvers in the Mission Critical Software Verification
Andrey Tyugashev, Dmitrii Zheleznov
Journal of E - Technology, Vol. 12, No. 3, 2021.
DOI: https://doi.org/10.6025/jet/2021/12/3/86-92
Link: https://www.dline.info/jet/fulltext/v12n3/jetv12n3_3.pdf
Abstract:
We have discussed the application of SMT solvers in the Mission Critical Software verification. We have developed the Rules of verification based on Real-Time Control Algorithmâ€™s Logic. Required specification can be feasible or non-feasible on defined basis of functional control processes. In this model, the feasibility of the specification is being checked by SMT solver Z3. We have used a particular Java application through API for the SMT solver.