摘要：在设计中，甲、乙楼设想作为单层农村住宅建筑进行示范，丙、丁楼设想作为木结构住宅建筑进行示范，戊楼设想作为2-3层的农村住宅建筑进行示范，接待中心设想作为小型社区中心建筑进行示范，致力于探索适用于不同类型的新建农村住宅和住宅公建的生态设计及生态技术。

摘要：提出一种验证含栈指针、静态区指针操作的C语言程序的方法.该方法定义指针的三元属性表示一个指针的状态.指针的三元属性包括指针指向数据块的名称、数据块的长度以及指针在所指向数据块上的偏移.通过对Hoare逻辑的扩展,基于指针的三元属性设计了相应的断言演算规则和演算过程中生成验证条件的方法.该方法可以解决访问路径别名判断、指针越界访问检查、非法指针解引用检查等问题.该方法已经在一个基于演绎推理的安全C语言验证系统中实现,并且成功验证了教材上常用的一些经典算法.

摘要：在一个基于形状图逻辑的C语言程序自动验证系统上,设计并实现了二叉树形状程序的循环不变形状图的自动推断方法.该方法与单链表程序循环不变形状图的推断方法的区别在于通过增加二叉树形状的等价和蕴含规则,使得在形状图的演算时支持二叉树中不确定方向的展开和折叠.此外,为了解决形状图变换规则变化给循环不变形状图推断带来的问题,还设计了算法用以判断在推断循环不变形状图的过程中是否使用新增的规则,并将判断算法融合到循环不变形状图推断流程中.本文方法使得系统支持自动推断二叉树指针程序的循环不变形状图.

摘要：在一个基于霍尔逻辑和形状图逻辑的C语言自动验证器中,设计并实现了对形状图中所含易变数据结构的形状检查方法.本工作在验证器的形状系统中实现了显式形状检查与隐式形状检查,并通过引入不同的形状级别,使验证器能够根据不同的严格程度及时发现程序中不符合形状定义的易变数据结构,避免对形状图逻辑的相关演算造成影响.此外,为分解易变数据结构中不同指针域带来的复杂性,形状检查方法引入了三阶段处理框架:形状分割、形状分析及形状推断,分别实现形状图的预处理,针对指针指向与节点类型等方面进行分析,以及根据相关规则推断易变数据结构的形状级别.

摘要：程序性质的自动验证有时需要验证者提供相关的归纳引理,程序验证的结果可靠与否依赖于验证者所提供的归纳引理正确与否。本文围绕操作易变数据的程序的自动验证,设计并实现一个相关引理的自动证明器,作为程序自动验证器中检查验证者所提供的归纳引理是否正确的工具。该证明器分析所有待证归纳引理,构建引理之间的依赖关系图,得出引理的证明顺序。对每个引理,分析得出它的归纳变元和应采用的归纳方法,把归纳证明的各步交给自动定理证明器Z3进行证明。该证明器的原型已嵌入一个基于演绎推理的安全C语言自动验证系统中,并成功验证了有序链表、二叉搜索树、AVL树、伸展树等数据结构的性质。