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.