本发明公开了一种基于约束求解器的自动形式验证方法与装置。针对C/C++源代码，编译为LLVMIR中间语言，在LLVMIR上自动构建符号执行模型，针对给定的源代码正确性属性形式化描述，使用符号执行的方式综合代码模型与代码属性，生成SMT约束，最后验证代码是否满足正确性属性，本发明使用约束求解器验证C/C++代码的正确性属性，通过符号执行编码C/C++代码为约束，根据使用约束求解器接口编写的代码正确性属性，可以验证不含无界循环的C/C++代码的正确性；针对引入无界循环代码的处理，通过使用循环不变式或有限展开循环，可以有限制地将循环编码为约束。