Open Access. Powered by Scholars. Published by Universities.®
- Institution
-
- Singapore Management University (46)
- University of Dayton (19)
- California Polytechnic State University, San Luis Obispo (11)
- Old Dominion University (7)
- University of Arkansas, Fayetteville (6)
-
- University of Nevada, Las Vegas (6)
- California State University, San Bernardino (4)
- City University of New York (CUNY) (4)
- Southern Adventist University (4)
- University of Malaya (4)
- Western University (4)
- Claremont Colleges (3)
- Edith Cowan University (3)
- Georgia Southern University (3)
- LSU New Orleans (3)
- Montclair State University (3)
- San Jose State University (3)
- Southern Methodist University (3)
- University of New Mexico (3)
- Virginia Commonwealth University (3)
- Columbus State University (2)
- East Tennessee State University (2)
- Florida Institute of Technology (2)
- Liberty University (2)
- Purdue University (2)
- The University of Akron (2)
- The University of Southern Mississippi (2)
- University of Kentucky (2)
- University of Louisville (2)
- University of Missouri, St. Louis (2)
- Keyword
-
- Algorithms (10)
- Machine Learning (9)
- Machine learning (7)
- Computer Science (6)
- Algorithm (5)
-
- Computer science (5)
- Deep Learning (5)
- Artificial Intelligence (4)
- Clustering (4)
- Genetic Algorithm (4)
- Python (4)
- Software engineering (4)
- Android (3)
- Classification (3)
- Quantum Computing (3)
- Verification (3)
- Visualization (3)
- Artificial intelligence (2)
- Bioinformatics (2)
- Computer (2)
- Computer Vision (2)
- Computer vision (2)
- Convolutional neural network (2)
- Cybersecurity (2)
- Data mining (2)
- Data science (2)
- Deep learning (2)
- Deep learning testing (2)
- Deep neural networks (2)
- Delay (2)
- Publication Year
- Publication
-
- Research Collection School Of Computing and Information Systems (45)
- Computer Science Faculty Publications (23)
- Theses and Dissertations (7)
- Electronic Theses and Dissertations (5)
- Master's Theses (5)
-
- Computer Science and Computer Engineering Undergraduate Honors Theses (4)
- Electrical and Computer Engineering Publications (4)
- Computer Engineering (3)
- Computer Science and Engineering Theses and Dissertations (3)
- Department of Computer Science Faculty Scholarship and Creative Works (3)
- Dissertations (3)
- Electronic Theses, Projects, and Dissertations (3)
- LSU New Orleans Theses and Dissertations (3)
- Student Works (2000-2009) (3)
- UNLV Theses, Dissertations, Professional Papers, and Capstones (3)
- CMC Senior Theses (2)
- Campus Research Month (2)
- College of Engineering: Graduate Celebration Programs (2)
- Computer Science ETDs (2)
- Honors College Theses (2)
- Publications and Research (2)
- Senior Honors Theses (2)
- The Summer Undergraduate Research Fellowship (SURF) Symposium (2)
- Theses : Honours (2)
- Theses and Dissertations (Comprehensive) (2)
- Theses and Dissertations--Computer Science (2)
- Williams Honors College, Honors Research Projects (2)
- 2010 Annual Nevada NSF EPSCoR Climate Change Conference (1)
- All Dissertations (1)
- All Master's Theses (1)
- Publication Type
Articles 91 - 120 of 204
Full-Text Articles in Software Engineering
Suitability Of Finite State Automata To Model String Constraints In Probablistic Symbolic Execution, Andrew Harris
Suitability Of Finite State Automata To Model String Constraints In Probablistic Symbolic Execution, Andrew Harris
Boise State University Theses and Dissertations
Probabilistic Symbolic Execution (PSE) extends Symbolic Execution (SE), a path-sensitive static program analysis technique, by calculating the probabilities with which program paths are executed. PSE relies on the ability of the underlying symbolic models to accurately represent the execution paths of the program as the collection of input values following these paths. While researchers established PSE for numerical data types, PSE for complex data types such as strings is a novel area of research.
For string data types SE tools commonly utilize finite state automata to represent a symbolic string model. Thus, PSE inherits from SE automata-based symbolic string models …
Redpc: A Residual Error-Based Density Peak Clustering Algorithm, Milan Parmar, Di Wang, Xiaofeng Zhang, Ah-Hwee Tan, Chunyan Miao, You Zhou
Redpc: A Residual Error-Based Density Peak Clustering Algorithm, Milan Parmar, Di Wang, Xiaofeng Zhang, Ah-Hwee Tan, Chunyan Miao, You Zhou
Research Collection School Of Computing and Information Systems
The density peak clustering (DPC) algorithm was designed to identify arbitrary-shaped clusters by finding density peaks in the underlying dataset. Due to its aptitudes of relatively low computational complexity and a small number of control parameters in use, DPC soon became widely adopted. However, because DPC takes the entire data space into consideration during the computation of local density, which is then used to generate a decision graph for the identification of cluster centroids, DPC may face difficulty in differentiating overlapping clusters and in dealing with low-density data points. In this paper, we propose a residual error-based density peak clustering …
Building Consumer Trust In The Cloud: An Experimental Analysis Of The Cloud Trust Label Approach, Lisa Van Der Werff, Grace Fox, Ieva Masevic, Vincent C. Emeakaroha, John P. Morrison, Theo Lynn
Building Consumer Trust In The Cloud: An Experimental Analysis Of The Cloud Trust Label Approach, Lisa Van Der Werff, Grace Fox, Ieva Masevic, Vincent C. Emeakaroha, John P. Morrison, Theo Lynn
Department of Computer Science Publications
The lack of transparency surrounding cloud service provision makes it difficult for consumers to make knowledge based purchasing decisions. As a result, consumer trust has become a major impediment to cloud computing adoption. Cloud Trust Labels represent a means of communicating relevant service and security information to potential customers on the cloud service provided, thereby facilitating informed decision making. This research investigates the potential of a Cloud Trust Label system to overcome the trust barrier. Specifically, it examines the impact of a Cloud Trust Label on consumer perceptions of a service and cloud service provider trustworthiness and trust in the …
The Effect Of Modeling Simultaneous Events On Simulation Results, John M. Carboni
The Effect Of Modeling Simultaneous Events On Simulation Results, John M. Carboni
Theses and Dissertations
This thesis explores the method that governs the prioritizing process for simultaneous events in relation to simulation results for discrete-event simulations. Specifically, it contrasts typical discrete-event simulation (DES) execution algorithms with how events are selected and ordered by the discrete-event system specification (DEVS) formalism. The motivation for this research stems from a desire to understand how the selection of events affects simulation output (i.e., response). As a particular use case, we briefly investigate the processing of simultaneous events by the Advanced Framework for Simulation, Integration and Modeling (AFSIM), a military discrete-event combat modeling and simulation package. To facilitate the building …
Quantum Computing Is Here To Stay, Manoj Thulasidas
Quantum Computing Is Here To Stay, Manoj Thulasidas
MITB Thought Leadership Series
QUANTUM COMPUTING is emerging from university laboratories and entering the industry arena at a painfully slow pace. The measured and deliberate progress is understandable given its complexity and promise. The stakes are high, because quantum computing presents the tantalising prospect of solving problems previously considered completely insoluble
Dish: Democracy In State Houses, Nicholas A. Russo
Dish: Democracy In State Houses, Nicholas A. Russo
Master's Theses
In our current political climate, state level legislators have become increasingly impor- tant. Due to cuts in funding and growing focus at the national level, public oversight for these legislators has drastically decreased. This makes it difficult for citizens and activists to understand the relationships and commonalities between legislators. This thesis provides three contributions to address this issue. First, we created a data set containing over 1200 features focused on a legislator’s activity on bills. Second, we created embeddings that represented a legislator’s level of activity and engagement for a given bill using a custom model called Democracy2Vec. Third, we …
Bilateral Dependency Neural Networks For Cross-Language Algorithm Classification, Duy Quoc Nghi Bui, Yijun Yu, Lingxiao Jiang
Bilateral Dependency Neural Networks For Cross-Language Algorithm Classification, Duy Quoc Nghi Bui, Yijun Yu, Lingxiao Jiang
Research Collection School Of Computing and Information Systems
Algorithm classification is to automatically identify the classes of a program based on the algorithm(s) and/or data structure(s) implemented in the program. It can be useful for various tasks, such as code reuse, code theft detection, and malware detection. Code similarity metrics, on the basis of features extracted from syntax and semantics, have been used to classify programs. Such features, however, often need manual selection effort and are specific to individual programming languages, limiting the classifiers to programs in the same language.To recognise the similarities and differences among algorithms implemented in different languages, this paper describes a framework of Bilateral …
A Machine Learning Recommender Model For Ride Sharing Based On Rider Characteristics And User Threshold Time, Govind Pramod Yatnalkar
A Machine Learning Recommender Model For Ride Sharing Based On Rider Characteristics And User Threshold Time, Govind Pramod Yatnalkar
Theses, Dissertations and Capstones
In the present age, human life is prospering incredibly due to the 4th Industrial Revolution or The Age of Digitization and Computing. The ubiquitous availability of the Internet and advanced computing systems have resulted in the rapid development of smart cities. From connected devices to live vehicle tracking, technology is taking the field of transportation to a new level. An essential part of the transportation domain in smart cities is Ride Sharing. It is an excellent solution to issues like pollution, traffic, and the rapid consumption of fuel. Even though Ride Sharing has several benefits, the current usage is …
Learning To Map The Visual And Auditory World, Tawfiq Salem
Learning To Map The Visual And Auditory World, Tawfiq Salem
Theses and Dissertations--Computer Science
The appearance of the world varies dramatically not only from place to place but also from hour to hour and month to month. Billions of images that capture this complex relationship are uploaded to social-media websites every day and often are associated with precise time and location metadata. This rich source of data can be beneficial to improve our understanding of the globe. In this work, we propose a general framework that uses these publicly available images for constructing dense maps of different ground-level attributes from overhead imagery. In particular, we use well-defined probabilistic models and a weakly-supervised, multi-task training …
Building Recommendation Systems, Orion Davis
Building Recommendation Systems, Orion Davis
Williams Honors College, Honors Research Projects
Recommendation systems are pieces of software that suggest new items to a user. There are many moving parts to these systems including data, the actual recommendation model, processing data and finally displaying data. This project explores the role each part plays in the overall system and how to develop a recommendation system for beer from scratch. This project highlights the algorithm behind the recommendations and a user facing Android application.
Criticality Assessments For Improving Algorithmic Robustness, Thomas B. Jones
Criticality Assessments For Improving Algorithmic Robustness, Thomas B. Jones
Computer Science ETDs
Though computational models typically assume all program steps execute flawlessly, that does not imply all steps are equally important if a failure should occur. In the "Constrained Reliability Allocation" problem, sufficient resources are guaranteed for operations that prompt eventual program termination on failure, but those operations that only cause output errors are given a limited budget of some vital resource, insufficient to ensure correct operation for each of them.
In this dissertation, I present a novel representation of failures based on a combination of their timing and location combined with criticality assessments---a method used to predict the behavior of systems …
Using Finite-State Models For Log Differencing, Hen Amar, Lingfeng Bao, Nimrod Busany, David Lo, Shahar Maoz
Using Finite-State Models For Log Differencing, Hen Amar, Lingfeng Bao, Nimrod Busany, David Lo, Shahar Maoz
Research Collection School Of Computing and Information Systems
Much work has been published on extracting various kinds of models from logs that document the execution of running systems. In many cases, however, for example in the context of evolution, testing, or malware analysis, engineers are interested not only in a single log but in a set of several logs, each of which originated from a different set of runs of the system at hand. Then, the difference between the logs is the main target of interest. In this work we investigate the use of finite-state models for log differencing. Rather than comparing the logs directly, we generate concise …
On The Sequential Massart Algorithm For Statistical Model Checking, Cyrille Jegourel, Jun Sun, Jin Song Dong
On The Sequential Massart Algorithm For Statistical Model Checking, Cyrille Jegourel, Jun Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
Several schemes have been provided in Statistical Model Checking (SMC) for the estimation of property occurrence based on predefined confidence and absolute or relative error. Simulations might be however costly if many samples are required and the usual algorithms implemented in statistical model checkers tend to be conservative. Bayesian and rare event techniques can be used to reduce the sample size but they can not be applied without prerequisite or knowledge about the system under scrutiny. Recently, sequential algorithms based on Monte Carlo estimations and Massart bounds have been proposed to reduce the sample size while providing guarantees on error …
List, Sample, And Count, Ali Assarpour
List, Sample, And Count, Ali Assarpour
Dissertations, Theses, and Capstone Projects
Counting plays a fundamental role in many scientific fields including chemistry, physics, mathematics, and computer science. There are two approaches for counting, the first relies on analytical tools to drive closed form expression, while the second takes advantage of the combinatorial nature of the problem to construct an algorithm whose output is the number of structures. There are many algorithmic techniques for counting, they cover the explicit approach of counting by listing to the approximate approach of counting by sampling.
This thesis looks at counting three sets of objects. First, we consider a subclass of boolean functions that are monotone. …
An Algorithmic Approach To Creating Effective Study Groups Using A Smart Phone App, Kelvin J. Rosado-Ayala
An Algorithmic Approach To Creating Effective Study Groups Using A Smart Phone App, Kelvin J. Rosado-Ayala
Honors College Theses
For many students entering college, meeting new people and studying are a common struggle. Study groups are generally recommended, especially if the groups are comprised of members with complementary personality traits. But the challenge still remains, how do freshmen or transfer students find and form these heterogeneous study groups. In order to help alleviate this issue, an Android application was developed to automatically create study groups for students. Using basic information provided by students upon registration, the algorithm is able to automatically find matching group members. The application was designed using an agile life cycle model over the course of …
Funqual: User-Defined, Statically-Checked Call Graph Constraints In C++, Andrew P. Nelson
Funqual: User-Defined, Statically-Checked Call Graph Constraints In C++, Andrew P. Nelson
Master's Theses
Static analysis tools can aid programmers by reporting potential programming mistakes prior to the execution of a program. Funqual is a static analysis tool that reads C++17 code ``in the wild'' and checks that the function call graph follows a set of rules which can be defined by the user. This sort of analysis can help the programmer to avoid errors such as accidentally calling blocking functions in time-sensitive contexts or accidentally allocating memory in heap-sensitive environments. To accomplish this, we create a type system whereby functions can be given user-defined type qualifiers and where users can define their own …
The Effect Of Endgame Tablebases On Modern Chess Engines, Christopher D. Peterson
The Effect Of Endgame Tablebases On Modern Chess Engines, Christopher D. Peterson
Computer Engineering
Modern chess engines have the ability to augment their evaluation by using massive tables containing billions of positions and their memorized solutions. This report examines the importance of these tables to better understand the circumstances under which they should be used. The analysis conducted in this paper empirically examines differences in size and speed of memorized positions and their impacts on engine strength. Using this technique, situations where memorized tables improve play (and situations where they do not) are discovered.
Understanding Natural Keyboard Typing Using Convolutional Neural Networks On Mobile Sensor Data, Travis Siems
Understanding Natural Keyboard Typing Using Convolutional Neural Networks On Mobile Sensor Data, Travis Siems
Computer Science and Engineering Theses and Dissertations
Mobile phones and other devices with embedded sensors are becoming increasingly ubiquitous. Audio and motion sensor data may be able to detect information that we did not think possible. Some researchers have created models that can predict computer keyboard typing from a nearby mobile device; however, certain limitations to their experiment setup and methods compelled us to be skeptical of the models’ realistic prediction capability. We investigate the possibility of understanding natural keyboard typing from mobile phones by performing a well-designed data collection experiment that encourages natural typing and interactions. This data collection helps capture realistic vulnerabilities of the security …
Cora: Commingled Remains And Analytics – An Open Community Ecosystem, Nicole Mcelroy, Ryan Ernst
Cora: Commingled Remains And Analytics – An Open Community Ecosystem, Nicole Mcelroy, Ryan Ernst
UNO Student Research and Creative Activity Fair
Anthropologists at organizations such as the DPAA (Defense POW/MIA Accounting Agency) have the tough job of sorting through commingled remains of fallen soldiers. Under the direction of Professor Pawaskar at the College of IS&T, Ryan Ernst and I are currently developing a web application for the DPAA that will help them inventory the bones and record all the appropriate associations. After the inventory web application is built we will begin the analysis process using graph theory and other mathematical algorithms. This will ultimately help organizations like the DPAA get closer to the end goal of identifying fallen soldiers from commingled …
Cross-Language Learning For Program Classification Using Bilateral Tree-Based Convolutional Neural Networks, Duy Quoc Nghi Bui, Lingxiao Jiang, Yijun Yu
Cross-Language Learning For Program Classification Using Bilateral Tree-Based Convolutional Neural Networks, Duy Quoc Nghi Bui, Lingxiao Jiang, Yijun Yu
Research Collection School Of Computing and Information Systems
Towards the vision of translating code that implements an algorithm from one programming language into another, this paper proposes an approach for automated program classification using bilateral tree-based convolutional neural networks (BiTBCNNs). It is layered on top of two tree-based convolutional neural networks (TBCNNs), each of which recognizes the algorithm of code written in an individual programming language. The combination layer of the networks recognizes the similarities and differences among code in different programming languages. The BiTBCNNs are trained using the source code in different languages but known to implement the same algorithms and/or functionalities. For a preliminary evaluation, we …
An Iterated Local Search Algorithm For The Team Orienteering Problem With Variable Profits, Aldy Gunawan, Kien Ming Ng, Graham Kendall, Junhan Lai
An Iterated Local Search Algorithm For The Team Orienteering Problem With Variable Profits, Aldy Gunawan, Kien Ming Ng, Graham Kendall, Junhan Lai
Research Collection School Of Computing and Information Systems
The orienteering problem (OP) is a routing problem that has numerous applications in various domains such as logistics and tourism. The objective is to determine a subset of vertices to visit for a vehicle so that the total collected score is maximized and a given time budget is not exceeded. The extensive application of the OP has led to many different variants, including the team orienteering problem (TOP) and the team orienteering problem with time windows. The TOP extends the OP by considering multiple vehicles. In this article, the team orienteering problem with variable profits (TOPVP) is studied. The main …
Logic -> Proof -> Rest, Maxwell Taylor
Logic -> Proof -> Rest, Maxwell Taylor
Senior Independent Study Theses
REST is a common architecture for networked applications. Applications that adhere to the REST constraints enjoy significant scaling advantages over other architectures. But REST is not a panacea for the task of building correct software. Algebraic models of computation, particularly CSP, prove useful to describe the composition of applications using REST. CSP enables us to describe and verify the behavior of RESTful systems. The descriptions of each component can be used independently to verify that a system behaves as expected. This thesis demonstrates and develops CSP methodology to verify the behavior of RESTful applications.
Process Models Discovery And Traces Classification: A Fuzzy-Bpmn Mining Approach., Kingsley Okoye Dr, Usman Naeem Dr, Syed Islam Dr, Abdel-Rahman H. Tawil Dr, Elyes Lamine Dr
Process Models Discovery And Traces Classification: A Fuzzy-Bpmn Mining Approach., Kingsley Okoye Dr, Usman Naeem Dr, Syed Islam Dr, Abdel-Rahman H. Tawil Dr, Elyes Lamine Dr
Journal of International Technology and Information Management
The discovery of useful or worthwhile process models must be performed with due regards to the transformation that needs to be achieved. The blend of the data representations (i.e data mining) and process modelling methods, often allied to the field of Process Mining (PM), has proven to be effective in the process analysis of the event logs readily available in many organisations information systems. Moreover, the Process Discovery has been lately seen as the most important and most visible intellectual challenge related to the process mining. The method involves automatic construction of process models from event logs about any domain …
Design And Implementation Of A Stand-Alone Tool For Metabolic Simulations, Milad Ghiasi Rad
Design And Implementation Of A Stand-Alone Tool For Metabolic Simulations, Milad Ghiasi Rad
School of Computing: Dissertations, Theses, and Student Research
In this thesis, we present the design and implementation of a stand-alone tool for metabolic simulations. This system is able to integrate custom-built SBML models along with external user’s input information and produces the estimation of any reactants participating in the chain of the reactions in the provided model, e.g., ATP, Glucose, Insulin, for the given duration using numerical analysis and simulations. This tool offers the food intake arguments in the calculations to consider the personalized metabolic characteristics in the simulations. The tool has also been generalized to take into consideration of temporal genomic information and be flexible for simulation …
Web Application For Graduate Course Recommendation System, Sayali Dhumal
Web Application For Graduate Course Recommendation System, Sayali Dhumal
Electronic Theses, Projects, and Dissertations
The main aim of the course advising system is to build a course recommendation path for students to help them plan courses to successfully graduate on time. The recommendation path displays the list of courses a student can take in each quarter from the first quarter after admission until the graduation quarter. The courses are filtered as per the student’s interest obtained from a questionnaire asked to the student.
The business logic involves building the recommendation algorithm. Also, the application is functionality-tested end-to-end by using nightwatch.js which is built on top of node.js. Test cases are written for every module …
Web Application For Graduate Course Advising System, Sanjay Karrolla
Web Application For Graduate Course Advising System, Sanjay Karrolla
Electronic Theses, Projects, and Dissertations
The main aim of the course recommendation system is to build a course recommendation path for students to help them plan courses to successfully graduate on time. The Model-View-Controller (MVC) architecture is used to isolate the user interface (UI) design from the business logic. The front-end of the application develops the UI using AngularJS. The front-end design is done by gathering the functionality system requirements -- input controls, navigational components, informational components and containers and usability testing. The back-end of the application involves setting up the database and server-side routing. Server-side routing is done using Express JS.
File-Level Defect Prediction: Unsupervised Vs. Supervised Models, Meng Yan, Yicheng Fang, David Lo, Xin Xia, Xiaohong Zhang
File-Level Defect Prediction: Unsupervised Vs. Supervised Models, Meng Yan, Yicheng Fang, David Lo, Xin Xia, Xiaohong Zhang
Research Collection School Of Computing and Information Systems
Background: Software defect models can help software quality assurance teams to allocate testing or code review resources. A variety of techniques have been used to build defect prediction models, including supervised and unsupervised methods. Recently, Yang et al. [1] surprisingly find that unsupervised models can perform statistically significantly better than supervised models in effort-aware change-level defect prediction. However, little is known about relative performance of unsupervised and supervised models for effort-aware file-level defect prediction. Goal: Inspired by their work, we aim to investigate whether a similar finding holds in effort-aware file-level defect prediction. Method: We replicate Yang et al.'s study …
Ancr—An Adaptive Network Coding Routing Scheme For Wsns With Different-Success-Rate Links †, Xiang Ji, Anwen Wang, Chunyu Li, Chun Ma, Yao Peng, Dajin Wang, Qingyi Hua, Feng Chen, Dingyi Fang
Ancr—An Adaptive Network Coding Routing Scheme For Wsns With Different-Success-Rate Links †, Xiang Ji, Anwen Wang, Chunyu Li, Chun Ma, Yao Peng, Dajin Wang, Qingyi Hua, Feng Chen, Dingyi Fang
Department of Computer Science Faculty Scholarship and Creative Works
As the underlying infrastructure of the Internet of Things (IoT), wireless sensor networks (WSNs) have been widely used in many applications. Network coding is a technique in WSNs to combine multiple channels of data in one transmission, wherever possible, to save node’s energy as well as increase the network throughput. So far most works on network coding are based on two assumptions to determine coding opportunities: (1) All the links in the network have the same transmission success rate; (2) Each link is bidirectional, and has the same transmission success rate on both ways. However, these assumptions may not be …
Parallelization Of Molecular Docking Algorithms Using Cuda For Use In Drug Discovery, Brandon Stewart, Jonathan Fine, Gaurav Chopra Phd
Parallelization Of Molecular Docking Algorithms Using Cuda For Use In Drug Discovery, Brandon Stewart, Jonathan Fine, Gaurav Chopra Phd
The Summer Undergraduate Research Fellowship (SURF) Symposium
Traditional drug discovery methodology uses a multitude of software packages to design and evaluate new drug-like compounds. While software packages implement a wide variety of methods, the serial (i.e. single core) implementation for many of these algorithms, prohibit large scale docking, such as proteome-wide docking (i.e. thousands of compounds with thousands of proteins). Several docking algorithms can be parallelized, significantly reducing the runtime of the calculations, thus enabling large-scale docking. Implementing algorithms that take advantage of the distributed nature of graphical processing units (GPUs) via the Compute Unified Device Architecture (CUDA) enables us to efficiently implement massively parallel algorithms. Two …
A Decidable Fragment In Separation Logic With Inductive Predicates And Arithmetic, Quang Loc Le, Makoto Tatsuta, Jun Sun, Wei-Ngan Chin
A Decidable Fragment In Separation Logic With Inductive Predicates And Arithmetic, Quang Loc Le, Makoto Tatsuta, Jun Sun, Wei-Ngan Chin
Research Collection School Of Computing and Information Systems
We consider the satisfiability problem for a fragment of separation logic including inductive predicates with shape and arithmetic properties. We show that the fragment is decidable if the arithmetic properties can be represented as semilinear sets. Our decision procedure is based on a novel algorithm to infer a finite representation for each inductive predicate which precisely characterises its satisfiability. Our analysis shows that the proposed algorithm runs in exponential time in the worst case. We have implemented our decision procedure and integrated it into an existing verification system. Our experiment on benchmarks shows that our procedure helps to verify the …