现代操作系统、嵌入式系统、航电系统等安全关键系统一般都使用C/C++语言进行开发,因此针对C程序的运行时验证技术研究变得非常重要。主流的运行时验证技术主要针对程序的内存安全性和形式化规约进行检测,首先通过对C程序中与内存操作和规约相关的代码进行插桩,然后编译运行插桩后的C程序来验证原程序是否满足内存安全性和给定的规约。但是现有技术存在许多局限性。一方面,现有技术大都只能处理单线程的C程序,在多线程C程序的情况下,可能引起对运行时信息的竞争访问问题,从而导致错误的验证结果。另一方面,针对形式化规约的运行时验证技术大都通过串行的方式处理多监控器,在规约数量较多的情况下,多监控器的串行运行会导致运行时性能大大降低。针对以上的两个局限性,本文主要研究面向多线程C程序的运行时验证技术和多监控器的并行验证技术。具体工作和创新点包括:首先,针对内存安全性问题,我们提出了面向多线程C程序的运行时验证算法。该算法采用有锁哈希表或无锁哈希表对指针元数据进行插入、查找和删除等操作,使得插桩后的多线程C程序可以并发地对指针元数据进行访问,从而实现对多线程C程序内存安全性的运行时验证。第二,针对形式化规约的验证问题,我们提出了面向多线程C程序的形式化规约验证算法。该算法采用无锁队列来存储和处理程序产生的事件,进行入队和出队操作,使得插桩后多线程目标程序和监控器线程可以并行地对程序产生的事件序列进行访问,从而实现对多线程C程序形式化规约的运行时验证。第三,针对多监控器的验证问题,我们提出了一种并行验证算法,其基本原理是根据监控器规约的数量和可用线程的数量,将规约产生的监控器平均分配到多个验证线程上,用户线程通过信号量控制验证线程的运行,从而实现多监控器的并行运行。最后,基于以上新的验证算法,我们实现了工具Movec,并在MiBench和SARD测试集上与现有技术进行了对比实验。实验结果表明,对于内存安全性的验证,Movec比Addresssanitizer能检测出更多的错误,采用有锁哈希表产生的运行时负载与待验证程序的线程数正相关,而采用无锁可扩展哈希表产生的运行时负载与待验证程序的线程数无关。对于形式化规约的验证,采用无锁队列和并行验证可以有效地对多线程C程序的多个形式化规约进行并行的运行时验证,多监控器并行验证算法产生的运行时负载比串行验证算法减少了约40%。