All Outputs (6)

A Heap Model for Java Bytecode to Support Separation Logic (2008)
Conference Proceeding
Luo, C., He, G., & Qin, S. (2008). A Heap Model for Java Bytecode to Support Separation Logic. In 15th Asia-Pacific Software Engineering Conference, 2-5 December 2008, Beijing, China ; proceedings (127-134). https://doi.org/10.1109/apsec.2008.72

Memory usage analysis is an important problem for resource-constrained mobile devices, especially under mission- or safety-critical circumstances. Program codes running on or being downloaded into such devices are often available in low-level bytecod... Read More about A Heap Model for Java Bytecode to Support Separation Logic.

A Formal Soundness Proof of Region-based Memory Management for Object-Oriented Paradigm (2008)
Conference Proceeding
Craciun, F., Qin, S., Chin, W., Liu, S., Maibaum, T., & Araki., K. (2008). A Formal Soundness Proof of Region-based Memory Management for Object-Oriented Paradigm. In Formal methods and software engineering : 10th International Conference on Formal Engineering Methods, ICFEM 2008, 27-31 October 2008, Kitakyushu-City, Japan ; proceedings (126-146). https://doi.org/10.1007/978-3-540-88194-0_10

Region-based memory management has been proposed as a viable alternative to garbage collection for real-time applications and embedded software. In our previous work we have developed a region type inference algorithm that provides an automatic compi... Read More about A Formal Soundness Proof of Region-based Memory Management for Object-Oriented Paradigm.

Verifying BPEL-like Programs with Hoare Logic (2008)
Conference Proceeding
Luo, C., Qin, S., & Qiu, Z. (2008). Verifying BPEL-like Programs with Hoare Logic. In 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, 17-19 June 2008, Nanjing, China; proceedings (151-158). https://doi.org/10.1109/tase.2008.41

The WS-BPEL language has recently become a de facto standard for modeling Web-based business processes. One of its essential features is the fully programmable compensation mechanism. To understand it better, many recent works have mainly focused on... Read More about Verifying BPEL-like Programs with Hoare Logic.

Analysing Memory Resource Bounds for Low-Level Programs (2008)
Conference Proceeding
Chin, W., Nguyen, H., Popeea, C., & Qin, S. (2008). Analysing Memory Resource Bounds for Low-Level Programs. In 2008 International Symposium on Memory Management, ISMM’08, 7-8 June 2008, Tucson, AZ ; proceedings (151-160). https://doi.org/10.1145/1375634.1375656

Embedded systems are becoming more widely used but these systems are often resource constrained. Programming models for these systems should take into formal consideration resources such as stack and heap. In this paper, we show how memory resource b... Read More about Analysing Memory Resource Bounds for Low-Level Programs.

Separation Logic for Multiple Inheritance (2008)
Conference Proceeding
Luo, C., & Qin, S. (2008). Separation Logic for Multiple Inheritance. In 1st International Conference on Foundations of Informatics, Computing and Software, FICS 2008, 3-6 June, 2008, Shanghai, China ; proceedings (27-40). https://doi.org/10.1016/j.entcs.2008.04.051

As an extension to Floyd-Hoare logic, separation logic has been used to facilitate reasoning about imperative programs manipulating shared mutable data structures. Recently, it has also been extended to support modular reasoning in Java-like object-o... Read More about Separation Logic for Multiple Inheritance.

Enhancing Modular OO Verification with Separation Logic (2008)
Conference Proceeding
Chin, W., David, C., Nguyen, H., Qin, S., Necula, G., & Wadler, P. (2008). Enhancing Modular OO Verification with Separation Logic. In 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 7-12 January, 2008, San Francisco, California, USA ; proceedings (87-99). https://doi.org/10.1145/1328897.1328452

Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the specifications of overridden methods in supercla... Read More about Enhancing Modular OO Verification with Separation Logic.