作为一种形式化验证的主流方法，定理证明已被成功地应用于软件和硬件的验证。不同于模型检测技术，定理证明与状态无关，不存在状态空间爆炸问题，因此可用来验证有穷状态系统、无穷状态系统以及参数化系统。它将系统和期望的性质均描述为逻辑公式，然后利用一组公理和推理规则去构造系统公式蕴含性质公式的证明，从而达到验证系统满足性质的目的。本文研究了基于命题投影时序逻辑的定理证明技术。命题投影时序逻辑(Propositional Projection Temporal Logic, PPTL)基于命题区间时序逻辑(Propositional Interval Temporal Logic,PITL)引入了新投影操作符prj，投影加操作符prj⊕，以及无穷模型。PPTL同时具备可判定性和完全ω正则表达力，能够描述顺序、并行、选择、循环等多种程序行为。为充分利用二者的优点，提出了一个完备的命题投影时序逻辑公理系统，包括公理和推理规则，常用定理以及合理性和完备性证明。使得对待验证系统的建模，期望性质的描述，以及系统模型满足期望性质的验证可在同一符号体系下完成。其中合理性证明基于PPTL模型理论，完备性的证明依赖于不动点理论和任何PPTL公式均可被转化成范式这一事实。给出的进程互斥用例说明了这一方法的可行性。基于给出的命题投影时序逻辑的公理系统，本文研究了实时系统的验证方法。以最早截止期优先调度算法为例，验证算法对任务集可行性的充要条件，即Liu and Layland定理。用建模、仿真和验证语言(Modeling, Simulation and VerificationLanguage, MSVL)描述算法，用PPTL公式描述性质，由于实现该算法的MSVL程序可被转化为PPTL公式，则可采用PPTL公理系统对其验证。除此，本文还研究了基于命题投影时序逻辑公理系统的硬件系统验证。以全加器和超前进位加法器为例说明了基于PPTL公理系统对硬件验证的一般方法。随着多核处理器的发展，多核并行程序的开发、规范及验证已经成为一个挑战。为描述多核并行程序不同进程之间的自治、并发和通信，基于投影时序逻辑(Projection Temporal Logic, PTL)提出了柱面计算模型(Cylinder Computation Model,CCM)。柱面计算模型以细粒度区间为公共时间轴，围绕在它周围的粗粒度区间形成一个柱面。执行在粗粒度区间上的进程被看做分布在不同核上的进程，这些进程在公共的投影点上完成通信，因此该模型可用来描述任意多核的并行计算。研究了CCM的模型理论，包括给出序列表达式的语法、语义和代数性质。序列表达式具有正则表达式的特点，用来灵活控制进程的执行，体现了进程的自治。在序列表达式的基础上给出了CCM的语法语义和逻辑定律。CCM体现了进程之间的并发。为执行CCM程序需将CCM嵌入到MSVL中，因此研究了CCM的操作语义和对应操作符的实现算法。文字处理器的实例说明了利用CCM对多核并行程序进行建模的方法。