ABSTRACT. Software synthesis is a technique for automatically generating code from a given specification. The goal of software synthesis is to make software development easier, while increasing both the productivity of the programmer and the correctness of the produced code. We present an approach to synthesis that relies on the use of automated reasoning and decision procedures. First we describe how to generalize decision procedures into predictable and complete synthesis procedures. Here completeness means that the procedure is guaranteed to find code that satisfies the given specification. The process of turning a decision procedure into a synthesis procedure will be illustrated using linear integer arithmetic as an example.  This approach is implemented in Comfusy [1]. Comfusy is an extension to the Scala compiler and a tool for complete functional synthesis. It accepts as an input expressions with input and output variables and outputs code that computes output values as a function of input values. In addition, it also outputs the preconditions that the input variables have to satisfy in order for a
solution to exist.

However, writing a complete specification can be a tedious task, sometimes even harder than writing the code itself. To overcome this problem, ideally the user could provide a few input-output examples, and then the code should be automatically derived.  We outline how to
broaden usability and applications of current software synthesis techniques.

We describe a live programming framework that allows end-users to perform transformations over strings using examples, and generate reusable stand-alone scripts. [2] Motivated by applications in automating repetitive file manipulations, we present synthesis algorithms and a language which are able to handle related tasks. This language contains operators like map, reduce, partition and split.  They can be easily combined to create more complex transformers.  The synthesis algorithms for those operations build upon and extend the functionality of a proprietary software Flash Fill, a state-of-the-art synthesis tool.

[1]  Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter:
Complete functional synthesis. PLDI 2010: 316-329

[2] Sumit Gulwani, Mikaël Mayer, Filip Niksic, Ruzica Piskac:
StriSynth: Synthesis for Live Programming. ICSE (2) 2015: 701-704

ABSTRACT. In this paper we define \lambda_R : a foundational calculus for sequence processing with regular expression types. Its term language is the lambda calculus extended with sequences of terms and its types are regular expressions over simple types. We provide a flexible notion of subtyping based on the semantic notion of nominal interpretation of a type. Then we prove that types are preserved by reduction (subject reduction), and that there exist no infinite reduction sequences starting at typed terms (strong normalization).

ABSTRACT. The S and K combinator expressions form a well-known Turing-complete subset of the lambda calculus. Using Prolog as a meta-language, we specify evaluation, type inference and combinatorial generation algorithms for SK-combinator trees. In the process, we unravel properties shedding new light on interesting aspects of their structure and distribution. We study the proportion of well-typed terms among size-limited SK-expressions as well as the type-directed generation of terms of sizes smaller then the size of their simple types. We also introduce the {\em well-typed frontier of an untypable term} and we use it to design a simplification algorithm for untypable terms taking advantage of the fact that well-typed terms are normalizable.

ABSTRACT. In this paper we present vanHelsing, a fully automatic first-order theorem prover aimed especially at the class of problems that arise in compiler verification. vanHelsing accepts input problems formulated in a subset of the TPTP language and is specially tailored to efficiently solve expression equivalence problems formulated in first-order logic. Besides solving these problems, vanHelsing provides also graphical debugging help which makes the visualization of problems and localization of failed proofs much easier. From our experiments we noticed that using this specialized tool one can gain up to factor 3 in performance when compared to the non-specific theorem provers.

ABSTRACT. Multiset orders are mainly used in termination problems. Although the multiset orders were developed in many directions since their appearance more than 30 years ago, they were never analyzed in depth. Compared to sets, the complexity of the multiset theory increases exponentially with the number of multisets. Multiset orders normally use two multisets, but termination problems usually involve several multisets.

We analyze the relations between the multisets and their submultisets involved in the multiset order $>_{mso}$ and derive many properties that can be used in proofs. For two finite multisets $M,N$, there can be several pairs of their submultisets that satisfy $M>_{mso} N$, which can be seen as solutions to the equation $M>_{mso} N$. We determine the number of solutions that prove $M>_{mso} N$ and establish an order between them, not total, but admitting a minimum and a maximum. We determine the formulae for the minimal submultisets and provide several algorithms to find the maximal submultisets.

These properties of multiset orders are used to find alternative, simpler and in some cases more exact proofs to known results, like the termination of the multiset order or the fact that $>_{mso}$ is a strict order when $>$ is. These properties also enable a better understanding of the underlying theory and can also be used in implementations of theorem provers.

The minimal and maximal submultisets allow for a deeper analysis in termination problems with multiset orders, being able to determine, for instance, how fast a program can terminate.

ABSTRACT. Creative telescoping is a key tool in symbolic summation and
integration. It is used for constructing for a given definite sum or
integral an associated linear recurrence or differential equation, which
can then be used by other algorithms for finding out all sorts of
interesting facts about the quantity in question. Four generations of
creative telescoping algorithms can be distinguished: the first was
based on elimination in ideals of operator algebras. The second is the
classical Zeilberger algorithm and its variants. The third goes back to
an idea of Apagodu and Zeilberger. These algorithms are particularly
easy to implement and to analyze, but may not find optimal solutions.
The fourth and final (so far) generation of creative telescoping
algorithms is based on Hermite reduction. This idea was first worked out
for definite integrals of multivariate rational functions by Chen in his
PhD thesis. It has since been extended to more general classes of sums
and integrals. In the talk, we will explain the idea of this apprach and
a striking advantage over earlier algorithms. We will also present a
Hermite-reduction based algorithm applicable to definite hypergeometric
sums, published this year in a joint ISSAC paper with Chen, Huang, and Li.

