Students working in the Software Model Checking Laboratory with Dr. Eric Mercer understand that oftentimes, a software "glitch" is more than a mere inconvenience.  In the past few years, software glitches have resulted in everything from misfirings of missiles to malfunctions in electronic voting machines.  With software having an increasingly large effect in all aspects of our lives, absolute reliability and correctness in software is crucial, and the question of how software engineers go about ensuring this has long been an unsolved problem in computer science.  Software model checking, however, may be part of the solution.

Software model checking is a complex endeavor that searches through a program to ensure that it is free of critical errors by formally modeling the program and then exploring its behavior to find bugs.  It can be extremely time intensive and requires enormous amounts of computational power.  Research in the lab, such as that conducted by undergraduate student Jacob Toronto, includes finding ways to make the process less costly-in terms of both time and money. 

Toronto created and implemented additions to the standardized random search techniques in Estes, a software model checking tool that was developed at BYU.  His additions reduced the amount of effort, time, and money required to find errors in software programs. He also conducted experiments to discover which methods for finding errors were the most efficient in the C program.  His findings were used to design a new set of criteria for determining the quality of programs used to standardize software model checking algorithms.