软件系统验证中李雅普诺夫不变量的优化（扩展版）
系统与控制
2011-08-30 v1 软件工程
最优化与控制
摘要
本文提出了一种用于数值软件系统验证的控制论框架，并将软件验证作为控制与系统理论的一个重要应用加以推进。其核心思想是将李雅普诺夫函数及其相关的计算技术从控制系统分析和凸优化领域迁移到各类软件安全性与性能规约的验证中。这些规约包括但不限于：无溢出、无除零错误、有限时间内终止、死代码的存在性以及某些用户自定义断言。该框架的核心是李雅普诺夫不变量。这些不变量是适当构造的程序变量函数，并沿执行轨迹满足某些类似于李雅普诺夫函数特性的性质。对不变量的搜索可形式化为一个凸优化问题。若该优化问题可行，其结果即为相应规约的一个证明凭证。
引用
@article{arxiv.1108.5622,
title = {Optimization of Lyapunov Invariants in Verification of Software Systems (Extended Version)},
author = {Mardavij Roozbehani and Alexandre Megretski and Eric Feron},
journal= {arXiv preprint arXiv:1108.5622},
year = {2011}
}
备注
50 pages, 5 figures. This is the long version with more details. Short version available at: http://arxiv.org/abs/1108.0170