ABSTRACT. Recursive branch and bound algorithms are often used, either rigorously or non-rigorously, to refine and isolate solutions to global optimization problems or systems of equations and inequalities involving nonlinear functions. The presented software library, Kodiak, integrates numeric and symbolic computation into a generic framework for the solution of such problems over hyper-rectangular variable and parameter domains. The correctness of both the generic branch and bound algorithm and the self-validating enclosure methods used, namely interval arithmetic and, for polynomials and rational functions, Bernstein expansion, has been formally verified. The algorithm has three main instantiations, for systems of equations and inequalities, for constrained global optimization, and for the computation of equilibria and bifurcation sets for systems of ordinary differential equations. For the latter category, and to enable the computation of bisection heuristics to reduce the branching factor, advantage is taken of the partial derivatives of the constraint functions, which are symbolically manipulated. Pavings (unions of box subsets of the search domain) for a continuum of solutions to underdetermined systems may also be produced. The capabilities of the software tool are outlined, and computational examples are presented.

ABSTRACT. We use several geometric techniques to characterize identifiability and to estimate noise robustness in the framework of l1-analysis regularization. This extends several recent theoretical results and algorithms that deal with the same issues in the less complex case of l1-synthesis regularizations.

ABSTRACT. This paper is a case study which presents numerical investigations based on the theoretical background developed in [1] The purpose is to numerically investigate the existence and the stability of equilibriums, as well as the existence of possible bifurcation at an equilibrium point for a set of given aero-dynamic data. The computations are performed in the framework of the non-simplified Aero-Data Model in a Research Environment, when the angle of attack is high.

ABSTRACT. Even-Odd Trees are a canonical tree-based number representation derived from a bijection between trees defined by the data type equation $T=1+T*T^*+T*T^*$ and positive natural numbers seen as iterated applications of $o(x)=2x$ and $i(x)=2x+1$ starting from $1$.

This paper introduces purely functional arithmetic algorithms for operations on Even-Odd Trees.

While within constant factors from their traditional counterparts for their average case behavior, our algorithms make tractable important computations that are impossible with traditional number representations.

ABSTRACT. Sparse matrix-vector multiplication (shortly spMV) and transposed spMV (shortly spMTV) are the most common subroutines in the numerical linear algebra. Sparse storage formats describe a way how sparse matrices are stored in a computer memory. Since the commonly used storage formats (like COO or CSR) are not sufficient for high-performance computations, extensive research has been conducted about maximal computational efficiency of these routines. For modern processor architectures (including multicore CPUs and GPUs), the main bottleneck of these routines is in the limited memory bandwidth. In this paper, we introduce the new approach for these routines for modern processor architectures using space efficient hierarchical format that can significantly reduce the amount of transferred amount of memory for almost all matrices arising from various technical areas. This format is an trade-off between space and execution efficiency. The performance of the these routines operation with these formats seems to be a very close to the hardware limits.

ABSTRACT. This article deals with the use of optimal lattice and optimal window in Discrete Gabor Transform computation. In the case of a generalized Gaussian window, extending earlier contributions, we introduce an additional local window adaptation technique for non-stationary signals. We illustrate our approach and the earlier one by addressing three time-frequency analysis problems to show the improvements achieved by the use of optimal lattice and window: close frequencies distinction, frequency estimation and SNR estimation. The results are presented, when possible, with real world audio signals.

ABSTRACT. The stretching rate of the sheet vary with time. The governing equations are reduced to ODE using the similarity transformations. The obtained equation is solved approximately by means of the Optimal Homotopy Asymptotic Method (OHAM). Some examples are given and the results obtained reveal that our procedure is effective and easy to use.

ABSTRACT. Clemens $et$ a$l$. have proposed SCBiCG (Bi-Conjugate Gradient method for Symmetric Complex matrices) ($\Gamma$, $m$) for solving linear equations with complex symmetric matrices, where coefficients $c_i$ need to be set in SCBiCG ($\Gamma$, $m$). They set the combinations $c_i$ with real number for SCBiCG ($\Gamma$, $m$) in their papers. However, we learn that the residual norms of SCBiCG($\Gamma$, $m$) do not converge in numerical experiments with several combinations when the coefficients $c_i$ are real, and the coefficients $c_i$ need to be set by users. We therefore design an efficient implementation such that the coefficients $c_i$ which are complex are given by a computation. Numerical experiments show that the residual norms of our proposed variant with the complex coefficients $c_i$ converge slightly faster than those of COCG (Conjugate Orthogonal Conjugate Gradient method).

ABSTRACT. In this paper, we would like to introduce a GPU accelerated solver for systems of linear equations with an infinite precision. The infinite precision means that the system can provide a precise solution without any rounding error. These errors usually come from limited precision of floating point values within their natural computer representation. In a simplified description, the system is using modular arithmetic for transforming an original SLE into dozens of integer SLEs that are solved in parallel via GPU. In the final step, partial results are used for a calculation of the final solution. The usage of GPU plays a key role in terms of performance because the whole process is computationally very intensive. The GPU solver can provide about one magnitude higher performance than a multithreaded one.