Zobrazeno 1 - 10
of 86
pro vyhledávání: '"Zongyan Qiu"'
Publikováno v:
2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE).
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::bbf7f798050e12805a2c293e9065a237
https://doi.org/10.1109/ase51524.2021.9678836
https://doi.org/10.1109/ase51524.2021.9678836
Publikováno v:
TASE
Correct mutual-exclusion is one of the key challenges in concurrent programming. Although the fine-grained locking schema can be more efficient compared with the coarse-grained techniques, it is tough to use, as well as error-prone. Here we present a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::432f8948a49b5e47863756db64105e61
https://doi.org/10.1109/tase.2017.8285633
https://doi.org/10.1109/tase.2017.8285633
Autor:
Jinjiang Lei, Zongyan Qiu
Publikováno v:
Scientific Annals of Computer Science, Vol XXIV, Iss 2, Pp 217-252 (2014)
The difficulties of verifying concurrent programs lie in their inherent non-determinism and interferences. Rely-Guarantee reasoning is one useful approach to solve this problem for its capability in formally specifying inter- thread interferences. Ho
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::01e61773450dd36f881eef0a6e0c04c7
http://www.info.uaic.ro/bin/download/Annals/XXIV2/XXIV2_2.pdf
http://www.info.uaic.ro/bin/download/Annals/XXIV2/XXIV2_2.pdf
Autor:
Hai-Feng Guo, Zongyan Qiu
Publikováno v:
Software: Practice and Experience. 45:1519-1547
Grammar-based test generation provides a systematic approach to producing test cases from a given context-free grammar. Unfortunately, naive grammar-based test generation is problematic because of the fact that exhaustive random test case production
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::22ce4d71038178968edc0a611e18dd87
https://doi.org/10.1002/spe.2278
https://doi.org/10.1002/spe.2278
Publikováno v:
Frontiers of Computer Science. 7:710-728
Web service choreography describes global models of service interactions among a set of participants. For an interaction to be executed, the participants must know the required channel(s) used in the interaction, otherwise the execution will get stuc
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::208c83d09b2b2430bdb2a0da2ade5563
https://doi.org/10.1007/s11704-013-1238-z
https://doi.org/10.1007/s11704-013-1238-z
Publikováno v:
Frontiers of Computer Science. 7:236-256
Confinement is used to prohibit safety-critical objects from unintended access. Approaches for specifying and verifying confinement have been proposed in the last twenty years but their application has been help back. We develop a novel framework for
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d66b1dfde3e301b3c5e851d94d04e8f3
https://doi.org/10.1007/s11704-013-1259-7
https://doi.org/10.1007/s11704-013-1259-7
Publikováno v:
Dependable Software Engineering: Theories, Tools, and Applications ISBN: 9783319476766
SETTA
SETTA
Twig pattern minimization is an important aspect of XML query optimization. During the minimizing process, it usually needs to take advantage of the constraints of XML Schema. The traditional methods for identifying constraints is to develop correspo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7892c02dfe4dd952bc102dbe5fce7adb
https://doi.org/10.1007/978-3-319-47677-3_9
https://doi.org/10.1007/978-3-319-47677-3_9
Autor:
Ke Zhang, Zongyan Qiu
Publikováno v:
Software Engineering and Formal Methods ISBN: 9783319415901
SEFM
SEFM
We implement an OO specification and verification framework VeriJ in the proof assistant Coq. This framework covers the main OO features like encapsulation, inheritance and polymorphism. It can modularly specify and verify programs, while only one sp
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f163ec0844ed7dff8d88c39255dd2a18
https://doi.org/10.1007/978-3-319-41591-8_18
https://doi.org/10.1007/978-3-319-41591-8_18
Autor:
Ke Zhang, Zongyan Qiu
Publikováno v:
Programming Languages ISBN: 9783319452784
SBLP
SBLP
To modularly specify and verify object oriented programs on some abstract level, we need abstraction techniques to hide the implementation details of the classes. Model fields and abstract predicates are two most important approaches to address the r
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b6ad74e7a1d8010c001e69a2d4dc118d
https://doi.org/10.1007/978-3-319-45279-1_12
https://doi.org/10.1007/978-3-319-45279-1_12
Publikováno v:
Programming Languages ISBN: 9783319452784
SBLP
SBLP
Object ownership is an important technique in dealing with object sharing and aliasing to support verification of OO programs. Dynamic Ownership proposes a very flexible encapsulation discipline and has been adopted in Spec#. However, to use this tec
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::456a17be1f53a4154fd6b8f957de7b83
https://doi.org/10.1007/978-3-319-45279-1_6
https://doi.org/10.1007/978-3-319-45279-1_6