形式化方法是开发高可信软件和安全攸关系统的有效途径,是高可信计算的研究重点之一。高可信计算追求软件和系统提供可信赖的计算服务能力,而这种可信赖性是建立在严格数学证明上的。形式化方法主要研究软硬件系统的规格描述、开发过程、以及检测验证,特别是程序正确性证明和系统安全性分析。研究的问题有活性、安全性、公平性、终止性、不变式、同步、异步、互斥、可达性、持续性、稳定性等。在处理这些程序和系统中的分析与验证问题时,传统的逻辑方法会因为状态空间爆炸而无法检测出全部错误,不能彻底地保证安全性；单纯数值计算又会产生浮点误差,影响整体的可靠性。因而,近年来研究者正在尝试使用以绝对准确性为目标的符号计算方法来处理它们,即将这些性质的检验问题转换成代数系统的求解问题。特别是随着计算机性能和计算机数学的不断发展,为开展该方向的研究提供了强有力的支撑。本文的主要贡献由以下几部分组成：1.理论部分：主要研究了若干种广义多项式的实根隔离问题。在M. Achatz等人2008年的工作基础上,提出了用连分数技巧逼近超越数ex和区间算术思想进行准确计算,改进了现有指数多项式实根隔离算法；同时对于幂指数多项式,推广了伪导数序列的构造方法,证明了广义Budan-Fourier定理对其仍然成立,并给出一个正根隔离近似算法。2.应用部分：主要尝试了将上述理论成果应用在程序验证和系统分析领域。方面,利用估计多指数多项式实根界算法,完善了A.Tiwari在2004年关于线性循环终止性的结论。在其终止性可判定理论的基础上,对于给定非终止循环构造出其非终止输入作为反例,使该结果更加完整。另一方面,将广义多项式实根隔离算法用于判定线性系统的可达性问题,除去了线性系统矩阵的可对角化限制,丰富了输入函数的类型,扩展了G.Lafferrierre等人在2001年的结果。3.软件部分：主要在计算机代数系统MAPLE下编制了程序包REACH,能够准确求解任意由指数多项式等式和不等式所组成系统,实现了判定有理特征值线性系统可达性的数学机械化,能集成在一般混成系统的验证工具中。