- Takeshi Ogita (Tokyo Woman's Christian University, Japan)

- Computer-assisted proofs for ODE and PDE
- Verified numerical linear algebra
- Verified numerical computations for dynamical systems
- Mathematics for verified numerical computations
- Applications of verified numerical computations

- A
*short abstract*will appear on the conference web page as soon as accepted,

and in the post-conference proceedings to be published by Springer LNCS. - A
consisting of*journal special issue**full papers*will be organized for consideration

in the journal Mathematics in Computer Science, published by Birkhauser/Springer.

- If you would like to give a talk at MACIS, you need to submit
at least a SHORT paper -- see
guideline
for the details.

- The deadline for all submissions is
~~August 11, 2015~~**September 1, 2015**-- see the Call for Papers for the details

- After the meeting, the submission guideline for a journal special issue will be communicated to you by the session organizers.

### Construction of Lyapunov functions by validated computation

Nobito Yamamoto (The University of Electro-Communications, Japan), Kaname Matsue (Institute of Statistical Mathematics, Japan), Tomohiro Hiwaki (The University of Electro-Communications, Japan)

**Abstract**: We provide a systematic method to validate the domain of Lyapunov functions around hyperbolic fixed points both for continuous and for discrete dynamical systems with computer assistance. We also give the construction of Lyapunov functions around periodic orbits as fixed points of Poincaré maps as well as validation examples in our talk.### A recursive formula for the circumradius of the n-simplex

Kenta Kobayashi (Hitotsubashi University, Japan)

**Abstract**: We present a recursive formula which gives the circumradius of the n-simplex in terms of the circumradius of its facets. Our formula shows that the circumradius of the n-simplex is closely related to the distances from each vertex to the circumcenter of the opposite facet. In particular, our formula shows that the circumradius of the tetrahedron can be expressed by the areas of the pedal triangles of each facet. We could only prove the formula for n up to 5, but numerical results strongly suggest that our formula holds true for any n.### H3 and H4 regularities of the Poisson equation on polygonal domains

Takehiko Kinoshita (Kyoto University), Yoshitaka Watanabe (Kyushu University), Mitsuhiro Nakao (National Institute of Technology, Sasebo College)

**Abstract**: This paper presents two equalities of H3 and H4 semi-norms for the solutions of the Poisson equation in a two-dimensional polygonal domain. These equalities enable us to obtain higher order constructive a priori error estimates for finite element approximation of the Poisson equation with validated computing.### Error-free transformation of matrix multiplication by a posteriori verification

Katsuhisa Ozaki (Shibaura Institute of Technology), Takeshi Ogita (Tokyo Woman's Christian University)

**Abstract**: This paper is concerned with accurate computations for matrix multiplication. An error-free transformation of matrix multiplication is developed by authors. It transforms a product of two floating-point matrices to a sum of several floating-point matrices by using only floating-point arithmetic. This transformation is useful for not only accurate computations for matrix multiplication but also interval enclosure of matrix multiplication. The key technique is an error-free splitting of floating-point numbers. We improve the error-free splitting and develop a posteriori validation method for the error-free transformation.### Verified computations for solutions to semilinear parabolic equations using the evolution operator

Akitoshi Takayasu (Waseda University), Makoto Mizuguchi (Waseda University), Takayuki Kubo (University of Tsukuba), Shin'Ichi Oishi (Waseda University)

**Abstract**: This article presents a theorem for guaranteeing existence of a solution for an initial-boundary value problem of semilinear parabolic equations. The sufficient condition of our main theorem is derived by a fixed-point formulation using the evolution operator. We note that the sufficient condition can be checked by verified numerical computations.### Verified error bounds for the real gamma function using double exponential formula over semi-infinite interval

Naoya Yamanaka (Teikyo Heisei University), Tomoaki Okayama (Hiroshima City University), Shin'Ichi Oishi (Waseda University)

**Abstract**: An algorithm is presented for computing verified error bounds for the value of the real gamma function. It has been shown that the double exponential formula is one of the most efficient methods for calculating integrals of the form. Recently, an useful evaluation based on the double exponential formula over the semi-infinite interval has been proposed. However, the evaluation would be overflow when applied to the real gamma function directly. In this paper, we present a theorem so as to overcome the problem in such a case. Numerical results are presented for illustrating effectiveness of the proposed theorem in terms of the accuracy of the calculation.