本发明公开一种面向C程序源码的程序可信性验证方法及装置，涉及软件安全领域，包括以下步骤，判断C程序源码是否符合编译器的规范要求，实施预处理，预处理后的C程序源码进入编译器的语法分析，生成控制流图，通过类型检查符号化，将安全性质添加到符号模型检测模块，再经过静态单赋值，形成符号公式系统，使用逻辑公式求解系统对符号公式系统进行逻辑公式转换，生成逻辑公式，将逻辑公式接入逻辑求解系统，从逻辑求解系统获取是否可满足结论，确定源码是否存在缺陷，解决C程序源码未能通过测试解决的潜在缺陷问题，以及基于定理证明等形式化验证方法效率低的问题，以静态方式实施运行时错误的检测，与传统测试技术方法形成互补。