Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 3 of 3
Full-Text Articles in Physical Sciences and Mathematics
A Quantum Interpretation Of Separating Conjunction For Local Reasoning Of Quantum Programs Based On Separation Logic, Xuan Bach Le, Shang-Wei Lin, Jun Sun, David Sanan
A Quantum Interpretation Of Separating Conjunction For Local Reasoning Of Quantum Programs Based On Separation Logic, Xuan Bach Le, Shang-Wei Lin, Jun Sun, David Sanan
Research Collection School Of Computing and Information Systems
It is well-known that quantum programs are not only complicated to write but also tedious to verify due to their enormous state-space and the sophisticated mathematics beneath. In this work, we propose a Hoare-style inference framework to verify quantum programs. We infuse separation logic in our framework and invent the $\hoarule{qframe}$ rule, the quantum counterpart of the frame rule, to support local reasoning of quantum programs. The design of our framework is planned with a mindset for intuition and human-readability, using vectors in Dirac notation for reasoning instead of the orthodox matrix representation as in existing approaches. For evaluation, we …
Towards Verification Of Computation Orchestration, Jin Song Dong, Yang Liu, Jun Sun, Xian Zhang
Towards Verification Of Computation Orchestration, Jin Song Dong, Yang Liu, Jun Sun, Xian Zhang
Research Collection School Of Computing and Information Systems
Recently, a promising programming model called Orc has been proposed to support a structured way of orchestrating distributed Web Services. Orc is intuitive because it offers concise constructors to manage concurrent communication, time-outs, priorities, failure of Web Services or communication and so forth. The semantics of Orc is precisely defined. However, there is no automatic verification tool available to verify critical properties against Orc programs. Our goal is to verify the orchestration programs (written in Orc language) which invoke web services to achieve certain goals. To investigate this problem and build useful tools, we explore in two directions. Firstly, we …
Modeling And Verifying Hierarchical Real-Time Systems Using Stateful Timed Csp, Jun Sun, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi, Étienne André
Modeling And Verifying Hierarchical Real-Time Systems Using Stateful Timed Csp, Jun Sun, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi, Étienne André
Research Collection School Of Computing and Information Systems
Modeling and verifying complex real-time systems are challenging research problems. The de facto approach is based on Timed Automata, which are finite state automata equipped with clock variables. Timed Automata are deficient in modeling hierarchical complex systems. In this work, we propose a language called Stateful Timed CSP and an automated approach for verifying Stateful Timed CSP models. Stateful Timed CSP is based on Timed CSP and is capable of specifying hierarchical real-time systems. Through dynamic zone abstraction, finite-state zone graphs can be generated automatically from Stateful Timed CSP models, which are subject to model checking. Like Timed Automata, Stateful …