All Outputs (31)

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.

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.

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.

Multiple Pre/Post Specifications for Heap-Manipulating Methods (2007)
Conference Proceeding
Chin, W., David, C., Nguyen, H., & Qin, S. (2007). Multiple Pre/Post Specifications for Heap-Manipulating Methods. In IEEE International Symposium on High Assurance Systems Engineering : 14-16 November 2007, Dallas, Texas ; proceedings. (357-364). https://doi.org/10.1109/hase.2007.19

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.

Linking Object-Z with Spec# (2007)
Conference Proceeding
Qin, S., & He, G. (2007). Linking Object-Z with Spec#. In 12th IEEE International Conference on Engineering of Complex Computer Systems, 11-14 Jul 2007, Auckland, New Zealand ; proceedings (185-196). https://doi.org/10.1109/iceccs.2007.27

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

Automated Verification of Shape, Size and Bag Properties (2007)
Conference Proceeding
Chin, W., David, C., Nguyen, H., & Qin, S. (2007). Automated Verification of Shape, Size and Bag Properties. In 12th IEEE International Conference on Engineering of Complex Computer Systems, 11-14 Jul 2007, Auckland, New Zealand ; proceedings (307-320). https://doi.org/10.1109/iceccs.2007.17

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.

Realizing Live Sequence Charts in SystemVerilog (2007)
Conference Proceeding
Wang, H., Qin, S., Sun, J., & Dong, J. (2007). Realizing Live Sequence Charts in SystemVerilog. In 1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering : June 6-8 2007, Shanghai ; proceedings (379-388). https://doi.org/10.1109/tase.2007.41

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.

Automated Verification of Shape and Size Properties via Separation Logic (2007)
Conference Proceeding
Nguyen, H., David, C., Qin, S., Chin, W., Cook, B., & Podelski, A. (2007). Automated Verification of Shape and Size Properties via Separation Logic. In Proceeding of the 8th international conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007) (251-266). https://doi.org/10.1007/978-3-540-69738-1_18

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.

HighSpec: a Tool for Building and Checking OZTA Models (2006)
Conference Proceeding
Dong, J., Hao, P., Zhang, X., & Qin, S. (2006). HighSpec: a Tool for Building and Checking OZTA Models. In 28th International Conference on Software Engineering, 20-28 May 2006, Shanghai, China ; proceedings (775-778). https://doi.org/10.1145/1134409

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.

Integrating Probability with Time and Shared-Variable Concurrency (2006)
Conference Proceeding
Zhu, H., Qin, S., He, J., & Bowen, J. (2006). Integrating Probability with Time and Shared-Variable Concurrency. In 30th Annual IEEE/NASA Software Engineering Workshop, SEW-30, 24-28 April 2005, Columbia, Maryland ; proceedings (179-189). https://doi.org/10.1109/sew.2006.22

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.

Constructing Property-Oriented Models for Verification (2006)
Conference Proceeding
He, J., Qin, S., & Sherif, A. (2006). Constructing Property-Oriented Models for Verification. In Unifying theories of programming : first international symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006 : revised selected papers (85-100). https://doi.org/10.1007/11768173_6

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.

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.

A Relational Model for Object-Oriented Designs (2004)
Conference Proceeding
He, J., Liu, Z., Li, X., Qin, S., & Chin, W. (2004). A Relational Model for Object-Oriented Designs. In Programming languages and systems : Second Asian Symposium, APLAS 2004, 4-6 November 2004, Taipei, Taiwan ; proceedings (415-436). https://doi.org/10.1007/978-3-540-30477-7_28

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.