Outputs (37)

PTSC: probability, time and shared-variable concurrency (2009)
Journal Article
Zhu, H., Qin, S., He, J., & Bowen, J. (2009). PTSC: probability, time and shared-variable concurrency. Innovations in Systems and Software Engineering, 5(4), 271-284. https://doi.org/10.1007/s11334-009-0100-9

Complex software systems typically involve features like time, concurrency and probability, where probabilistic computations play an increasing role. It is challenging to formalize languages comprising all these features. In this paper, we integrate... Read More about PTSC: probability, time and shared-variable concurrency.

Memory Usage Verification Using Hip/Sleek (2009)
Conference Proceeding
He, G., Qin, S., Luo, C., W.-n., C., Liu, Z., & Ravn, A. (2009). Memory Usage Verification Using Hip/Sleek. In Automated technology for verification and analysis : 7th International Symposium, ATVA 2009, 14-16 October, 2009, Macao, China ; proceedings (166-181). https://doi.org/10.1007/978-3-642-04761-9_14

Embedded systems often come with constrained memory footprints. It is therefore essential to ensure that software running on such platforms fulfils memory usage specifications at compile-time, to prevent memory-related software failure after deployme... Read More about Memory Usage Verification Using Hip/Sleek.

Theoretical Aspects of Software Engineering. The 3rd IEEE International Symposium (2009)
Book
Chin, W., & Qin, S. (Eds.). (2009). Theoretical Aspects of Software Engineering. The 3rd IEEE International Symposium. Institute of Electrical and Electronics Engineers

An Interval-based Inference of Variant Parametric Types (2009)
Conference Proceeding
Craciun, F., Chin, W., He, G., Qin, S., & Castagna, G. (2009). An Interval-based Inference of Variant Parametric Types. In Programming languages and systems : 18th European Symposium on Programming, ESOP 2009 : held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, 22-29 March, 2009 ; proceedings (112-127). https://doi.org/10.1007/978-3-642-00590-9_9

Variant parametric types represent the successful integration of subtype and parametric polymorphism to support a more flexible subtyping for Java like languages. A key feature that helps strengthen this integration is the use-site variance. Dependin... Read More about An Interval-based Inference of Variant Parametric Types.

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)
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.

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)
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.