Some Symbolic Computation Issues In Program Verification And System Analysis

Formal method is an effective approach to develop trustworthy softwares and safety-critical systems. It is also one of the most important topics in trustworthy computing. Trustworthy computing pursues the reliable computing services, whom need to be proved by rigorously mathematical reasoning. Formal method stares at the specification, develop-ment, checking and verification of software and hardware systems, specially for proving the correctness of programs and analyzing the safety of systems. Their core tasks include liveness, safety, fairness, termination, invariant, synchronization, asynchronization, ex-clusion, reachability, duration, stability and so on.For the problems in program verification and system analysis, the traditional logic method can not determine the whole safety since it would suffer from the state space ex-plosion and fail to find out all bugs. And purely numerical computation would involve floating-point errors, thus affects the reliability in large. So recent research resorts to symbolic computation, which places excessive emphasis on the absolute exactness, that is, reducing the problem of checking safety properties to that of solving algebraic systems. More importantly, this method is quite feasible and promising owing to the increasing-powerful computer performance and the growing-mature computer mathematics.The main contributions of this thesis are as follows:1. Theory:The real root isolation problems in several generalized polynomials are well studied. Based on M. Achatz's work (2008), we present a tip of continued fraction for approaching to the transcendent number ex and compute the exact value with interval arithmetic, thus improve the existing algorithm for isolating the real roots of exponential polynomials. In the meanwhile, we also develop the construc-tion of pseudo-derivative sequences for power-exponential polynomials, prove the generalized Budan-Fourier theorem for them, and give an algorithm for isolating their positive roots approximately.2. Application:We dedicate the above theoretic results to the fields of program ver-ification and system analysis. On one hand, we present an algorithm for estimat-ing the real root bounds of multi-exponential polynomials, to supplement the re-sult about the termination of linear loops in A. Tiwari's work (2004). Under his termination-deciding method, a nonterminating input can be further constructed as an counterexample for the given nonterminating loop, which makes the result more complete. On the other hand, we successfully decide the reachability of linear sys-tems by the algorithms of isolating those generalized polynomials'real roots. We remove the restriction that the matrices of linear systems must be diagonalizable and enlarge the scope of input functions, thus enrich G. Lafferrierre's work (2001).3. Software:Based on the computer algebra system MAPLE, we provide a program package REACH, which can exactly solve the arbitrary system consisting of expo-nential polynomial equations and inequalities. It implements mathematics mecha-nization of deciding the reachability of rational eigenvalue linear systems, and can be integrated into verification tools for general hybrid systems.