ABSTRACT. The opening session will contain a short presentation of SYNASC including a summary concerning the submissions, the acceptance rate and some details on the program.

ABSTRACT. This lecture addresses gender issues in CS from Research, Education, Society perspectives. I start from UN Goal 5, Achieve gender equality and empower all women and girls to contextualize the topic in an open and meaningful context. I present research issues, some from my own projects (see 1,2,3), others from examples of biased technology, like smartphone voice assistants and data sets for job recruiting based on male population.

Then, I present statistics about female presence in education, research and industry. Further, the presentation goes in depth and presents two specific projects we run at the Norwegian University of Science and Technology for increasing gender balance among students and among professors.

These are ADA (URL https://www.ntnu.edu/girls/about-ada) and IDUN (URL https://www.ntnu.edu/idun).

The presentation concludes with a list of International projects and resource.

ABSTRACT. We employ the mathematical methodology of metric semantics in designing the continuation-based denotational and operational semantics for two process calculi recently investigated in the literature based on well-known Milner's CCS. We prove that our denotational models are weakly abstract with respect to their corresponding operational models.

ABSTRACT. Deep learning (DL) methods have recently gained popularity. Training this class of models is, however, computing-intensive, and frequently GPUs are used to boost performance. Although the costs of GPU-based systems are gradually reducing due to the high demand, they are still prohibitive: in public clouds, GPU-powered virtual machines (VMs) time unit price is 5-8x higher than CPU-only VMs. While the cloud remains the most cost-effective and flexible deployment, operation costs can be reduced, in large settings, by rightsizing and sharing resources among multiple processes. This work addresses the online joint capacity planning and job scheduling with due dates problem and proposes alternative matheuristic solution methods. Our objective is to optimize operation costs by: i) rightsizing the VM capacities at each node, ii) partitioning the set of GPUs among multiple concurrent jobs on the same VM, and iii) determining a due-date-aware job schedule. The effectiveness of the proposed hierarchical approach, coupled with an appropriate Mixed Integer Linear Programming formulation, is validated against first-principle methods by relying on simulation. The experiments prove that the efficiency of GPU-based systems evaluated in terms of costs can be improved by 50-70%. Finally, scalability analyses show that the proposed approach enables to solve problem instances with up to 100 nodes in less than one minute on average, making it suitable for practical scenarios.

ABSTRACT. Complex applications, which include microservices, computationally intensive batch jobs, and sophisticated interaction with the external environment, demand for heterogeneous computational infrastructures that range from cloud to HPC and edge computing. In this context, a crucial problem is to facilitate the work of DevOps teams in i. the conception of the right operational architecture for the application, ii. its transformation into infrastructural code that automates its deployment, taking into account the peculiarities of each of the diverse infrastructures involved in this, and iii. its operation. The SODALITE framework aims at addressing this scenario. This paper presents the main features offered by the first version of the framework, currently focusing on managing cloud and HPC clusters, and shows them in practice through a relevant case study.

ABSTRACT. In today's world of big data, multi-tenant cloud Customer Relationship Management Systems with an ever increasing pressure to customize offerings for each prospect, there is a need for distributed problem solving that can help salespeople win sales using data driven recommendations.

With this work we are proposing a Decision Support System constructed as a multi-agent architecture for Business to Business Customer Relationship Management Systems that can guide salespeople during the conversion of a prospect into a client. The implementation and the results using real-world CRM data are presented and discussed in this paper.

ABSTRACT. The main aim of this paper is to give some local fixed point theorems for three classes of generalized contractions with applications to open mapping theorems. We consider Chatterjea and Berinde type contractions of the well-known alpha-contraction, and we obtain results which generalize the classical case of Banach contractions.

ABSTRACT. The aim of this paper is to survey the most relevant developments done in the last decade around the concept of almost contractions.

ABSTRACT. The main purpose of this study is to present some results related to Meir-Keeler Theorem. Beside the existence and uniqueness results (which are well-known) we give several stability properties (data dependence, well-posedness in sense of Tykhonov, Ulam-Hyers stability and Ostrowski stability property) of the fixed point equation.

ABSTRACT. The purpose of this work is to present some qualitative results in fixed point theory, based on iteration method, for some classes of multi-valued operators. We will consider the following classes: multi-valued contractions, multi-valued Berinde type contractions, multi-valued graphic contractions.

