Marc Moreno Maza

2papers

2 Papers

SCOct 25, 2018
Symbolic-Numeric Integration of Rational Functions

Robert M. Corless, Robert H. C. Moir, Marc Moreno Maza et al.

We consider the problem of symbolic-numeric integration of symbolic functions, focusing on rational functions. Using a hybrid method allows the stable yet efficient computation of symbolic antiderivatives while avoiding issues of ill-conditioning to which numerical methods are susceptible. We propose two alternative methods for exact input that compute the rational part of the integral using Hermite reduction and then compute the transcendental part two different ways using a combination of exact integration and efficient numerical computation of roots. The symbolic computation is done within BPAS, or Basic Polynomial Algebra Subprograms, which is a highly optimized environment for polynomial computation on parallel architectures, while the numerical computation is done using the highly optimized multiprecision rootfinding package MPSolve. We show that both methods are forward and backward stable in a structured sense and away from singularities tolerance proportionality is achieved by adjusting the precision of the rootfinding tasks.

SEJan 24, 2012
Generating Program Invariants via Interpolation

Marc Moreno Maza, Rong Xiao

This article focuses on automatically generating polynomial equations that are inductive loop invariants of computer programs. We propose a new algorithm for this task, which is based on polynomial interpolation. Though the proposed algorithm is not complete, it is efficient and can be applied to a broader range of problems compared to existing methods targeting similar problems. The efficiency of our approach is testified by experiments on a large collection of programs. The current implementation of our method is based on dense interpolation, for which a total degree bound is needed. On the theoretical front, we study the degree and dimension of the invariant ideal of loops which have no branches and where the assignments define a P-solvable recurrence. In addition, we obtain sufficient conditions for non-trivial polynomial equation invariants to exist (resp. not to exist).