scholarly journals Toward the Synthesis of Gauss Pivoting Code for Linear Systems Resolution : Application Mechanical Problems

10.29007/75kg ◽  
2018 ◽  
Author(s):  
Nacera Djehaf ◽  
Matthieu Martel ◽  
Mikaël Barboteu

The purpose of this talk is primarily to introduce a new methodology to synthesize numerically accurate programs for the Gaussian elimination method in order to solve linear systems coming from mechanical problems. The synthesis is based on program transformation techniques and it is guided in its estimation of accuracy by interval arithmetic that computes the propagation of roundoff errors. Besides a discussion on numerical accuracy issues related to floating-points arithmetics and roundoff errors, we present our approach used to compute the error bound during the resolution process. Finally, some experimental results will be presented to prove the efficiency of our synthesizer tool and show that the specialized produced code to solve the family of systems given in input is far more accurate and faster than the standard implementation of the Gauss method.

10.29007/gpsh ◽  
2018 ◽  
Author(s):  
Abdulbasit Ahmed ◽  
Alexei Lisitsa ◽  
Andrei Nemytykh

It has been known for a while that program transformation techniques, in particular, program specialization, can be used to prove the properties of programs automatically. For example, if a program actually implements (in a given context of use) a constant function, sufficiently powerful and semantics preserving program transformation may reduce the program to a syntactically trivial ``constant'' program, pruning unreachable branches and proving thereby the property. Viability of such an approach to verification has been demonstrated in previous works where it was applied to the verification of parameterized cache coherence protocols and Petri Nets models.In this paper we further extend the method and present a case study on its appication to the verification of a cryptographic protocol. The protocol is modeled by functional programs at different levels of abstraction and verification via program specialization is done by using Turchin's supercompilation method.


Sign in / Sign up

Export Citation Format

Share Document