Proof Checking for SMT-solving and its application in the Railway domain

可满足性模理论（SMT）求解器是用于验证计算机程序的最先进的工具，并作为质量保证过程的一部分应用于工业。他们使用一套理论和搜索算法来证明软件的正确性，以正式的方法解决问题。SMT解决的一个不足之处是SMT证明没有标准化的格式，因此没有标准的方法来检查它们的有效性。相反，SAT求解器（SMT求解器所基于的）更成熟，并且具有这样一种标准化的证明检查方法;因此可以设想一种类似的SMT求解策略。拟议的博士项目旨在与西门子公司一起建立这样一个检查器并进行工业案例研究。西门子有意将SMT解决方案应用于高度复杂的铁路控制系统的设计和验证。SMT解决方案和验证检查的结合将导致效率和鲁棒性的提高，并将产生高度可靠的验证解决方案，可以取代和改进更传统的验证和测试形式。因此，利用经过验证的SMT求解将减少系统开发时间，从而节省资源，同时提高完整性。

Satisfiability-modulo-theory (SMT) solvers are state-of-the-art tools for verifying computer programs and are applied in Industry as part of quality assurance processes. They do this in a formal approach for solving problems using a set of theories and a search algorithm to prove the correctness of software. One deficiency of SMT-solving is that there is no standardised format for SMT-proofs and therefore no standard approach to checking their validity. Conversely, SAT-solvers (which SMT-solvers are based on) are more mature and have such a standardised proof checking approach; therefore one can envisage a similar strategy for SMT-solving. The proposed PhD-project aims to build such a checker and conduct industrial case-studies, together with Siemens. Siemens is interested in applying SMT-solving to the design and verification of highly complex Railway control systems.The combination of SMT-solving and proof checking will lead to improvements of both, efficiency and robustness, and will produce a highly reliable verification solution that can replace and improve more traditional forms of verification and testing. Thus, utilizing proof-checked SMT-solving will reduce system development time and thus save resources and at the same time increase integrity.