Programming Languages and Compilers Commons^™

Introducing Non-Determinism To The Parallel C Compiler, Rowen Concepcion

Electronic Theses, Projects, and Dissertations

The Planguages project is the birthplace of the Planguage programming
approach, which is designed to alleviate the task of writing parallel
programs and harness massively parallel computers and networks of workstations.

Planguage has two existing translators, Parallel C (PC) and Pfortran,
which is used for their base languages, C and Fortran77. The translators
work with MPI (Message Passing Interface) for communications. SOS
(ipStreams, Overlapping and Shortcutting), a function library that supports
the three named functionalities, can be used to further optimize parallel algorithms.

This project is the next step in the continuing project of updating
the PC Compiler. The goal …

Scc-Based Improved Reachability Analysis For Markov Decision Processes, Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong

Research Collection School Of Computing and Information Systems

Markov decision processes (MDPs) are extensively used to model systems with both probabilistic and nondeterministic behavior. The problem of calculating the probability of reaching certain system states (hereafter reachability analysis) is central to the MDP-based system analysis. It is known that existing approaches on reachability analysis for MDPs are often inefficient when a given MDP contains a large number of states and loops, especially with the existence of multiple probability distributions. In this work, we propose a method to eliminate strongly connected components (SCCs) in an MDP using a divide-and-conquer algorithm, and actively remove redundant probability distributions in the MDP …

Exploring Computer Science: Coding Can Be Fun, Peter Brown, Travis Dalton, Tori Myers

Arthur Vining Davis High Impact Fellows Projects

The focus of this project is to adopt a course/curriculum that builds interest in computer science and appeals to high school students through a variety of programs and activities. One of our goals is to increase interest in computer science among high school students especially minority and female students. Students will learn how to use programming languages, utilize higher level problem solving and program robots using the skills they acquired. The course, Exploring Computer Science, gives students the opportunity to learn a variety of computer science topics and have fun doing it.

Writing Self-Testing Java Classes With Selftest, Yoonsik Cheon

Departmental Technical Reports (CS)

This document provides a tutorial introduction to Java annotations called SelfTest. The SelfTest annotations allow one to annotate Java classes with test data, and the SelfTest annotation processor generates executable JUnit test classes from annotated Java classes by translating test cases to executable JUnit tests. The SelfTest annotations not only automate unit testing of Java classes significantly but also provides a step toward writing self-testing Java classes by embedding test data in source code for both compile and runtime processing.

Automatic Objects Removal For Scene Completion, Jianjun Yang, Yin Wang, Honggang Wang, Kun Hua, Wei Wang, Ju Shen

Computer Science Faculty Publications

With the explosive growth of Web-based cameras and mobile devices, billions of photographs are uploaded to the Internet. We can trivially collect a huge number of photo streams for various goals, such as 3D scene reconstruction and other big data applications. However, this is not an easy task due to the fact the retrieved photos are neither aligned nor calibrated. Furthermore, with the occlusion of unexpected foreground objects like people, vehicles, it is even more challenging to find feature correspondences and reconstruct realistic scenes. In this paper, we propose a structure-based image completion algorithm for object removal that produces visually …

Conception, Design And Construction Of A Remote Wifi Vehicle Using Arduino, Clayton Broman

Physics

The scope of this senior project was to make a wireless vehicle controlled via Internet Protocol. This vehicle operates remotely and without direct line of sight. Commands are sent from a program running on a laptop and transmitted using a wireless router. Visual data is retrieved from a network camera, mounted on the vehicle, in real-time, to see where you are going.

Teaching Tip: The Flipped Classroom, Heng Ngee Mok

Research Collection School Of Computing and Information Systems

The flipped classroom has been gaining popularity in recent years. In theory, flipping the classroom appears sound: passive learning activities such as unidirectional lectures are pushed to outside class hours in the form of videos, and precious class time is spent on active learning activities. Yet the courses for information systems (IS) undergraduates at the university that the author is teaching at are still conducted in the traditional lecture-in-class, homework-after-class style. In order to increase students’ engagement with the course content and to improve their experience with the course, the author implemented a trial of the flipped classroom model for …

Unstructured P2p Link Lifetimes Redux, Zhongmei Yao, Daren B. H. Cline

Computer Science Faculty Publications

