All Outputs (3)

The Semantics and Tool Support of OZTA (2005)
Conference Proceeding
Dong, J., Hao, P., Qin, S., & Zhang, X. (2005). The Semantics and Tool Support of OZTA. In Formal methods and software engineering : 7th International Conference on Formal Engineering Methods, ICFEM 2005, 1-4 November, 2005, Manchester, UK ; proceedings (66-80). https://doi.org/10.1007/11576280_6

In this work, we firstly enhance OZTA, a combination of Object-Z and Timed Automata, by introducing a set of timed patterns as language constructs that can specify the dynamic and timing features of complex real-time systems in a systematic way. Then... Read More about The Semantics and Tool Support of OZTA.

Memory Usage Verification for OO Programs (2005)
Conference Proceeding
Chin, W., Nguyen, H., Qin, S., & Rinard, M. (2005). Memory Usage Verification for OO Programs. In Static analysis : 12th International Symposium, SAS 2005, 7-9 September 2005, London, UK ; proceedings (70-86). https://doi.org/10.1007/11547662_7

We present a new type system for an object-oriented (OO) language that characterizes the sizes of data structures and the amount of heap memory required to successfully execute methods that operate on these data structures. Key components of this typ... Read More about Memory Usage Verification for OO Programs.

Verifying safety policies with size properties and alias controls (2005)
Conference Proceeding
Chin, W., Khoo, S., Qin, S., Popeea, C., & Nguyen, H. (2005). Verifying safety policies with size properties and alias controls. In Proceedings of the 27th International Conference on Software Engineering, ICSE 05, 15-21 May 2005, St Louis MO (186-195). https://doi.org/10.1145/1062455.1062500

Many software properties can be analysed through a relational size analysis on each function’s inputs and outputs. Such relational analysis (through a form of dependent typing) has been successfully applied to declarative programs, and to restricted... Read More about Verifying safety policies with size properties and alias controls.