Abstract
For many decades, the correctness of programs has been a concern for computer scientists and software engineers. At present, it is still not easy to ensure the correctness of nontrivial programs, although many researchers have made various attempts in this direction.
Recently, the Verifying Compiler is proposed as a grand challenge in computing research [7]. But its goal can be achieved incrementally. The following is quoted from Hoare (page 68 of [7]):
The progress of the project can be assessed by the number of lines of code that have been verified, and the level of annotation and verification that has been achieved. The relevant levels of annotations are: structural integrity, partial functional specification, total specification. The relevant levels of verification are: by testing, by human proof, by machine assistance, and fully automatic.
Supported in part by the National Natural Science Foundation of China (NSFC).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Boyer, R.S., Elspas, B., Levitt, K.N.: SELECT – A formal system for testing and debugging programs by symbolic execution. In: Proc. of the Int. conf. on Reliable Software, pp. 234–245 (1975)
Bush, W.R., Pincus, J.D., Sielaff, D.J.: A static analyzer for finding dynamic programming errors. Software – Practice And Experience 30, 775–802 (2000)
Cousot, P., et al.: The ASTRÉE analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. J. ACM 52(3), 365–473 (2005)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp. 234–245 (2002)
Hoare, C.A.R.: Assertions in modern software engineering practice, Keynote address. In: 26th Int’l Computer Software and Applications Conf (COMPSAC), Oxford, England (August 2002)
Hoare, T.: The verifying compiler: A grand challenge for computing research. J. of the ACM 50(1), 63–69 (2003)
King, J.C.: Symbolic execution and testing. Comm. of the ACM 19(7), 385–394 (1976)
Mackworth, A.K.: Constraint satisfaction. In: Shapiro, S.C. (ed.) Encyclopedia of Artificial Intelligence, vol. 1, pp. 205–211. John Wiley, New York (1990)
Zhang, J.: Symbolic execution of program paths involving pointer and structure variables. In: Proc. of the 4th Int’l Conf. on Quality Software (QSIC), pp. 87–92 (2004)
Zhang, J., Wang, X.: A constraint solver and its application to path feasibility analysis. of Software Engineering and Knowledge Engineering 11(2), 139–156 (2001)
Zhang, J., Xu, C., Wang, X.: Path-oriented test data generation using symbolic execution and constraint solving techniques. In: Proc. 2nd Int’l Conf. on Software Engineering and Formal Methods (SEFM), pp. 242–250 (2004)
Zitser, M., Lippmann, R., Leek, T.: Testing static analysis tools using exploitable buffer overflows from open source code. In: Proc. of the 12th ACM SIGSOFT Int’l Symp. on Foundations of Software Engineering, pp. 97–106 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Zhang, J. (2008). Constraint Solving and Symbolic Execution . In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_59
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_59
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)