Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves

This article describes the formal verification of a compilation algorithm that transforms parallel moves (parallel assignments between variables) into a semantically-equivalent sequence of elementary moves. Two different specifications of the algorithm are given: an inductive specification and a functional one, each with its correctness proofs. A functional program can then be extracted and integrated in the Compcert verified compiler.     

Semi-Automatic Composition of Loop Transformations for Deep Parallelism and Memory Hierarchies

Modern compilers are responsible for translating the idealistic operational semantics of the source program into a form that makes efficient use of a highly complex heterogeneous machine. Since optimization problems are associated with huge and unstructured search spaces, this combinational task is poorly achieved in general, resulting in weak scalability and disappointing sustained performance. We address this challenge by working on the program representation itself, using a semi-automatic optimization approach to demonstrate that current compilers offen suffer from unnecessary constraints and intricacies that can be avoided in a semantically richer transformation framework. Technically, the purpose of this paper is threefold: (1) to show that syntactic code representations close to the operational semantics lead to rigid phase ordering and cumbersome expression of architecture-aware loop transformations, (2) to illustrate how complex transformation sequences may be needed to achieve significant performance benefits, (3) to facilitate the automatic search for program transformation sequences, improving on classical polyhedral representations to better support operation research strategies in a simpler, structured search space. The proposed framework relies on a unified polyhedral representation of loops and statements, using normalization rules to allow flexible and expressive transformation sequencing. Thisrepresentation allows to extend the scalability of polyhedral dependence analysis, and to delay the (automatic) legality checks until the end of a transformation sequence. Our work leverages on algorithmic advances in polyhedral code generation and has been implemented in a modern research compiler.     

BLP改进模型的形式化描述及自动化验证

在《信息安全技术操作系统安全技术要求》中,提出访问验证保护级安全操作系统的研发过程需要完全形式化的安全策略模型。针对该情况,对经典的数据机密性BLP模型进行相应改进,为系统中的主客体引入多级安全标签以及安全迁移规则,使其满足实际系统开发的需求。运用完全形式化的方法对改进模型的状态、不变量、迁移规则等进行描述,使用Isabelle定理证明器证明了迁移规则对模型的不变量保持性,从而实现对模型正确性的自动形式化验证,并保证了模型的可靠性。     

微内核架构文件系统的形式化设计与验证方法研究

文件系统作为数据存储和管理的功能模块,其正确性是操作系统安全性的重要方面.采用形式化方法对微内核架构文件系统进行设计,使用操作系统对象语义模型(OSOSM)框架提出微内核架构文件系统的状态自动机模型,并依此描述系统调用的功能语义和系统状态转换,分析和归纳文件系统的功能正确性断言.以实现的微内核安全操作系统(Verified Trusted Oper-ating System,VTOS)为例,阐述在Isabelle/HOL定理证明器环境中构建状态自动机模型的方法,并对VTOS文件系统的形式化设计和功能正确性断言进行一致性验证,结果显示,VTOS文件系统的设计和实现符合预期的正确性规格说明.     

基于E语言和C参考模型的IP功能验证方案

提出并实现了一种基于E语言和C参考模型的IP功能验证方案。该方案能够自动生成验证向量并自动完成仿真结果的正确性判断,可以解决验证的充分性和验证时间之间的矛盾。使用这种方案可以有效地提高功能验证效率和质量,缩短设计周期,降低设计成本。     

Web服务质量建模及其正确性验证

针对现有的Web服务质量模型主要考虑的都是通用的服务质量属性,没有考虑特定的Web服务属性在评价中的作用,提出了一个新的Web服务质量模型,它引入了一个特定领域的服务质量属性,该模型包括三个子模型。模型中建立了相关的服务质量树和目标对象树,通过量化指标子模型对目标对象进行量化,形成相应的服务权重树。该模型既可适应用于单个的Web服务请求,也可以用于多个服务组合而成的请求。通过一个应用实例验证了模型的正确性和可用性。     

Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function

We present a new technique for verification of complex hardware devices that allows both generality and a high degree of automation. The technique is based on our new way of constructing a light-weight completion function together with new encoding of uninterpreted functions called reference file representation.Our technique combines our completion function method and reference file representation with compositional model checking and theorem proving. This extends the state of the art in two directions. First, we obtain a more general verification methodology. Second, it is easier to use, since it has a higher degree of automation.As a benchmark, we take Tomasulo's algorithm for scheduling out-of-order instruction execution used in many modern superscalar processors like the Pentium-II and the PowerPC 604. The algorithm is parameterized by the processor configuration, and our approach allows us to prove its correctness in general, independent of any actual design.     

3D通用人脸模型的自适应算法及应用

利用3D人脸建模的方法进行人脸识别有效地克服了2D人脸识别系统中识别率易受光照、姿态、表情影响的缺陷。文章采用一种依据人脸图像对3D通用人脸模型进行自适应调整的有效算法,构造出特定的人脸模型并运用于人脸识别中。通过比较从人脸图像中估算出的特征点与通用人脸模型在图像平面上的投影点之间的关系,对3D通用人脸模型进行全局和局部调整,以适应人脸中眼、口、鼻的个性化特征。最后以一个实例说明了此算法的应用。