Information Technology Reference
In-Depth Information
In either case the executable code has been derived from generic artefacts and,
therefore, verification is likely to benefit from the ability to partially evaluate
specific information. We are currently experimenting with an SWPL scenario
where we plan to use interleaved partial evaluation and symbolic execution.
References
1. King, J.C.: A program verifier. PhD thesis, Carnegie-Mellon University (1969)
2. Jones, N.D., Gomard, C.K., Sestoft, P.: Partial evaluation and automatic program
generation. Prentice-Hall, Englewood Cliffs (1993)
3. Beckert, B., Hahnle, R., Schmitt, P. (eds.): Verification of Object-Oriented Soft-
ware: The KeY Approach. LNCS, vol. 4334. Springer, Heidelberg (2006)
4. Beckert, B., Platzer, A.: Dynamic logic with non-rigid functions: A basis for object-
oriented program verification. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006.
LNCS (LNAI), vol. 4130, pp. 266-280. Springer, Heidelberg (2006)
5. Heisel, M., Reif, W., Stephan, W.: Program verification by symbolic execution and
induction. In: Knuth, E., Neuhold, E.J. (eds.) Operating Systems 1982. LNCS,
vol. 152, Springer, Heidelberg (1985)
6. Pasareanu, C.S., Visser, W.: Verification of Java programs using symbolic execu-
tion and invariant generation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS,
vol. 2989, pp. 164-181. Springer, Heidelberg (2004)
7. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an
overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.)
CASSIS 2004. LNCS, vol. 3362, pp. 49-69. Springer, Heidelberg (2005)
8. Baum, M.: Debugging by visualizing of symbolic execution. Master's thesis, Dept.of
Computer Science, Institute for Theoretical Computer Science (June 2007)
9. de Halleux, J., Tillmann, N.: Parameterized unit testing with Pex. In: Beckert, B.,
Hahnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 171-181. Springer, Heidelberg
(2008)
10. Engel, C., Hahnle, R.: Generating unit tests from formal proofs. In: Gurevich, Y.,
Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 169-188. Springer, Heidelberg
(2007)
11. Stenzel, K.: A formally verified calculus for full Java Card. In: Rattray, C., Maharaj,
S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 491-505. Springer,
Heidelberg (2004)
12. Deng, X., Lee, J.: Robby: Bogor/Kiasan: a k-bounded symbolic execution for check-
ing strong heap properties of open systems. In: Proc. 21st IEEE/ASM Intl. Con-
ference on Automated Software Engineering, Tokyo, Japan, pp. 157-166. IEEE
Computer Society, Los Alamitos (2006)
13. Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520,
Department of Computer Science, Katholieke Universiteit Leuven (August 2008)
14. Schultz, U.P., Lawall, J.L., Consel, C.: Automatic program specialization for java.
ACM Transactions on Programming Languages and Systems 25 (2003)
15. Bubel, R., Hahnle, R., Weiss, B.: Abstract interpretation of symbolic execution
with explicit state updates. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E.
(eds.) FMCO 2008. LNCS, vol. 5751, pp. 247-277. Springer, Heidelberg (2009)
