ABSTRACT. Symbolic execution plays a crucial role in modern testing techniques, debugging, and automated program analysis. In particular, it is used for generating test cases. Instead of executing a program with concrete values, symbolic execution uses abstract symbols. Execution is performed by maintaining the current symbolic state together with appropriate

Although symbolic execution techniques have improved enormously in the last few years with application in several software analysis tools, not much effort has been spent on its formal justification. In this talk, based on a join effort with Frank de Boer, we introduce a formal model of symbolic execution for a basic programming language and show its correctness.

We show how to extend the basic theory to more advanced programming concepts, such as recursive procedures, object-orientation, arrays, multithreading, and concurrent objects, and conclude with some of the challenges and possibilities of a formal approach to symbolic execution.

ABSTRACT. Minimizing the Euclidean distance (l2 -norm) from a given point to the solution set of a given system of polynomial equations can be accomplished via critical point techniques. This article extends critical point techniques to minimization with respect to Hamming distance (l0-“norm”) and taxicab distance (l1 -norm). Numerical algebraic geometric techniques are derived for computing a finite set of real points satisfying the polynomial equations which contains a global minimizer. Several examples are used to demonstrate the new techniques.

ABSTRACT. The paper applies Bézier extraction that enables the conversion of T-splines to Bézier surfaces. This approach is used to represent the boundary in the considered boundary value problems modeled by the Laplace equation. As a result, it is possible to define the boundary with the effective T-splines and solve the boundary value problems by parametric integral equation system (PIES) using Bézier surfaces. In numerical examples, we examine the effectiveness of the proposed strategy for 3D problems with known analytical solutions.

ABSTRACT. In this paper six theoretical results, concerning the static stability and existence of a capillary free surface in a dewetted Bridgman crystal growth process, are presented. The results are obtained in an axis symmetric 2D model for semiconductors for which the wetting angle and the growth angle is greater than 180. Numerical illustration is given in case of GaSb semiconductor when oxygen is introduced in the ampule for increase the apparent wetting angle. The reported results can help, the practical crystal growers, in better understanding the dependence of the free surface shape and size on the pressure difference across the free surface and prepare the appropriate seed size and thermal conditions before seeding the growth process.

ABSTRACT. Asteroid discovery is not an activity restricted to the notable surveying efforts that have their private staff, equipment and detection programs, but it is also popular among amateurs and various mini-surveys. In light of this situation, new Near Earth Asteroids (NEAs) are found out every day. Most of the amateurs and mini-surveys discoveries are obtained by means of manual methods, based on the human eye examination of celestial image data. Naturally, these methods are limited by the size and complexity of the input data. To address the issues linked to such dimensional data, we developed under the NEARBY project an automated pipeline prototype for asteroid detection. This solution comes in the form of a modular system, allowing us to explore different detection techniques. Throughout this paper a visual technique, based on image processing will be presented as a possible future replacement for the astronomical technique, based on computation in the celestial reference system used now.

ABSTRACT. Sorting is a fundamental problem in computer science and represents a bottleneck in many applications. Quicksort is one of the most renowned algorithms that solves this problem and is often implemented in many standard libraries due to its simplicity and performance. Being a Divide and Conquer algorithm, it is easy to modify it and take advantage of parallel computers. The aim of this experimental paper is to come up with a parallel implementation of the algorithm, analyze its performance and point out some surprising bottlenecks of this well-known problem.

ABSTRACT. In this paper, we present an approach to localize pulmonary lung lesion using fuzzy deep learning. Our approach uses a simple convolutional neural network based on the LIDC-IDRI patches images with a probability vector (fuzzy) determining the belonging into an anatomical structure on CTs.

ABSTRACT. Eye Tracking technologies opened countless opportunities thanks to their non-intrusive way to interact with people, not only defining new levels of entertainment, but also providing significant important data in healthcare, offering treatment through training for people with vision disorders. In this paper we present an approach for helping children with cerebral palsy to adapt to the world and increase their capacity of concentration by enabling them to use Eye Tracking devices without requiring the classic time consuming calibration tests.

ABSTRACT. Immersive technologies (virtual and augmented reality) started gaining a lot of ground over the past few years initially in the video game industry, followed by simulators and finally integrated into many other classic applications. This paper aims to analyze how users respond to using new controlling devices in a scene designed as a driving simulator (race car track). The landscape and the controls are specifically tailored for interactions within immersive environments. In order to understand the capabilities of the experimental application and evaluate the new controls, several tests were conducted. The results are presented from a user experience perspective, emphasizing qualities, side-effects, and problems of such an approach.

ABSTRACT. This paper is addressed to the problem of estimating the trend of the price for different periods of time while using different classification algorithms which are making predictions based on previous states of the products and how they evolved after that. We try an approach of creating prediction models in mass, many of them having bad results but in the same time saving the models with very good estimations.

