Insights Into Critical Program Verification

关键系统的验证是一项必不可少的任务，绝不能被忽视。学术界和工业界已经开发出各种方法来验证不同的系统和系统的各个方面，并且正在不断改进，然而，在大多数情况下，必须进行的一些操作需要进行非常资源密集的计算。技术的进步使得这些资源要付出高昂的代价。斯旺西大学计算机科学系已经对铁路领域的验证进行了广泛的研究[]，并开发了先进的工具包，可以无缝地将图形化的铁路规划模型和工程师设计的相应轨道细节转换为复杂的数学语言，然后可以传递给其他工具来对检查标准进行证明，要么证明评估标准得到满足，要么显示它们是如何被违反的。通过证明对上述数学模型的检查，目前是通过将它们转换为一个大的一阶逻辑表达式，并将其传递给SAT求解器来完成的，SAT求解器是一种旨在为表达式中每个未赋值的变量找到一个值的工具，这样(1)没有变量未赋值，(2)表达式成立。这一步是最耗时的，而且由于时间是宝贵的，特别是在工业中，我们认为探索新的技术和方法来最大限度地减少所需的解决时间是很重要的。多年来，人们一直在努力设计并行SAT求解器[][]，它利用计算系统中的多个核心来尝试解决给定的问题，与使用单核解决问题相比，在更短的时间内解决问题。最近，图形处理器在图形领域之外的计算能力变得越来越强，通过利用这种专业硬件的特性，可以更快地执行一般计算。这种硬件提供了极高的并行性，允许同时运行相同指令集的数千个实例。已经进行了研究，并且已经开发了一些技术来将SAT求解与这些特殊设备联系起来[][][]，然而，近年来，随着通用图形处理单元（gpgpu）硬件开发的巨大进步，这项研究似乎有所下降。特别是，限制因素，如很少的板载内存，已经大大放松，商业硬件提供超过32GB的RAM，目前具有扩展功能。我们相信，以目前的技术水平，在设计、测试和开发新技术和工具方面还有很大的空间，可以充分有效地利用gpgpu来解决SAT问题。我们的目标是探索和开发适用于大规模并行环境的新的SAT求解技术，同时也生产一个完整的SAT求解器，能够为SAT问题的实例提供显着的加速。

Verification of critical systems is an essential task, and mustn't be neglected. Various ways of verifying different systems, and aspects of systems, have already been developed by the academic and industry communities and are constantly improved, however, in most cases, some of the operations that have to be undertaken requre very resource-intensive computations to be undertaken. Advancements in technology make available such resources for a heafty price. Verification in the railway domain has been studied extensively by the Department of Computer Science in Swansea University[] and advanced toolkits have been developed to seemlessly transform graphical railway plan models, and corresponding track details designed by engineers, to complex mathematical languages that can then be passed to other tools to carry out the proofs on the checked criteria, either prove that assessed criteria are met or show how they are violated. The checking of the aforementioned mathematical models through provers, is currently done by translating them to a large first-order logic expression, and passing it to a SAT solver, which is a tool aimed at finding a value for every unassigned variable in the expression, such that (1) no variable is left unassigned and (2) the expression holds.This step is the most time consuming, and since time is precious especially in industry, we feel it is important to explore new techniques and approaches to minimizng the solving time required. Over the years, efforts have been made to design parallel SAT solvers[][][], that utilize multiple cores in a computing system to try and solve the problem they are given, in a shorter time compared to solving using a single core. Recently, graphics processors have become much more capable for computations outside the graphics domain, allowing general computations to be performed faster by exploting features of this specialty hardware. This hardware offers extreme parallelism, allowing for thousainds of instances of the same sets of instructions to be ran concurrnetly.Research has been carried out, and some techniques have been developed to link SAT solving with these special devices[][][], however this research seems to have declined in recent years, as massive advancements in the hardware development of the general purpose graphical processing units (GPGPUs) have been made. In particular, limiting factors such as little onboard memory, have been relaxed greatly, with comercial hardware offering upwards of 32GB of RAM at the moment, with extension capabilities. We belive that with current technologies, there is room for the design, testing, and development of new techniques and tools to make full and efficient use of GPGPUs for SAT solving.We aim to explore and develop new SAT solving techniques applicable to massively parallelized enviroments, whilst also producing a complete SAT solver, capable of delivering significant speedups to instances of SAT problems.