The range of verification problems that can be solved with logic model checking tools has increased significantly in the last few decades. This increase in capability is based on algorithmic advances and new theoretical insights, but it has also benefitted from the steady increase in processing speeds and main memory...
In this paper we discuss the application of a range of techniques to the
verification of mission-critical flight software at NASA’s Jet Propulsion Laboratory.
For this type of application we want to achieve a higher level of confidence than can
be achieved through standard software testing. Unfortunately, given the current...