ABSTRACT. In this paper, we propose a general construction for creating statistically random sequences using digit expansions of real functions. We identify different pitfalls and weaknesses in the presented system. A pseudorandom number generator (PRNG) is described based on a modified Riemann-Siegel Z(t) function. It is shown that the output satisfies the statistical requirements of the NIST SP 800-22 randomness suite. We also analyze the resistance of the system against some well-known cryptographic attacks.

ABSTRACT. A common pattern in high performance scientific computing is the structured grid pattern in which one or more elements of a matrix are computed as a stencil operation of other matrix neighbouring elements. Since there are multiple options to efficiently implement this pattern on modern computing architectures, we provide a comparison of the performance of a number of parallel implementations on a multi-core system with GPU capabilities. The application used for this case study implements the propagation of wireless signals in a bi-dimensional environment, considering reflections and signal attenuation. The parallel programming paradigms examined in this paper include CUDA , TBB, Rust and OpenMP, with CUDA proving to be the fastest implementation.

ABSTRACT. A numerical simulation algorithm is presented for fractional-order systems, based on the Adams-Bashforth-Moulton(ABM) predictor-corrector scheme. The algorithm is implemented in CUDA, using the specific GPU capabilities. A comparison with the implementation on a BlueGene/P cluster show the advantages and disadvantages of using this CUDA implementation.

ABSTRACT. For a pair of polynomials with real or complex coefficients, given in any particular basis, the problem of finding their GCD is known to be ill-posed. An answer is still desired for many applications, however. Hence, looking for a GCD of so-called \textsl{approximate polynomials} where this term explicitly denotes small uncertainties in the coefficients has received significant attention in the field of hybrid symbolic-numeric computation. In this paper we give an algorithm, based on one of Victor Ya.~Pan, to find an approximate GCD for a pair of approximate polynomials given in a Lagrange basis. More precisely, we suppose that these polynomials are given by their approximate values at distinct known points. We first find each of their roots by using a Lagrange basis companion matrix for each polynomial, cluster the roots of each polynomial to identify multiple roots, and then ``marry'' the two polynomials to find their GCD. At no point do we change to the monomial basis, thus preserving the good conditioning properties of the original Lagrange basis. We discuss advantages and drawbacks of this method. The computational cost is dominated by the rootfinding step; unless special-purpose eigenvalue algorithms are used, the cost is cubic in the degrees of the polynomials. In principle, this cost could be reduced but we do not do so here.

ABSTRACT. In the last few years the research done in automatising of medical diagnosis systems have increased significantly despite the fact that it is a slow process to gain trust in such a domain where every detail can make the difference between life and death. Lots of methods based on classic programmable algorithms and machine learning methods gave very good results in lung segmentation and tumor segmentation tasks which can lead to a big increase in early prevention of such dangerous diseases. The goal of this paper is to prove that a classic programmable algorithm can detect lung tumors on CT scans with very good precision and can run as fast as a neural network. To achieve it we implemented a segmentation algorithm using the CUDA API and managed to obtained important results in both precision and speed of detection.

ABSTRACT. Road accidents are directly proportional to the number of cars on the market. Without car safety systems, this number will keep rising. The main factor for the accidents are drowsiness and fatigue. These can be detected by analysing images with the driver so, an example of a driver monitoring system may include a monitoring camera, mounted in front of the driver. A method based on machine learning and computer vision can be a solution to solve the problem of driver safety. The objectives of our work includes an analysis of different approaches of driver monitoring systems and the implementation of a system based on convolutional neural networks which analyze the images coming from a monochrome infrared monitoring camera placed in front of the driver seat. The goal of this work is to decide if the driver is attentive or not (attentive) on the road. Our research was done by implementing a classifier based on AlexNet architecture and return one of the 6 attention classed. To improve the system accuracy, the face was detected using DNN Face Detector (using OpenCV approach). The final system is able to detect when the driver is not paying attention to the road, based on existing test data.

ABSTRACT. The classification of Gastrointestinal Polyps from colonoscopy video clips uses special machine learning techniques. In this paper, for classification of polyps in hyperplastic lesions, serrated lesions and adenomas ones, we used Inception V3, a convolution neural network that rely on multi-branch convolution networks. We used a dataset in which there are 152 instances with three types of lesions, for 76 polyps. The results obtained with the Inception V3 convolutional neural network model are satisfactory compared with the other paper and the human experts.

