Insights Into Critical Program Verification

深入了解关键程序验证

• 批准号: 2280387
• 金额: --
• 依托单位: Swansea University
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2019
• 资助国家: 英国
• 起止时间: 2019 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2280387
• 关键词: Insights; Into; Critical; Program; Verification

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.

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