Abstract
Strongly dynamic software systems are difficult to verify. By strongly dynamic, we mean that the actors in such systems change dynamically, that the resources used by such systems are dynamically allocated and deallocated, and that for both sets, no bounds are statically known. In this position paper, we describe the progress we have made in automated verification of strongly dynamic systems using abstract interpretation with three-valued logical structures. We then enumerate a number of challenges that must be tackled in order for such techniques to be widely adopted.
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
Arnold, G.: Combining heap analyses by intersecting abstractions. Master’s thesis, Tel Aviv University (October 2004)
Ashcraft, K., Engler, D.: Using programmer-written compiler extensions to catch security holes. In: Proc. IEEE Symp. on Security and Privacy, Oakland, CA (May 2002)
Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) ETAPS 1998 and FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proc. Computer Aided Verification, pp. 154–169 (2000)
Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., R.,, Laubach, S., Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: Proc. Intl. Conf. on Software Eng, June 2000, pp. 439–448 (2000)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. Symp. on Principles of Prog. Languages, pp. 269–282. ACM Press, New York (1979)
Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Proc. Conf. on Prog. Lang. Design and Impl, pp. 57–68 (June 2002)
DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: Proc. Conf. on Prog. Lang. Design and Impl. pp. 59–69 (June 2001)
Dor, N., Rodeh, M., Sagiv, M.: Checking cleanness in linked lists. In: Proc. Static Analysis Symp. Springer, Heidelberg (2000)
Field, J., Goyal, D., Ramalingam, G., Yahav, E.: Typestate verification: Abstraction techniques and complexity results. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 439–462. Springer, Heidelberg (2003)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: Proc. Conf. on Prog. Lang. Design and Impl. Berlin, pp. 234–245 (June 2002)
Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proc. Conf. on Prog. Lang. Design and Impl. Berlin, pp. 1–12 (June 2002)
Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Tools and Algs.for the Construct.and Anal.of Syst. pp. 512–529 (2004)
Gopan, D., Reps, T., Sagiv, M.: Numeric analysis of array operations. In: Proc. Symp. on Principles of Prog. Languages (2005)
Hoare, C.A.R.: Recursive data structures. Int. J. of Comp. and Inf. Sci. 4(2), 105–132 (1975)
Jeannet, B., Gopan, D., Reps, T.: A relational abstraction for functions. In: To appear in Proc. 12th Int. Static Analysis Symp. (September 2005) (to appear)
Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. In: Proc. Static Analysis Symp. Springer, Heidelberg (2004)
Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Proc. Static Analysis Symp. pp. 280–301 (2000)
Lev-Ami, T., Reps, T., Sagiv, M., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: Int.Symp.on Softw.Testing and Analysis, pp. 26–38 (2000)
Loginov, A., Reps, T., Sagiv, M.: Learning abstractions for verifying data-structure properties. In: Int.Conf.on Computer Aided Verif. (2005)
Manevich, R., Ramalingam, G., Field, J., Goyal, D., Sagiv, M.: Compactly representing first-order structures for static analysis. In: Proc. Static Analysis Symp. pp. 196–212 (2002)
Manevich, R., Sagiv, M., Ramalingam, G., Field, J.: Partially disjunctive heap abstraction. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 265–279. Springer, Heidelberg (2004)
Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, Springer, Heidelberg (2005)
Nielson, F., Nielson, H.R., Sagiv, M.: A Kleene Analysis of Mobile Ambients. In: Smolka, G. (ed.) ESOP 2000 and ETAPS 2000. LNCS, vol. 1782, pp. 305–319. Springer, Heidelberg (2000)
Ramalingam, G., Warshavsky, A., Field, J., Goyal, D., Sagiv, M.: Deriving specialized program analyses for certifying component-client conformance. In: Proc. Conf. on Prog. Lang. Design and Impl. pp. 83–94 (2002)
Reig, F.: Detecting security vulnerabilities in C code with type checking (extended abstract) (2003), http://www.cs.nott.ac.uk/~fxr/
Rinetskey, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Wilhelm, R. (ed.) CC 2001 and ETAPS 2001. LNCS, vol. 2027, pp. 133–149. Springer, Heidelberg (2001)
Rinetzky, N., Bauer, J., Reps, T., Sagiv, M., Wilhelm, R.: A semantics for procedure local heaps and its abstractions. In: Proc. Symp. on Principles of Prog. Languages (2005)
Rinetzky, N., Sagiv, M., Yahav, E.: Interprocedural shape analysis for cutpoint-free programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, Springer, Heidelberg (2005)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 24(3), 217–298 (2002)
Shaham, R., Yahav, E., Kolodner, E.K., Sagiv, M.: Establishing local temporal heap safety properties with applications to compile-time memory management. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 483–503. Springer, Heidelberg (2003)
Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng. 12(1), 157–171 (1986)
Yahav, E.: Verifying safety properties of concurrent Java programs using 3-valued logic. In: Proc. Symp. on Principles of Prog. Languages, pp. 27–40 (2001)
Yahav, E., Ramalingam, G.: Verifying safety properties using separation and heterogeneous abstractions. In: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, pp. 25–34. ACM Press, New York (2004), doi:10.1145/996841.996846
Yahav, E., Reps, T., Sagiv, M., Wilhelm, R.: Verifying temporal heap properties specified via evolution logic. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol. 2618, pp. 204–222. Springer, Heidelberg (2003)
Yahav, E., Sagiv, M.: Automatically verifying concurrent queue algorithms. In: Workshop on Software Model Checking (2003)
Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Tools and Algs.for the Construct.and Anal.of Syst. pp. 530–545 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Dor, N. et al. (2008). Automatic Verification of Strongly Dynamic Software Systems. 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_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_11
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)