ABSTRACT. SPIKE, an induction-based theorem prover built to reason on conditional theories with equality, is one of the few formal tools able to perform automatically mutual and lazy induction. Designed at the beginning of 1990s, it has been successfully used in many non-trivial applications and served as a prototype for different proof experiments and extensions. The first paper introducing SPIKE is [13], published shortly after the tool was created. The goal of this paper is to highlight and bring together in one spot the major changes supported by SPIKE since then.

ABSTRACT. This paper presents the extended processing of adjectives with visible arguments in the Mizar system. The proposed enhancement is compared with the current implementation by presenting the results of a case study based on refactoring selected Mizar Mathematical Library (MML) theories.

ABSTRACT. We present a model generator which generates SAT problems from digraphs. There are a few restrictions on the input digraphs. There must be no self-loops, and its vertices must be Boolean variables or labeled by distinct Boolean variables. We call such digraphs communication graphs. The model is pretty straightforward: if the communication graph contains the edges $(a, b)$ and $(a, c)$, and there is no other edge from $a$, then this is encoded by the clause: $\{\neg a, b, c\}$. The intuition is that from $a$ we can go to $b$ or $c$. We have to represent all cycles as well. If $(a, b, c, a)$ is a cycle with the set of exit points $\{d, e\}$ in the input communication graph, then it is encoded by the clause: $\{\neg a, \neg b, \neg c, d, e\}$. The intuition is the following: we have to leave the cycle and we have to go to $d$ or $e$. We call this model as the weak model of communication graphs. We show that the weak model is a Black-and-White SAT problem if and only if the input is a strongly connected communication graph. We prove also that all clauses in such models are independent. From this we obtain that a weak model generated from a strong digraph is a minimal unsatisfiable SAT instance if we add to it the black and the white clauses, which are the only solutions of a Black-and-White SAT problems. The generation of weak models is difficult because we have to find all cycles, including non-simple cycles. Therefore, we discuss how to create models of digraphs without cycle detection.

ABSTRACT. Mathematical logic was developed in an effort to provide formal foundations for mathematics. In this quest, which ultimately failed, logic begat computer science, yielding both computers and theoretical computer science. But then logic turned out to be a disappointment as foundations for computer science, as almost all decision problems in logic are either unsolvable or intractable. Starting from the mid 1970s, however, there has been a quiet revolution in logic in computer science, and problems that are theoretically undecidable or intractable were shown to be quite feasible in practice. This talk describes the rise, fall, and rise of logic in computer science, describing several modern applications of logic to computing, include databases, hardware design, and software engineering.

ABSTRACT. We study binomiality of the steady state ideals of chemical reaction networks. Considering rate constants as indeterminates, the concept of unconditional binomiality has been introduced and an algorithm based on linear algebra has been proposed in a recent work for reversible chemical reaction networks, which has a polynomial time complexity upper bound on the number of species and reactions. In this article, using a modified version of species--reaction graphs, we present an algorithm based on graph theory which performs by adding and deleting edges and changing the labels of the edges in order to test unconditional binomiality. We have implemented our graph theoretical algorithm as well as the linear algebra one in Maple and made experiments on biochemical models. Our experiments show that the performance of the graph theoretical approach is similar to or better than the linear algebra approach, while it is drastically faster than Gr\"obner basis and quantifier elimination methods.

ABSTRACT. In graph theory, graph colorings are a major area of study. Graph colorings involve the constrained assignment of labels (colors) to vertices or edges. There are many types of colorings defined in the literature, the most common being the proper vertex coloring. The proper vertex k-coloring is defined as vertex coloring from a set of k colors such that no two adjacent vertices have the same color. In this paper, we focus on a variant of the proper vertex k-coloring problem, termed graceful coloring. A graceful k-coloring of an undirected connected graph G is a proper vertex coloring using k colors, that induces a proper edge coloring, where the color for an edge (u; v) is the absolute value of the difference between the colors assigned to vertices u and v. The minimum k for which a graph G has a graceful k-coloring is termed the graceful chromatic number of the graph. In a previous work (Mincu, Obreja, Popa, SYNASC 2019) we find the graceful chromatic number for some well-known graphs and classes of graphs, such as diamond graph, Petersen graph, Moser spindle graph, Goldner-Harary graph, friendship graphs, fan graphs, and others. In this study, we continue the investigation and find the graceful chromatic number for other well-known individual graphs, like D¨urer graph, Heawood graph, M¨obius-Kantor graph, Nauru graph, Tietze’s graph, Golomb graph and classes of graphs, like cactus, Gear, web graphs, etc.