ABSTRACT. In the last few years the filed of deep learning and in general machine learning in medical imaging has become the state-of-the-art in terms of medical image analysis and processing. In our experimental work, we try to provide a high-level approach of fully connected deep neural networks applied in medical image segmentation (lung CT scans), by using Deep Learning GPU Training System (DIGITS) avoiding rigorous mathematical formalism of neural networks.

For this purpose using the concept of solving problems by learning from experiences is necessary. The goal of our experimental work is to design an analysis of particular methods in lung CT scans segmentation by using the one of the most used architecture in the filed deep learning for biomedical image segmentation techniques, U-NET architecture. This will lead to obtain in the back-end a mathematical model with the purpose of training to obtain useful results when fed input data and will demonstrate how to train a fully convolutional network (FCN) like U-NET model to segment lung tumor tissues found in computed tomographic (CT) on abdominal images using GPU processing with NVidia DIGITS.

ABSTRACT. To deal with large amounts of data while offering high availability and throughput and low latency, cloud computing systems rely on distributed, partitioned, and replicated data stores. Such cloud storage systems are complex software artifacts that are very hard to design and analyze, also because of the need to analyze both correctness and performance. Formal specification and model checking should therefore be beneficial during their design and validation. In particular, I propose rewriting logic and its accompanying Maude tools as a suitable framework for formally specifying and analyzing both the correctness and the performance of cloud storage systems. I then give an overview of the use of rewriting logic at the University of Illinois' Assured Cloud Computing center on industrial data stores such as Google's Megastore and Facebook/Apache's Cassandra. I also briefly summarize the experiences of the use of a different formal method for similar purposes by engineers at Amazon Web Services.

ABSTRACT. The degree distance of a connected graph G, denoted by D'(G) was proposed by Gutman and independently by Dobrynin and Kochetova as a weighted version of the Wiener index. In a previous paper [ Utilitas Mathematica, 97:7(2015), 161-181] Tomescu and Kanwal determined four unicyclic connected graphs having smallest degree distances. Here seven bicyclic connected graphs of order n having smallest degree distances are determined provided n≥19.

ABSTRACT. In computer science, Virtual Organisms (VO) are structures capable of populating the level between hardware and adaptive software agents. This paper discusses the applicability of this concept to the publisher-subscriber paradigm, by having a VO as the broker inside the network. When considering long distances between publishers and subscribers, the VO's (or broker's) usage is to optimize their connection experience. Thus, the VO's cells can be used as either mirroring nodes to support streaming applications, or just as nodes managing traffic flow optimizations in the publisher-subscriber paradigm. The paper also presents a novel greedy algorithm and workflows for choosing the intermediate path nodes connecting entities in the network through the VO's cells. The evaluation section shows how it can be applied to optimize routing traffic in cloud computing for gaming using a real dataset, and also introduces the concept of predictive reconfiguration for VOs.

ABSTRACT. —There is an exponential volume of captured images (millions of captures taken every night to be processed and analyzed), Big Data analysis has become essential for the study of the solar system. The analysis often requires more advanced algorithms capable of processing the available data and solve the essential problems in almost real time. One such problem that needs very rapid investigation involves the detection of Near Earth Asteroids (NEAs) and their orbit refinement which improves the answer to the question “will the Earth colide with any hazardous asteroid?”. This paper proposes a cloud distributed architecture meant to render near real-time results, focused on image stacking techniques and pairing of unknown objects with known orbits for asteroid discovery and identification.

ABSTRACT. Permafrost is a terrestrial Essential Climate Variables, being extremely vulnerable to climate change and recent years have witnessed a growing interest in permafrost sensitivity to air temperature rising, especially in the arctic regions. As a result of climate change, permafrost degradation generates irreversible changes in the plant species composition and in the local hydrological system, affecting the infrastructure and local comunities. The advantages of using remote sensing data to reveal landscape changes in permafrost areas has been widely acknowledged. The aim of this study is to quantify the landscape changes based on free satellite images available in archives in several sites distributed in different types of permafrost zones (continuous, discontinuous, isolated and sporadic) located in West Siberia. We used satellite images from the summer season selected from Landsat archive in the last 30 years to assess the spatio-temporal changes in vegetation indices, lakes extent changes and distribution of wild fire scars. To quatify the spatio-temporal changes we used Google Earth Engine and the first results show that the main landscape changes in this time interval are related to lake shrinking due to permafrost degradation in several sites, an increase in the normalized difference vegetation index values, meaning a slight greening as reported by other studies in southern tundra. Also, a high density of wildfire scars has been identified in the southern part of the West Siberia in several years. Acknowledgments This work was supported by a grant of the Romanian National Authority for Scientific Research and Innovation, CCDI-UEFISCDI, project number ERANET-RUS-PLUS-SODEEP, within PNCD III.