We revisit link lifetimes in random P2P graphs under dynamic node failure and create a unifying stochastic model that generalizes the majority of previous efforts in this direction. We not only allow nonexponential user lifetimes and age-dependent neighbor selection, but also cover both active and passive neighbor-management strategies, model the lifetimes of incoming and outgoing links, derive churn-related message volume of the system, and obtain the distribution of transient in/out degree at each user. We then discuss the impact of design parameters on overhead and resilience of the network.

Visual Typo Correction By Collocative Optimization: A Case Study On Merchandize Images, Xiao-Yong Wei, Zhen-Qun Yang, Chong-Wah Ngo, Wei Zhang

Research Collection School Of Computing and Information Systems

Near-duplicate retrieval (NDR) in merchandize images is of great importance to a lot of online applications on e-Commerce websites. In those applications where the requirement of response time is critical, however, the conventional techniques developed for a general purpose NDR are limited, because expensive post-processing like spatial verification or hashing is usually employed to compromise the quantization errors among the visual words used for the images. In this paper, we argue that most of the errors are introduced because of the quantization process where the visual words are considered individually, which has ignored the contextual relations among words. We propose …

Identity Based Identification From Algebraic Coding Theory, Guomin Yang, Chik How Tan, Yi Mu, Willy Susilo, Duncan S. Wong

Research Collection School Of Computing and Information Systems

Cryptographic identification schemes allow a remote user to prove his/her identity to a verifier who holds some public information of the user, such as the user public key or identity. Most of the existing cryptographic identification schemes are based on numbertheoretic hard problems such as Discrete Log and Factorization. This paper focuses on the design and analysis of identity based identification (IBI) schemes based on algebraic coding theory. We first revisit an existing code-based IBI scheme which is derived by combining the Courtois–Finiasz–Sendrier signature scheme and the Stern zero-knowledge identification scheme. Previous results have shown that this IBI scheme is …

Parameter Synthesis For Hierarchical Concurrent Real-Time Systems, Étienne André, Yang Liu, Jun Sun, Jin Song Dong

Research Collection School Of Computing and Information Systems

Modeling and verifying complex real-time systems, involving timing delays, are notoriously difficult problems. Checking the correctness of a system for one particular value for each delay does not give any information for other values. It is thus interesting to reason parametrically, by considering that the delays are parameters (unknown constants) and synthesizing a constraint guaranteeing a correct behavior. We present here Parametric Stateful Timed Communicating Sequential Processes, a language capable of specifying and verifying parametric hierarchical real-time systems with complex data structures. Although we prove that the synthesis is undecidable in general, we present several semi-algorithms for efficient parameter synthesis, …

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 …

Model Checking Approach To Automated Planning, Yi Li, Jin Song Dong, Jing Sun, Yang Liu, Jun Sun

Research Collection School Of Computing and Information Systems

Model checking provides a way to automatically explore the state space of a finite state system based on desired properties, whereas planning is to produce a sequence of actions that leads from the initial state to the target goal states. Previous research in this field proposed a number of approaches for connecting model checking with planning problem solving. In this paper, we investigate the feasibility of using an established model checking framework, Process Analysis Toolkit (PAT), as a planning solution provider for upper layer applications. To achieve this, we first carry out a number of experiments on different model checking …

Learning Assumptions For Compositional Verification Of Timed Systems, Shang-Wei Lin Lin, Yang Liu, Jun Sun, Jun Sun

Research Collection School Of Computing and Information Systems

Compositional techniques such as assume-guarantee reasoning (AGR) can help to alleviate the state space explosion problem associated with model checking. However, compositional verification is difficult to be automated, especially for timed systems, because constructing appropriate assumptions for AGR usually requires human creativity and experience. To automate compositional verification of timed systems, we propose a compositional verification framework using a learning algorithm for automatic construction of timed assumptions for AGR. We prove the correctness and termination of the proposed learning-based framework, and experimental results show that our method performs significantly better than traditional monolithic timed model checking.

Closed Type Families With Overlapping Equations, Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, Stephanie Weirich

Computer Science Faculty Research and Scholarship

Open, type-level functions are a recent innovation in Haskell that move Haskell towards the expressiveness of dependent types, while retaining the look and feel of a practical programming language. This paper shows how to increase expressiveness still further, by adding closed type functions whose equations may overlap, and may have non-linear patterns over an open type universe. Although practically useful and simple to implement, these features go be- yond conventional dependent type theory in some respects, and have a subtle metatheory.

