All Outputs (37)

A Relational Model for Object-Oriented Designs
Presentation / Conference Contribution
He, J., Liu, Z., Li, X., Qin, S., & Chin, W.-N. (2004, November). A Relational Model for Object-Oriented Designs. Presented at Second ASIAN Symposium on Programming Languages and Systems (APLAS 2004), Taipei, Taiwan

This paper develops a mathematical characterisation of object-oriented concepts by defining an observation-oriented semantics for an object-oriented language (OOL) with a rich variety of features including subtypes, visibility, inheritance, dynamic b... Read More about A Relational Model for Object-Oriented Designs.

Constructing Property-Oriented Models for Verification
Presentation / Conference Contribution
He, J., Qin, S., & Sherif, A. (2006, February). Constructing Property-Oriented Models for Verification. Presented at First International Symposium on Unifying Theories of Programming (UTP 2006), County Durham, UK

This paper advocates a general approach to formal verification by constructing property-oriented models. We instantiate the approach using timing properties, and construct a heterogeneous untimed model in which time is abstracted away, so that we can... Read More about Constructing Property-Oriented Models for Verification.

Integrating Probability with Time and Shared-Variable Concurrency
Presentation / Conference Contribution
Zhu, H., Qin, S., He, J., & Bowen, J. (2005, April). Integrating Probability with Time and Shared-Variable Concurrency. Presented at The 30th Nasa/IEEE Software Engineering Workshop (SEW-30), Columbia, Maryland, USA

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 Integrating Probability with Time and Shared-Variable Concurrency.

Automated Verification of Shape and Size Properties via Separation Logic
Presentation / Conference Contribution
Nguyen, H.-H., David, C., Qin, S., Chin, W.-N., Cook, B., & Podelski, A. (2007, January). Automated Verification of Shape and Size Properties via Separation Logic. Presented at Eighth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007), Nice, France

Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is concise, precise and expressive for ensuring the safety of pointer-b... Read More about Automated Verification of Shape and Size Properties via Separation Logic.

Automated Verification of Shape, Size and Bag Properties
Presentation / Conference Contribution
Chin, W., David, C., Nguyen, H., & Qin, S. (2007, July). Automated Verification of Shape, Size and Bag Properties. Presented at 12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007), Auckland, New Zealand

In recent years, separation logic has emerged as a contender for formal reasoning of heap-manipulating imperative programs. Recent works have focused on specialised provers that are mostly based on fixed sets of predicates. To improve expressivity, w... Read More about Automated Verification of Shape, Size and Bag Properties.

HighSpec: a Tool for Building and Checking OZTA Models
Presentation / Conference Contribution
Dong, J., Hao, P., Zhang, X., & Qin, S. (2006, May). HighSpec: a Tool for Building and Checking OZTA Models. Presented at 28th International Conference on Software Engineering (ICSE 2006), Shanghai, China

HighSpec is an interactive system for composing and checking OZTA specifications. The integrated high level specification language, OZTA, is a combination of Object-Z (OZ) and Timed Automata (TA). Building on the strength of Object-Z's in specifying... Read More about HighSpec: a Tool for Building and Checking OZTA Models.

Linking Object-Z with Spec#
Presentation / Conference Contribution
Qin, S., & He, G. (2007, July). Linking Object-Z with Spec#. Presented at 12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007), Auckland, New Zealand

Formal specifications have been a focus of software engineering research for many years and have been applied in a wide variety of settings. Their use in software engineering not only promotes high-level verification via theorem proving or model chec... Read More about Linking Object-Z with Spec#.

Analysing Memory Resource Bounds for Low-Level Programs
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.

An Interval-based Inference of Variant Parametric Types
Presentation / Conference Contribution
Craciun, F., Chin, W.-N., He, G., Qin, S., & Castagna, G. (2009, March). An Interval-based Inference of Variant Parametric Types. Presented at 18th European Symposium on Programming (ESOP 2009), York, UK

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.

Separation Logic for Multiple Inheritance
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.

A Formal Soundness Proof of Region-based Memory Management for Object-Oriented Paradigm
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.

Realizing Live Sequence Charts in SystemVerilog
Presentation / Conference Contribution
Wang, H., Qin, S., Sun, J., & Dong, J. (2007, June). Realizing Live Sequence Charts in SystemVerilog. Presented at First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE 2007), Shanghai, China

The design of an embedded control system starts with an investigation of properties and behaviors of the process evolving within its environment, and an analysis of the requirement for its safety performance. In early stages, system requirements are... Read More about Realizing Live Sequence Charts in SystemVerilog.

Multiple Pre/Post Specifications for Heap-Manipulating Methods
Presentation / Conference Contribution
Chin, W., David, C., Nguyen, H., & Qin, S. (2007, November). Multiple Pre/Post Specifications for Heap-Manipulating Methods. Presented at 10th IEEE High Assurance Systems Engineering Symposium (HASE 2007), Dallas, Texas, USA

Automated verification plays an important role for high assurance software. This typically uses a pair of pre/post conditions as a formal (but possibly partial) specification of each method before it is systematically verified. In this paper, we advo... Read More about Multiple Pre/Post Specifications for Heap-Manipulating Methods.

Enhancing Modular OO Verification with Separation Logic
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.

Verifying BPEL-like Programs with Hoare Logic
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.

A Heap Model for Java Bytecode to Support Separation Logic
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.

Memory Usage Verification Using Hip/Sleek
Presentation / Conference Contribution
He, G., Qin, S., Luo, C., W.-n., C., Liu, Z., & Ravn, A. (2009, October). Memory Usage Verification Using Hip/Sleek. Presented at 7th International Symposium on Automated Technology for Verification and Analysis (ATVA 2009), Macao, China

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.