ABSTRACT. The main objective of this study is to propose an algorithm that delineates in an automatic and efficient manner large scale floods from large collections of Synthetic Aperture Radar (SAR) images. The proposed algorithm is based on the regular processing of subsequently acquired pairs of Sentinel-1 SAR images from the same orbit. The algorithm then detects all meaningful positive/negative changes in the SAR backscatter derived from the two images acquired pre- and post- the event. The procedure is applied iteratively to multi-temporal data collections allowing to determine an update of the flood extent each time a new image is acquired. The detected flooding-related changes are used to regularly and automatically update the preceding water bodies and floodwater maps of a region of interest. The particularly high sampling rate of the Sentinel-1 A/B constellation enables the automated high-frequency monitoring of all relevant changes. The approach has been validated after intensive testing over different areas of interest in South East Asia e.g. Myanmar and Laos as countries highly affected by floods. Moreover, the algorithm is implemented on a virtual platform that handles efficiently large collections of Sentinel-1 data from all the orbits and dates available over areas of interest affected by floods.

ABSTRACT. In this paper, we investigate state of the art deep learning model topologies applied to the problem of semantic segmentation, particularly for extracting road segments in satellite images. In our experiments we used Pan-Sharpened RGB input data from the SpaceNet Roads Dataset, analyzed U-Net, SegNet and ResNet model performance and investigate how different loss functions affect the model performance.

ABSTRACT. The field of numerical algebraic geometry consists of a collection of numerical methods for computing and manipulating solution sets to systems of polynomial equations. One foundational method in numerical algebraic geometry is homotopy continuation which tracks solutions as a parameter is changed. This tutorial will introduce some basic fundamental ideas associated with homotopy continuation and numerical algebraic geometry which will be demonstrated using the software package Bertini available at bertini.nd.edu

ABSTRACT. The recent increased availability of insulin pumps and continuous glucose monitors created a new focus in current research: the development of a close-loop system that would become the perfect artificial pancreas. So far, there are some community projects that try to achieve this goal. If our hypothesis is supported, then artificial intelligence could solve this problem once and for all. Artificial intelligence could help the patient maintain the blood glucose level as stable as possible, while requiring little to no interaction from the user. Such a closed-loop system may improve the quality of life for the patient and prevent the long-term side effects of diabetes.

ABSTRACT. The serious games show great potential for older adults with Parkinson’s disease, because video games combine both cognitive and physical training which require the user to perform physical movements while conducting cognitive exercises. A user can interact with a virtual coach to control the video game using voice recognition, and the video game can interact with the user by offering feedback after sentiment recognition. By example, the virtual coach can discover that the user is more sad that a day before and can tell him/her a joke. Therefore, machine learning may be used to generate voice responses that are predicted to improve or maintain a user’s level of engagement with his/her virtual coach. Also, the system tries to combine real time speech processing with the serious game and the parameterization of the difficulty level. The aim is to develop an automatic speech and sentiment recognition system applicable to distorted speech. This system can be integrated into a speech therapy application that incorporates the motivational potential contributing to frequent and autonomous usage.

ABSTRACT. This work presents an intelligent hospital management system for medical personnel and patients scheduling. In response to the dynamic changing environment, system must be capable to continuously adjust the schedules. We propose a multi-agent architecture that can handle this issues. Different hospital concepts, medical personnel, patients and other hospital resources were modeled as agents. We stated that such system would substantially reduce the waiting time in medical institutions by managing resources more efficiently.

ABSTRACT. —Motifs are small topological patterns of interconnections occurring in complex networks at numbers that are significantly higher than those in randomized networks. In their pioneering work

ABSTRACT. It has become apparent to many that we are enjoying a golden age of transportation, whereby people can travel the world and cargo can be shipped from even the most exotic of sources, everything with a high degree of punctuality expectation. The former is indeed the scope of this presentation: delays in transport can prove to be catastrophic if not properly handled (ex. emergency patient or perishable produce). To this end, the present proposal puts forward the problem of determining real-time delays within the constraints of a transport system. An exploration on software and hardware solutions for measuring the progress of a vehicle within a scheduled operation, and offering said information for processing and use, has been done in a generic matter, as to allow application on a vast range of environments

ABSTRACT. Artificial Intelligence is the science of combining technological and theoretical concepts from multiple disciplines aimed at creating similar behavior in machines to that found in humans. The present work investigates methods of improving the field of pattern classification by applying evolutionary algorithms to train deep neural networks architectures. A significant advantage of evolutionary algorithms over backpropagation is that the neuroevolutionary algorithms allows for training parts of the deep neural network. The framework developed for the present work can be adapted to the required memory and processing resources of the target hardware platform in different application scenarios.