Open Access. Powered by Scholars. Published by Universities.®
- Discipline
-
- Physical Sciences and Mathematics (4221)
- Computer Sciences (4218)
- Databases and Information Systems (1556)
- Software Engineering (1250)
- Artificial Intelligence and Robotics (755)
-
- Information Security (739)
- Graphics and Human Computer Interfaces (493)
- Numerical Analysis and Scientific Computing (453)
- Engineering (346)
- Programming Languages and Compilers (268)
- Computer Engineering (233)
- Social and Behavioral Sciences (213)
- Theory and Algorithms (212)
- Business (202)
- OS and Networks (149)
- Communication (102)
- Operations Research, Systems Engineering and Industrial Engineering (101)
- Social Media (83)
- Data Storage Systems (82)
- Medicine and Health Sciences (80)
- Education (68)
- Public Affairs, Public Policy and Public Administration (55)
- Computer and Systems Architecture (52)
- Health Information Technology (52)
- Transportation (51)
- Management Information Systems (49)
- Digital Communications and Networking (47)
- E-Commerce (44)
- Finance and Financial Management (40)
- Higher Education (30)
- Keyword
-
- Deep learning (70)
- Machine learning (59)
- Privacy (44)
- Empirical study (40)
- Deep Learning (35)
-
- Security (34)
- Training (34)
- Task analysis (32)
- Cloud computing (31)
- Data mining (31)
- Artificial intelligence (29)
- Reinforcement learning (29)
- Social media (29)
- Software engineering (29)
- Neural networks (28)
- Android (27)
- Blockchain (27)
- Feature extraction (27)
- Large Language Models (26)
- Model Check (26)
- Servers (26)
- Access control (25)
- Large language models (25)
- Authentication (24)
- Encryption (24)
- Natural language processing (24)
- Privacy-preserving (24)
- Anomaly detection (23)
- Large Language Model (23)
- Visualization (23)
- Publication Year
Articles 2281 - 2310 of 4271
Full-Text Articles in Entire DC Network
Improved Construction For Inner Product Functional Encryption, Qingsong Zhao, Qingkai Zeng, Ximeng Liu
Improved Construction For Inner Product Functional Encryption, Qingsong Zhao, Qingkai Zeng, Ximeng Liu
Research Collection School Of Computing and Information Systems
Functional encryption (FE) is a vast new paradigm for encryption scheme which allows tremendous flexibility in accessing encrypted data. In a FE scheme, a user can learn specific function of encrypted messages by restricted functional key and reveals nothing else about the messages. Besides the standard notion of data privacy in FE, it should protect the privacy of the function itself which is also crucial for practical applications. In this paper, we construct a secret key FE scheme for the inner product functionality using asymmetric bilinear pairing groups of prime order. Compared with the existing similar schemes, our construction reduces …
Slade: A Smart Large-Scale Task Decomposer In Crowdsourcing, Yongxin Tong, Lei Chen, Zimu Zhou, H. V. Jagadish, Lidan Shou
Slade: A Smart Large-Scale Task Decomposer In Crowdsourcing, Yongxin Tong, Lei Chen, Zimu Zhou, H. V. Jagadish, Lidan Shou
Research Collection School Of Computing and Information Systems
Crowdsourcing has been shown to be effective in a wide range of applications, and is seeing increasing use. A large-scale crowdsourcing task often consists of thousands or millions of atomic tasks, each of which is usually a simple task such as binary choice or simple voting. To distribute a large-scale crowdsourcing task to limited crowd workers, a common practice is to pack a set of atomic tasks into a task bin and send to a crowd worker in a batch. It is challenging to decompose a large-scale crowdsourcing task and execute batches of atomic tasks, which ensures reliable answers at …
User-Friendly Deniable Storage For Mobile Devices, Bing Chang, Yao Cheng, Bo Chen, Fengwei Zhang, Wen-Tao Zhu, Yanju Liu, Zhan Wang
User-Friendly Deniable Storage For Mobile Devices, Bing Chang, Yao Cheng, Bo Chen, Fengwei Zhang, Wen-Tao Zhu, Yanju Liu, Zhan Wang
Research Collection School Of Computing and Information Systems
Mobile devices are prevalently used to process sensitive data, but traditional encryption may not work when an adversary is able to coerce the device owners to disclose the encryption keys. Plausibly Deniable Encryption (PDE) is thus designed to protect sensitive data against this powerful adversary. In this paper, we present MobiPluto, a user-friendly PDE scheme for denying the existence of sensitive data stored on mobile devices. A salient difference between MobiPluto and the existing PDE systems is that any block-based file systems can be deployed on top of it. To further improve usability and deniability of MobiPluto, we introduce a …
Secure Smart Metering Based On Lora Technology, Yao Cheng, Hendra Saputra, Leng Meng Goh, Yongdong Wu
Secure Smart Metering Based On Lora Technology, Yao Cheng, Hendra Saputra, Leng Meng Goh, Yongdong Wu
Research Collection School Of Computing and Information Systems
Smart metering allows Substation Automation System (SAS) to remotely and timely read smart meters. Despite its advantages, smart metering brings some challenges. a) It introduces cyber attack risks to the metering system, which may lead to user privacy leakage or even the compromise of smart metering systems. b) Although the majority of meters are located within a regional power supply area, some hard-to-reach nodes are geographically far from the clustered area, which account for a big portion of the entire smart metering operation cost. Facing the above challenges, we propose a secure smart metering infrastructure based on LoRa technology which …
Securing Display Path For Security-Sensitive Applications On Mobile Devices, Jinhua Cui, Yuanyuan Zhang, Zhiping Cai, Anfeng Liu, Yangyang Li
Securing Display Path For Security-Sensitive Applications On Mobile Devices, Jinhua Cui, Yuanyuan Zhang, Zhiping Cai, Anfeng Liu, Yangyang Li
Research Collection School Of Computing and Information Systems
While smart devices based on ARM processor bring us a lot of convenience, they also become an attractive target of cyber-attacks. The threat is exaggerated as commodity OSes usually have a large code base and suffer from various software vulnerabilities. Nowadays, adversaries prefer to steal sensitive data by leaking the content of display output by a security-sensitive application. A promising solution is to exploit the hardware visualization extensions provided by modern ARM processors to construct a secure display path between the applications and the display device. In this work, we present a scheme named SecDisplay for trusted display service, it …
Hybrid Privacy-Preserving Clinical Decision Support System In Fog-Cloud Computing, Ximeng Liu, Robert H. Deng, Yang Yang, Ngoc Hieu Tran, Shangping Zhong
Hybrid Privacy-Preserving Clinical Decision Support System In Fog-Cloud Computing, Ximeng Liu, Robert H. Deng, Yang Yang, Ngoc Hieu Tran, Shangping Zhong
Research Collection School Of Computing and Information Systems
In this paper, we propose a framework for hybrid privacy-preserving clinical decision support system in fog cloud computing, called HPCS. In HPCS, a fog server uses a lightweight data mining method to securely monitor patients' health condition in real-time. The newly detected abnormal symptoms can be further sent to the cloud server for high-accuracy prediction in a privacy-preserving way. Specifically, for the fog servers, we design a new secure outsourced inner-product protocol for achieving secure lightweight single-layer neural network. Also, a privacy-preserving piecewise polynomial calculation protocol allows cloud server to securely perform any activation functions in multiple-layer neural network. Moreover, …
A Lightweight Policy Preserving Ehr Sharing Scheme In The Cloud, Zuobin Ying, Lu Wei, Qi Li, Ximeng Liu, Jie Cui
A Lightweight Policy Preserving Ehr Sharing Scheme In The Cloud, Zuobin Ying, Lu Wei, Qi Li, Ximeng Liu, Jie Cui
Research Collection School Of Computing and Information Systems
Electronic Health Record (EHR) is a digital health documentary. It contains not only the health-related records but also the personal sensitive information. Therefore, how to reliably share EHR through the cloud is a challenging issue. Ciphertext-policy attribute-based encryption (CP-ABE) is a promising cryptography prototype, which can achieve fine-grained access control as well as one-to-many encryption. In CP-ABE, access policy is attached to the ciphertext, and however, the access policy is not protected, which will also cause some privacy leakage. In this paper, we propose a policy preserving EHR system on the basis of CP-ABE. Specifically, we designed an algorithm, which …
Strong Identity-Based Proxy Signature Schemes, Revisited, Weiwei Liu, Yi Mu, Guomin Yang, Yangguang Tian
Strong Identity-Based Proxy Signature Schemes, Revisited, Weiwei Liu, Yi Mu, Guomin Yang, Yangguang Tian
Research Collection School Of Computing and Information Systems
Proxy signature is a useful cryptographic primitive that has been widely used in many applications. It has attracted a lot of attention since it was introduced. There have been lots of works in constructing efficient and secure proxy signature schemes. In this paper, we identify a new attack that has been neglected by many existing proven secure proxy signature schemes. We demonstrate this attack by launching it against an identity-based proxy signature scheme which is proven secure. We then propose one method that can effectively prevent this attack. The weakness in some other proxy signature schemes can also be fixed …
Skylens: Visual Analysis Of Skyline On Multi-Dimensional Data, Xun Zhao, Yanhong Wu, Weiwei Cui, Xinnan Du, Yuan Chen, Yong Wang, Dik Lun Lee, Huamin Qu
Skylens: Visual Analysis Of Skyline On Multi-Dimensional Data, Xun Zhao, Yanhong Wu, Weiwei Cui, Xinnan Du, Yuan Chen, Yong Wang, Dik Lun Lee, Huamin Qu
Research Collection School Of Computing and Information Systems
Skyline queries have wide-ranging applications in fields that involve multi-criteria decision making, including tourism, retail industry, and human resources. By automatically removing incompetent candidates, skyline queries allow users to focus on a subset of superior data items (i.e.. the skyline), thus reducing the decision-making overhead. However, users are still required to interpret and compare these superior items manually before making a successful choice. This task is challenging because of two issues. First, people usually have fuzzy, unstable, and inconsistent preferences when presented with multiple candidates. Second, skyline queries do not reveal the reasons for the superiority of certain skyline points …
Collaborative Fall Detection Using Smartphone And Kinect, Xue Li, Lanshun Nie, Hanchuan Xu, Xianzhi Wang
Collaborative Fall Detection Using Smartphone And Kinect, Xue Li, Lanshun Nie, Hanchuan Xu, Xianzhi Wang
Research Collection School Of Computing and Information Systems
Humanfall detection has attracted broad attentions as sensors and mobile devices are increasingly adopted in real-life scenarios such as smart homes. The complexity of activities in home environments pose severe challenges to the fall detection research with respect to the detection accuracy. We propose a collaborative detection platform that combines two subsystems: a threshold-based fall detection subsystem using mobile phones and a support vector machine (SVM)-based fall detection subsystem using Kinects. Both subsystems have their respective confidence models and the platform detects falls by fusing the data of both subsystems using two methods: the logical rules-based and D-S evidence fusion …
Simulation-Based Security Of Function-Hiding Inner Product Encryption, Qingsong Zhao, Qingkai Zeng, Ximeng Liu, Huanliang Xu
Simulation-Based Security Of Function-Hiding Inner Product Encryption, Qingsong Zhao, Qingkai Zeng, Ximeng Liu, Huanliang Xu
Research Collection School Of Computing and Information Systems
Functional encryption (FE) [1,2] is a modern type of encryption scheme that extends several previous notions and allows tremendous flexibility in controlling and computing on encrypted data. FE enables an authority to derive constrained decryption keys that are used by a user to obtain specific functions of encrypted messages. Informally, the authority generates a secret key skf for a function f from a master secret key. Then, the user can only learn f(x) from a ciphertext Enc(x) with skf and reveal nothing else about x.
A Compact Representation Of Human Actions By Sliding Coordinate Coding, Runwei Ding, Qianru Sun, Mengyuan Liu, Hong Liu
A Compact Representation Of Human Actions By Sliding Coordinate Coding, Runwei Ding, Qianru Sun, Mengyuan Liu, Hong Liu
Research Collection School Of Computing and Information Systems
Human action recognition remains challenging in realistic videos, where scale and viewpoint changes make the problem complicated. Many complex models have been developed to overcome these difficulties, while we explore using low-level features and typical classifiers to achieve the state-of-the-art performance. The baseline model of feature encoding for action recognition is bag-of-words model, which has shown high efficiency but ignores the arrangement of local features. Refined methods compensate for this problem by using a large number of co-occurrence descriptors or a concatenation of the local distributions in designed segments. In contrast, this article proposes to encode the relative position of …
Pose Guided Person Image Generation, Liqian Ma, Xu Jia, Qianru Sun, Bernt Schiele, Tinne Tuytelaars, Luc Van Gool
Pose Guided Person Image Generation, Liqian Ma, Xu Jia, Qianru Sun, Bernt Schiele, Tinne Tuytelaars, Luc Van Gool
Research Collection School Of Computing and Information Systems
This paper proposes the novel Pose Guided Person Generation Network (PG$^2$) that allows to synthesize person images in arbitrary poses, based on an image of that person and a novel pose. Our generation framework PG^2 utilizes the pose information explicitly and consists of two key stages: pose integration and image refinement. In the first stage the condition image and the target pose are fed into a U-Net-like network to generate an initial but coarse image of the person with the target pose. The second stage then refines the initial and blurry result by training a U-Net-like generator in an adversarial …
Law Enforcement Resource Optimization With Response Time Guarantees, Jonathan Chase, Jiali Du, Na Fu, Truc Viet Le, Hoong Chuin Lau
Law Enforcement Resource Optimization With Response Time Guarantees, Jonathan Chase, Jiali Du, Na Fu, Truc Viet Le, Hoong Chuin Lau
Research Collection School Of Computing and Information Systems
In a security-conscious world, and with the rapid increase in the global urbanized population, there is a growing challenge for law enforcement agencies to efficiently respond to emergency calls. We consider the problem of spatially and temporally optimizing the allocation of law enforcement resources such that the quality of service (QoS) in terms of emergency response time can be guaranteed. To solve this problem, we provide a spatio-temporal MILP optimization model, which we learn from a real-world dataset of incidents and dispatching records, and solve by existing solvers. One key feature of our proposed model is the introduction of risk …
Eacsip: Extendable Access Control System With Integrity Protection For Enhancing Collaboration In The Cloud, Willy Susilo, Peng Jiang, Fuchun Guo, Guomin Yang, Yong Yu, Yi Mu
Eacsip: Extendable Access Control System With Integrity Protection For Enhancing Collaboration In The Cloud, Willy Susilo, Peng Jiang, Fuchun Guo, Guomin Yang, Yong Yu, Yi Mu
Research Collection School Of Computing and Information Systems
It is widely acknowledged that the collaborations with more users increase productivity. Secure cloud storage is a promising tool to enhance such a collaboration. Access control system can be enabled with attribute-based encryption. In this system, a user encrypts and uploads his/her data to the cloud with an access policy, such that only people who satisfy that access policy can decrypt the data. When a recipient would like to enable another person who is originally unauthorized by the original access policy, this recipient will need to extend the access policy by adding a new policy that includes the new person …
Vkse-Mo: Verifiable Keyword Search Over Encrypted Data In Multi-Owner Settings, Yinbin Miao, Jianfeng Ma, Ximeng Liu, Junwei Zhang, Zhiquan Liu
Vkse-Mo: Verifiable Keyword Search Over Encrypted Data In Multi-Owner Settings, Yinbin Miao, Jianfeng Ma, Ximeng Liu, Junwei Zhang, Zhiquan Liu
Research Collection School Of Computing and Information Systems
Searchable encryption (SE) techniques allow cloud clients to easily store data and search encrypted data in a privacy-preserving manner, where most of SE schemes treat the cloud server as honest-but-curious. However, in practice, the cloud server is a semi-honest-but-curious third-party, which only executes a fraction of search operations and returns a fraction of false search results to save its computational and bandwidth resources. Thus, it is important to provide a results verification method to guarantee the correctness of the search results. Existing SE schemes allow multiple data owners to upload different records to the cloud server, but these schemes have …
What Do Developers Search For On The Web?, Xin Xia, Lingfeng Bao, David Lo, Pavneet Singh Kochhar, Ahmed E. Hassan, Zhenchang Xing
What Do Developers Search For On The Web?, Xin Xia, Lingfeng Bao, David Lo, Pavneet Singh Kochhar, Ahmed E. Hassan, Zhenchang Xing
Research Collection School Of Computing and Information Systems
Developers commonly make use of a web search engine such as Google to locate online resources to improve their productivity. A better understanding of what developers search for could help us understand their behaviors and the problems that they meet during the software development process. Unfortunately, we have a limited understanding of what developers frequently search for and of the search tasks that they often find challenging. To address this gap, we collected search queries from 60 developers, surveyed 235 software engineers from more than 21 countries across five continents. In particular, we asked our survey participants to rate the …
D-Watch: Embracing “Bad” Multipaths For Device-Free Localization With Cots Rfid Devices, Ju Wang, Jie Xiong, Hongbo Jiang, Xiaojiang Chen, Dingyi Fang
D-Watch: Embracing “Bad” Multipaths For Device-Free Localization With Cots Rfid Devices, Ju Wang, Jie Xiong, Hongbo Jiang, Xiaojiang Chen, Dingyi Fang
Research Collection School Of Computing and Information Systems
Device-free localization, which does not require any device attached to the target, is playing a critical role in many applications, such as intrusion detection, elderly monitoring and so on. This paper introduces D-Watch, a device-free system built on the top of low cost commodity-off-the-shelf RFID hardware. Unlike previous works which consider multipaths detrimental, D-Watch leverages the ''bad'' multipaths to provide a decimeter-level localization accuracy without offline training. D-Watch harnesses the angle-of-arrival information from the RFID tags' backscatter signals. The key intuition is that whenever a target blocks a signal's propagation path, the signal power experiences a drop which can be …
Leveraging Auxiliary Tasks For Document-Level Cross-Domain Sentiment Classification, Jianfei Yu, Jing Jiang
Leveraging Auxiliary Tasks For Document-Level Cross-Domain Sentiment Classification, Jianfei Yu, Jing Jiang
Research Collection School Of Computing and Information Systems
In this paper, we study domain adaptationwith a state-of-the-art hierarchicalneural network for document-level sentimentclassification. We first design a newauxiliary task based on sentiment scoresof domain-independent words. We thenpropose two neural network architecturesto respectively induce document embeddingsand sentence embeddings that workwell for different domains. When thesedocument and sentence embeddings areused for sentiment classification, we findthat with both pseudo and external sentimentlexicons, our proposed methods canperform similarly to or better than severalhighly competitive domain adaptationmethods on a benchmark dataset of productreviews.
Multi-User Multi-Keyword Rank Search Over Encrypted Data In Arbitrary Language, Yang Yang, Ximeng Liu, Robert H. Deng
Multi-User Multi-Keyword Rank Search Over Encrypted Data In Arbitrary Language, Yang Yang, Ximeng Liu, Robert H. Deng
Research Collection School Of Computing and Information Systems
Multi-keyword rank searchable encryption (MRSE) returns the top-k results in response to a data user's request of multi-keyword search over encrypted data, and hence provides an efficient way for preserving data privacy in cloud storage systems while without loss of data usability. Many existing MRSE systems are constructed based on an algorithm which we term as k-nearest neighbor for searchable encryption (KNN-SE). Unfortunately, KNN-SE has a number of shortcomings which limit its practical applications. In this paper, we propose a new MRSE system which overcomes almost all the defects of the KNN-SE based MRSE systems. Specifically, our new system does …
Graphmp: An Efficient Semi-External-Memory Big Graph Processing System On A Single Machine, Peng Sun, Yonggang Wen, Nguyen Binh Duong Ta, Xiaokui Xiao
Graphmp: An Efficient Semi-External-Memory Big Graph Processing System On A Single Machine, Peng Sun, Yonggang Wen, Nguyen Binh Duong Ta, Xiaokui Xiao
Research Collection School Of Computing and Information Systems
Recent studies showed that single-machine graph processing systems can be as highly competitive as clusterbased approaches on large-scale problems. While several outof-core graph processing systems and computation models have been proposed, the high disk I/O overhead could significantly reduce performance in many practical cases. In this paper, we propose GraphMP to tackle big graph analytics on a single machine. GraphMP achieves low disk I/O overhead with three techniques. First, we design a vertex-centric sliding window (VSW) computation model to avoid reading and writing vertices on disk. Second, we propose a selective scheduling method to skip loading and processing unnecessary edge …
Towards Tightly Secure Deterministic Public Key Encryption, Daode Zhang, Bao Li, Yamin Liu, Haiyang Xue, Xianhui Lu, Dingding Jia
Towards Tightly Secure Deterministic Public Key Encryption, Daode Zhang, Bao Li, Yamin Liu, Haiyang Xue, Xianhui Lu, Dingding Jia
Research Collection School Of Computing and Information Systems
In this paper, we formally consider the construction of tightly secure deterministic public key encryption (D-PKE). Initially, we compare the security loss amongst the D-PKE schemes under the concrete assumptions and also analyze the tightness of generic D-PKE constructions. Furthermore, we prove that the CPA secure D-PKE scheme of Boldyreva et al. (Crypto’08) is tightly PRIV-IND-CPA secure for block-sources. Our security reduction improves the security loss of their scheme from O(nc∗) to O(1). Additionally, by upgrading the all-but-one trapdoor function (TDF) in the construction of Boldyreva et al. to all-but-n TDF defined by Hemenway et al. (Asiacrypt’11), we give general …
A Multiagent-Based Approach For Vehicle Routing By Considering Both Arriving On Time And Total Travel Time, Zhiguang Cao, Hongliang Guo, Jie Zhang
A Multiagent-Based Approach For Vehicle Routing By Considering Both Arriving On Time And Total Travel Time, Zhiguang Cao, Hongliang Guo, Jie Zhang
Research Collection School Of Computing and Information Systems
Arriving on time and total travel time are two important properties for vehicle routing. Existing route guidance approaches always consider them independently, because they may conflict with each other. In this article, we develop a semi-decentralized multiagent-based vehicle routing approach where vehicle agents follow the local route guidance by infrastructure agents at each intersection, and infrastructure agents perform the route guidance by solving a route assignment problem. It integrates the two properties by expressing them as two objective terms of the route assignment problem. Regarding arriving on time, it is formulated based on the probability tail model, which aims to …
Inferring Social Media Users’ Demographics From Profile Pictures: A Face++ Analysis On Twitter Users, Soon-Gyo Jung, Jisun An, Haewoon Kwak, Joni Salminen, Bernard J. Jansen
Inferring Social Media Users’ Demographics From Profile Pictures: A Face++ Analysis On Twitter Users, Soon-Gyo Jung, Jisun An, Haewoon Kwak, Joni Salminen, Bernard J. Jansen
Research Collection School Of Computing and Information Systems
In this research, we evaluate the applicability of using facial recognition of social media account profile pictures to infer the demographic attributes of gender, race, and age of the account owners leveraging a commercial and well-known image service, specifically Face++. Our goal is to determine the feasibility of this approach for actual system implementation. Using a dataset of approximately 10,000 Twitter profile pictures, we use Face++ to classify this set of images for gender, race, and age. We determine that about 30% of these profile pictures contain identifiable images of people using the current state-of-the-art automated means. We then employ …
A Novel Density Peak Clustering Algorithm Based On Squared Residual Error, Milan Parmar, Di Wang, Ah-Hwee Tan, Chunyan Miao, Jianhua Jiang, You Zhou
A Novel Density Peak Clustering Algorithm Based On Squared Residual Error, Milan Parmar, Di Wang, Ah-Hwee Tan, Chunyan Miao, Jianhua Jiang, You Zhou
Research Collection School Of Computing and Information Systems
The density peak clustering (DPC) algorithm is designed to quickly identify intricate-shaped clusters with high dimensionality by finding high-density peaks in a non-iterative manner and using only one threshold parameter. However, DPC has certain limitations in processing low-density data points because it only takes the global data density distribution into account. As such, DPC may confine in forming low-density data clusters, or in other words, DPC may fail in detecting anomalies and borderline points. In this paper, we analyze the limitations of DPC and propose a novel density peak clustering algorithm to better handle low-density clustering tasks. Specifically, our algorithm …
Learning Likely Invariants To Explain Why A Program Fails, Long H. Pham, Jun Sun, Lyly Tran Thi, Jingyi Wang, Xin Peng
Learning Likely Invariants To Explain Why A Program Fails, Long H. Pham, Jun Sun, Lyly Tran Thi, Jingyi Wang, Xin Peng
Research Collection School Of Computing and Information Systems
Debugging is difficult. Recent studies show that automatic bug localization techniques have limited usefulness. One of the reasons is that programmers typically have to understand why the program fails before fixing it. In this work, we aim to help programmers understand a bug by automatically generating likely invariants which are violated in the failed tests. Given a program with an initial assertion and at least one test case failing the assertion, we first generate random test cases, identify potential bug locations through bug localization, and then generate program state mutation based on active learning techniques to identify a predicate 'explaining' …
Automatic Loop-Invariant Generation And Refinement Through Selective Sampling, Jiaying Li, Jun Sun, Li Li, Quang Loc Le, Shang-Wei Lin
Automatic Loop-Invariant Generation And Refinement Through Selective Sampling, Jiaying Li, Jun Sun, Li Li, Quang Loc Le, Shang-Wei Lin
Research Collection School Of Computing and Information Systems
Automatic loop-invariant generation is important in program analysis and verification. In this paper, we propose to generate loop-invariants automatically through learning and verification. Given a Hoare triple of a program containing a loop, we start with randomly testing the program, collect program states at run-time and categorize them based on whether they satisfy the invariant to be discovered. Next, classification techniques are employed to generate a candidate loop-invariant automatically. Afterwards, we refine the candidate through selective sampling so as to overcome the lack of sufficient test cases. Only after a candidate invariant cannot be improved further through selective sampling, we …
Fib: Squeezing Loop Invariants By Interpolation Between Forward/Backward Predicate Transformers, Shang-Wei Lin, Jun Sun, Hao Xiao, Yang Liu, David Sana, Henri Hansen
Fib: Squeezing Loop Invariants By Interpolation Between Forward/Backward Predicate Transformers, Shang-Wei Lin, Jun Sun, Hao Xiao, Yang Liu, David Sana, Henri Hansen
Research Collection School Of Computing and Information Systems
Loop invariant generation is a fundamental problem in program analysis and verification. In this work, we propose a new approach to automatically constructing inductive loop invariants. The key idea is to aggressively squeeze an inductive invariant based on Craig interpolants between forward and backward reachability analysis. We have evaluated our approach by a set of loop benchmarks, and experimental results show that our approach is promising.
Detecting Semantic Uncertainty By Learning Hedge Cues In Sentences Using An Hmm, Xiujun Li, Wei Gao, Jude Shavlik
Detecting Semantic Uncertainty By Learning Hedge Cues In Sentences Using An Hmm, Xiujun Li, Wei Gao, Jude Shavlik
Research Collection School Of Computing and Information Systems
Detecting speculative assertions is essential to distinguish semantically uncertain information from the factual ones in text. This is critical to the trustworthiness of many intelligent systems that are based on information retrieval and natural language processing techniques, such as question answering or information extraction. We empirically explore three fundamental issues of uncertainty detection: (1) the predictive ability of different learning methods on this task; (2) whether using unlabeled data can lead to a more accurate model; and (3) whether closed-domain training or crossdomain training is better. For these purposes, we adopt two statistical learning approaches to this problem: the commonly …
Classification-Based Parameter Synthesis For Parametric Timed Automata, Jiaying Li, Jun Sun, Bo Gao, Étienne Andre
Classification-Based Parameter Synthesis For Parametric Timed Automata, Jiaying Li, Jun Sun, Bo Gao, Étienne Andre
Research Collection School Of Computing and Information Systems
Parametric timed automata are designed to model timed systems with unknown parameters, often representing design uncertainties of external environments. In order to design a robust system, it is crucial to synthesize constraints on the parameters, which guarantee the system behaves according to certain properties. Existing approaches suffer from scalability issues. In this work, we propose to enhance existing approaches through classification-based learning. We sample multiple concrete values for parameters and model check the corresponding non-parametric models. Based on the checking results, we form conjectures on the constraint through classification techniques, which can be subsequently confirmed by existing model checkers for …