Outputs (8)

Verifying BPEL-like Programs with Hoare Logic (2008)
Journal Article
Luo, C., Qin, S., & Qiu, Z. (2008). Verifying BPEL-like Programs with Hoare Logic. Frontiers of Computer Science in ChinabOnline, 2(4), 344-356. https://doi.org/10.1007/s11704-008-0039-2

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.

A Heap Model for Java Bytecode to Support Separation Logic (2008)
Presentation / Conference Contribution
Luo, C., He, G., & Qin, S. (2008, December). A Heap Model for Java Bytecode to Support Separation Logic. Presented at 15th Asia-Pacific Software Engineering Conference (APSEC 2008), Beijing, China

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.

Timed Automata Patterns (2008)
Journal Article
Dong, J., Hao, P., Qin, S., Sun, J., & Wang, Y. (2008). Timed Automata Patterns. IEEE Transactions on Software Engineering, 34(6), 844-859. https://doi.org/10.1109/tse.2008.52

Timed Automata have proven to be useful for specification and verification of real-time systems. System design using Timed Automata relies on explicit manipulation of clock variables. A number of automated analyzers for Timed Automata have been devel... Read More about Timed Automata Patterns.

A Formal Soundness Proof of Region-based Memory Management for Object-Oriented Paradigm (2008)
Presentation / Conference Contribution
Craciun, F., Qin, S., Chin, W., Liu, S., Maibaum, T., & Araki., K. (2008, October). A Formal Soundness Proof of Region-based Memory Management for Object-Oriented Paradigm. Presented at 10th International Conference on Formal Engineering Methods (ICFEM 2008), Kitakyushu, Japan

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)
Presentation / Conference Contribution
Luo, C., Qin, S., & Qiu, Z. (2008, June). Verifying BPEL-like Programs with Hoare Logic. Presented at International Symposium on Theoretical Aspects of Software Engineering, Nanjing, China

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)
Presentation / Conference Contribution
Chin, W.-N., Nguyen, H., Popeea, C., & Qin, S. (2008, June). Analysing Memory Resource Bounds for Low-Level Programs. Presented at 7th International Symposium on Memory Management, Tucson, Arizona

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)
Presentation / Conference Contribution
Luo, C., & Qin, S. (2008, June). Separation Logic for Multiple Inheritance. Presented at International Conference on Foundations of Informatics, Computing and Software, Shanghai, China

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)
Presentation / Conference Contribution
Chin, W.-N., David, C., Nguyen, H., Qin, S., Necula, G., & Wadler, P. (2008, January). Enhancing Modular OO Verification with Separation Logic. Presented at The 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008), San Francisco, USA

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.