Outputs (37)

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.

Multiple Pre/Post Specifications for Heap-Manipulating Methods (2007)
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.

Automated Verification of Shape, Size and Bag Properties (2007)
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.

Linking Object-Z with Spec# (2007)
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#.

Realizing Live Sequence Charts in SystemVerilog (2007)
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.

Automated Verification of Shape and Size Properties via Separation Logic (2007)
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.

HighSpec: a Tool for Building and Checking OZTA Models (2006)
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.

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

From statecharts to verilog : a formal approach to hardware/software co-specification (2006)
Journal Article
Qin, S., Chin, W., He, J., & Qiu, Z. (2006). From statecharts to verilog : a formal approach to hardware/software co-specification. Innovations in Systems and Software Engineering, 2(1), 17-38. https://doi.org/10.1007/s11334-005-0020-2

Hardware-Software co-specification is a critical phase in co-design. Our co-specification process starts with a high level graphical description in Statecharts and ends with an equivalent parallel composition of hardware and software descriptions in... Read More about From statecharts to verilog : a formal approach to hardware/software co-specification.