Evgeny Novikov

Evgeny Novikov, Anton Tuzov

In this paper we construct a third order method for solving additively split autonomous stiff systems of ordinary differential equations. The constructed additive method is L-stable with respect to the implicit part and allows to use an arbitrary approximation of the Jacobian matrix. Automatic stepsize selection based on local error and stability control are performed. The estimations for error and stability control have been obtained without significant additional computational costs. Numerical experiments show reliability and efficiency of the implemented integration algorithm.

Dirk Beyer, Stefan Löwe, Evgeny Novikov et al.

Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems, namely, 59 device drivers with 1119 revisions from the Linux kernel.

Evgeny Novikov, Anton Tuzov

In this paper we construct a third order method for solving additively split autonomous stiff systems of ordinary differential equations. The constructed additive method is L-stable with respect to the implicit part and allows to use an arbitrary approximation of the Jacobian matrix. In opposite to our previous paper, the fourth stage is explicit. So, the constructed method also has a good stability properties because of L-stability of the intermediate numerical formulas in the fourth stage, but has a lower computational costs per step. Automatic stepsize selection based on local error and stability control are performed. The estimations for error and stability control have been obtained without significant additional computational costs. Numerical experiments show reliability and efficiency of the implemented integration algorithm.