Nomair A. Naeem
ABSTRACT
For a single object, many programming errors can be detected by specifying the undesirable sequence of events using typestate. However, since objects interact with one another, defining temporal specifications only for a single object is too restrictive. In our research, we are interested in extending techniques from static typestate verification to static verification of multi-object temporal specifications.
- C. Allan, P. Avgustinov, A. Christensen, L. Hendren, S. Kuzins, O. Lhotk, O. de Moor, D. Sereni, G. Sittampalam, and a J. Tibble. Adding trace matching with free variables to AspectJ. OOPSLA, pages 345--364, 2005. Google Scholar
Digital Library
- E. Bodden, L. Hendren, and O. Lhotk. A staged static program analysis to improve the performance of runtime monitoring. ECOOP, pages 525--549, 2007. Google ScholarDigital Library
- A. Deutsch. A storeless model of aliasing and its abstractions using finite representations of right-regular equivalence relations. ICCL, pages 2--13, 1992.Google ScholarCross Ref
- S. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay. Effective typestate verification in the presence of aliasing. ISSTA, pages 133--144, 2006. Google ScholarDigital Library
- H. Jonkers. Abstract storage structures. de Bakker and van Vliet, editors, Algorithmic Languages, pages 321--343, 1981.Google Scholar
- N. A. Naeem and O. Lhotk. Extending typestate analysis to multiple interacting objects. Technical Report CS-2008-04, U. of Waterloo, 2008. To appear in OOPSLA'08.Google Scholar
- T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. POPL, 1995. Google ScholarDigital Library
- M. Sagiv, T. Reps, and S. Horwitz. Precise interprocedural dataflow analysis with applications to constant propagation. Theoretical Computer Science, 167(1-2):131--170, 1996. Google ScholarDigital Library
- R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng., 12(1):157--171, 1986. Google ScholarDigital Library
Index Terms
- Validating temporal properties of interacting objects
Recommendations
Typestate-like analysis of multiple interacting objects
OOPSLA '08: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applicationsThis paper presents a static analysis of typestate-like temporal specifications of groups of interacting objects, which are expressed using tracematches. Whereas typestate expresses a temporal specification of one object, a tracematch state may change ...
Typestate-like analysis of multiple interacting objects
This paper presents a static analysis of typestate-like temporal specifications of groups of interacting objects, which are expressed using tracematches. Whereas typestate expresses a temporal specification of one object, a tracematch state may change ...
The Clara framework for hybrid typestate analysis
A typestate property describes which operations are available on an object or a group of inter-related objects, depending on this object's or group's internal state, the typestate. Researchers in the field of static analysis have devised static program ...
Comments