Making Bug-Checking in Software and Hardware Design Cheaper and More Efficient

upstart writes:

Making bug-checking in software and hardware design cheaper and more efficient:

The development of complex hardware and software is error-prone and costly. Testing can detect the presence of bugs in these designs, but it cannot prove their absence. One technique that can provide worthful feedback on the correctness of system designs is model checking. Model checking is an automated reasoning technique to find flaws in hardware and software systems. Ph.D. candidate Muhammad Mahmoud has redesigned algorithms to make them more suitable for model checking using GPUs, which allow for parallel computing at low cost.

Model checking is used to catch potential bugs as early as possible-preferably at the design phase-to make the necessary modifications quickly and cost-effectively. Successful examples of model checking include verifying CERN controllers, railway interlockings, nuclear control systems, and medical imaging. Companies such as Amazon, Microsoft, and Facebook use and develop model checking technology to ensure their products behave functionally correct.

[...] In this thesis, Muhammad Mahmoud, of the research group Software Engineering and Technology at the department of Mathematics and Computer Science, investigated how Graphics Processing Units (GPUs) can be employed effectively for [bounded model checking (BMC)], focusing on the reasoning on SAT. GPUs offer great potential for parallel computation, while keeping power consumption low.

Read more of this story at SoylentNews.