计算机软硬件技术的快速发展，使得软件的应用渗透到了社会的各个领域，从手机到internet，软件在人们的生活中扮演着重要的角色。然而，随着软件复杂性的提高，软件开发的质量和效率却不能令人满意。软件常常发生故障，对人们的工作生活带来不利影响，甚至造成巨大损失，特别是对软件可靠性和安全性要求很高的航空航天技术。因此，如何在软件的开发和运行中保证软件的正确性、可靠性和安全性等高可信性质成为了软件理论和技术的重要研究内容。于是，出现了程序验证技术的研究方向。本文从程序验证的一个侧面提出了验证软件正确性的一个技术软件水印验证编译器技术，该技术从软件来源的源头开始，保障了软件的正确性、可靠性和安全性，使得软件开始使用时就能保证它是正确的，减少了软件出错的概率。从而防止了合法软件数据被非法篡改导致的软件失效，带来严重后果。同时揭示出软件的侵权行为，保护了版权所有者的合法利益，保障了软件的安全性。　　现今，互联网技术的普及提高使软件侵权者能够容易的获取所需软件，并使用逆向工程（Reverse-Engineering）和再工程（Re-Engineering）技术对软件进行非法分析和改造，从中窃取对侵权者有用的代码或数据，使得软件的正确性和安全性失去保障。所以，互联网在给软件产业带来高效率的同时，也同时带来了不同程度的危害。因此，人们如何从软件来源的源头上，即当软件开始使用时，就能确保它具有正确、可靠和安全的可信性质，保证软件不被非法利用和侵犯，从而筑起软件保护的第一道屏障，是软件开发者广泛关注的问题。　　对软件的保护可在侵权行为发生之前或之后进行。在侵权行为发生之前，开发者可以利用软件加密、防篡改、代码混淆或程序验证等技术对软件进行处理，增加侵权者分析和改造软件的难度，提高盗用软件的成本。但是，这种技术大多需要对软件进行较大幅度的修改，并依赖于特定的软硬件环境，从一定程度上影响了软件的扩展性、移植性和执行效率。而随着软件复杂度的提高，这种技术给软件性能带来的影响变得更加明显。为弥补现有技术的不足，一种新的软件保护技术——软件水印验证编译器技术——被提出并逐步受到人们的关注。软件水印验证编译器技术的基本思想是：将一个包含版权信息（如软件版权所有者、开发者或合法使用者）的水印嵌入到软件中，在软件被盗用后，通过特殊的验证过程将水印从侵权软件中验证出来，然后利用编译器技术实现该验证过程。　　本文首先介绍实现软件水印验证编译器技术的程序验证和编译系统相关知识，然后再介绍软件水印的基本概念和一种典型的软件水印技术——动态图软件水印技术，以及一个基于该技术的验证编译器原型系统的实现方法。