EngineeringComputer Science
Daniel Kroening
2021.2.2Frontiers in Artificial Intelligence and Applications
tlooto Summary
Researchers apply propositional satisfiability to discover programming flaws in low-level programs, such as embedded software.
Abstract
This chapter covers an application of propositional satisfiability to program analysis. We focus on the discovery of programming flaws in low-level programs, such as embedded software. The loops in the program are unwound together with a property to form a formula, which is then converted into CNF. The method supports low-level programming constructs such as bit-wise operators or pointer arithmetic.
Citation format
KROENING, Daniel. Chapter 20. software verification. Frontiers in Artificial Intelligence and Applications, 2021.