Experience Report: Type-Checking Polymorphic Units For Astrophysics Research In Haskell, Takayuki Muranushi, Richard A. Eisenberg

Computer Science Faculty Research and Scholarship

Many of the bugs in scientific programs have their roots in mistreatment of physical dimensions, via erroneous expressions in the quantity calculus. Now that the type system in the Glasgow Haskell Compiler is rich enough to support type-level integers and other promoted datatypes, we can type-check the quantity calculus in Haskell. In addition to basic dimension-aware arithmetic and unit conversions, our units library features an extensible system of dimensions and units, a notion of dimensions apart from that of units, and unit polymorphism designed to describe the laws of physics. We demonstrate the utility of units by writing an astrophysics …

Introduction To Parallel Computation, Clinton Mckay

Graduate Student Theses, Dissertations, & Professional Papers

Introduction to Parallel Computing is a course designed to educate students on how to use the parallel libraries and tools provided by modern operating systems and massively parallel computer graphics hardware.

Using a series of lectures and hands-on exercises. Students will learn about parallel algorithms and concepts that will aid them in analyzing a problem and constructing a parallel solution, if possible, using the tools available to their disposal.

The course consists of lectures, projects, quizzes, and homework. The combination of these components will deliver the necessary domain knowledge to students, test them, and in the process train them to …

A Hybrid Approach Using Rup And Scrum As A Software Development Strategy, Dalila Castilla

UNF Graduate Theses and Dissertations

According to some researchers, a hybrid approach can help optimize the software development lifecycle by combining two or more methodologies. RUP and Scrum are two methodologies that successfully complement each other to improve the software development process. However, the literature has shown only few case studies on exactly how organizations are successfully applying this hybrid methodology and the benefits and issues found during the process. To help fill this literature gap, the main purpose of this thesis is to describe the development of the Lobbyist Registration and Tracking System for the City of Jacksonville case study where a hybrid approach, …

Assessing Satellite Image Data Fusion With Information Theory Metrics, James Cross

Dissertations and Theses

A common problem in remote sensing is estimating an image with high spatial and high spectral resolution given separate sources of measurements from satellite instruments, one having each of these desirable properties. This thesis presents a survey of seven families of algorithms which have been developed to provide this common pattern of satellite image data fusion. They are all tested on artificially degraded sets of satellite data from the Moderate Resolution Imaging Spectroradiometer (“MODIS”) with known ideal results, and evaluated using the commonly accepted data fusion assessment metrics spectral angle mapper (“SAM”) and Erreur Relative Globale Adimensionelle de Synth`ese (“ERGAS”). …

Complexity Of The Soundness Problem Of Workflow Nets, Guan Jun Liu, Jun Sun, Yang Liu, Jin Song Dong

Research Collection School Of Computing and Information Systems

Classical workflow nets (WF-nets for short) are an important subclass of Petri nets that are widely used to model and analyze workflow systems. Soundness is a crucial property of workflow systems and guarantees that these systems are deadlock-free and bounded. Aalst et al. proved that the soundness problem is decidable for WF-nets and can be polynomially solvable for free-choice WF-nets. This paper proves that the soundness problem is PSPACE-hard for WF-nets. Furthermore, it is proven that the soundness problem is PSPACE-complete for bounded WF-nets. Based on the above conclusion, it is derived that the soundness problem is also PSPACE-complete for …

An Approach For Clone Detection In Documentation Reuse, Dmitry V. Lutsiv, Dmitry Koznov, Hamid A. Basit, Eng Lieh Ouh, Mikhail N. Smirnov, Konstantin Y. Romanovsky

Research Collection School Of Computing and Information Systems

The paper focuses on the searching method for repetitions in DocBook/DRL or plain text documents. An algorithm has been designed based on software clone detection. The algorithm supports filtering results: clones are rejected if clone length in the group is less than 5 symbols, intersection of clone groups is eliminated, meaningfulness clones are removed, the groups containing clones consisting only of XML are eliminated. Remaining search is supported: found clones are extracted from the documentation, and clone search is repeated. One step is proved to be enough. Adaptive reuse technique of Paul Bassett – Stan Jarzabek has been implemented. A …