Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
In one case, they bypassed the check by entering “;SHUTDOWN;” in HEX and turning it back into the standard coding just before the SQL command was sent to the database.
- 2.
Only a very few people write (can write) program specifications in formal language.
- 3.
For example, human testers may have to manually input data on Web browsers to test a website software system.
- 4.
- 5.
We use the term, “property” for a condition in symbolic execution.
- 6.
Conditions like \(c > 545\) for a real number, \(c\). The conditions cannot be checked completely with only specific numbers like \(c = 546, 545.1, 545.01, ...\).
- 7.
Conventional testing requires specific values for variables in order for the function executions to traverse rarely traversed paths, and finding such values is quite difficult. On the other hand, symbolic execution follows all the paths in the same manner.
References
H. Anai, K. Yokoyama, Algorithms of Quantifier Elimination and Their Applications: Optimization by Symbolic and Algebraic Methods (University of Tokyo Press, Tokyo, 2011) (In Japanese)
B.F. Caviness, J.R. Johnson (ed.), Quantifier elimination and cylindrical algebraic decomposition. Texts and Monographs in Symbolic Computation (Springer, New York, 1998)
M. Yoon, Y. Yun, H. Nakayama, Sequential Approximate Multiobjective Optimization Using Computational Intelligence (Springer, New York, 2009)
Matt Lake, Epic failures: 11 infamous software bugs. ComputerWorld, Sept 2010. http://www.computerworld.com/s/article/9183580
C. Cadar, P. Godefroid, S. Khurshid, K.C. Pasareanu, Sen, N. Tillmann, Symbolic execution for software testing in practice: preliminary assessment, in ICSE ’11 (2011)
V. D’Silva, D. Kroening, G. Weissenbacher, A survey of automated techniques for formal software verification, in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, TCAD (2008)
G. Li, I. Ghosh, S.P. Rajan, Klover: a symbolic execution and automatic test generation tool for c++ programs, in CAV 2011 (2011)
T. Matsuzaki, H. Iwane, H. Anai, N. Arai, The complexity of math problems—linguistic, or computational? in The 6th International Joint Conference on Natural Language Processing (IJCNLP13), pp. 73–81 (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer Japan
About this chapter
Cite this chapter
Masuoka, R., Anai, H. (2014). Mathematics and Manufacturing: The Symbolic Approach. In: Nishii, R., et al. A Mathematical Approach to Research Problems of Science and Technology. Mathematics for Industry, vol 5. Springer, Tokyo. https://doi.org/10.1007/978-4-431-55060-0_35
Download citation
DOI: https://doi.org/10.1007/978-4-431-55060-0_35
Published:
Publisher Name: Springer, Tokyo
Print ISBN: 978-4-431-55059-4
Online ISBN: 978-4-431-55060-0
eBook Packages: EngineeringEngineering (R0)