Mathematics and Manufacturing: The Symbolic Approach

This chapter discusses applications of the symbolic approach to the manufacture of hardware and software. Two example applications, one hardware and the other software, are illustrated. The first example is the design of a hard disk drive (HDD) head by using quantifier elimination (QE), and the other is software validation using symbolic execution. Both examples demonstrate the strengths of the symbolic approach over conventional numerical approaches. While there are, of course, challenges facing the symbolic approach such as faithful modeling and the need for abstraction, it is an extremely powerful and game-changing technology.