Using Satisfiability Modulo Theories for Inductive Verification of Lustre Programs

The problem of verifying safety properties of Lustre programs with integer arithmetic have been attacked in several different ways. Abstract interpretation is used in NBAC, and inductive verification using a SAT solver is used in Luke.This paper presents a method of using Satisfiability Modulo Theories (SMT) as an incremental decision procedure for inductive verification of Lustre program. We show that even a very naive approach using SMT is competitive and in some instances complementary to other approaches.     

An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types

The theory of recursive data types is a valuable modeling tool for software verification. In the past, decision procedures have been proposed for both the full theory and its universal fragment. However, previous work has been limited in various ways. In this paper, we present a general algorithm for the universal fragment. The algorithm is presented declaratively as a set of abstract rules which are terminating, sound, and complete. We show how other algorithms can be realized as strategies within our general framework. Finally, we propose a new strategy and give experimental results showing that it performs well in practice.     

求解极小SMT不可满足子式的宽度优先搜索算法

极小不可满足子式能够为可满足性模理论(SMT)公式的不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误.针对极小SMT不可满足子式的求解问题,提出了SMT公式搜索树及其3类结点的概念,并给出了不可满足子式、极小不可满足子式与3类结点之间的映射关系.基于这种映射关系,采用宽度优先的搜索策略提出了宽度优先搜索的极小SMT不可满足子式求解算法.基于业界公认的SMT Competition 2007测试集进行实验的结果表明,该算法能够有效地求解极小不可满足子式.     

Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)

The Satisfiability Modulo Theories Competition (SMT-COMP) arose from the SMT-LIB initiative to spur adoption of common, community-designed formats, and to spark further advances in satisfiability modulo theories (SMT). The first SMT-COMP was held in 2005 as a satellite event of CAV 2005. SMT-COMP 2006 was held August 17–19, 2006, as a satellite event of CAV 2006. This paper describes the rules and competition format for SMT-COMP 2006, the benchmarks used, the participants, and the results.     

On Variable-inactivity and Polynomial Formula-Satisfiability Procedures

Verification problems require to reason in theories of datastructures and fragments of arithmetic. Thus, decision proceduresfor such theories are needed, to be embedded in, or interfacedwith, proof assistants or software model checkers. Such decisionprocedures ought to be sound and complete, to avoid false negativesand false positives, efficient, to handle large problems, andeasy to combine, because most problems involve multiple theories.The rewrite-based approach to decision procedures aims at addressingthese sometimes conflicting issues in a uniform way, by harnessingthe power of general first-order theorem proving. In this article,we generalize the rewrite-based approach from deciding the satisfiabilityof sets of ground literals to deciding that of arbitrary groundformulæ in the theory. Next, we present polynomial rewrite-basedsatisfiability procedures for the theories of records with extensionalityand integer offsets. The generalization of the rewrite-basedapproach to arbitrary ground formulæ and the polynomialsatisfiability procedure for the theory of records with extensionalityuse the same key property—termed variable-inactivity—thatallows one to combine theories in a simple way in the rewrite-basedapproach.     

Using Resolution for Testing Modal Satisfiability and Building Models

This paper presents a translation-based resolution decision procedure for the multimodal logic K _(m)(,,) defined over families of relations closed under intersection, union, and converse. The relations may satisfy certain additional frame properties. Different from previous resolution decision procedures that are based on ordering refinements, our procedure is based on a selection refinement, the derivations of which correspond to derivations of tableaux or sequent proof systems. This procedure has the advantage that it can be used both as a satisfiability checker and as a model builder. We show that tableaux and sequent-style proof systems can be polynomially simulated with our procedure. Furthermore, the finite model property follows for a number of extended modal logics.     

基于图分解的(3,4)-CNF公式的可满足性

对于规则的(3,4)-CNF公式F,公式F对应的因子图GF恰好是一个(3,4)-双向正则二部图.利用正则二部图的有关性质,证明了对于任意的(3,4)-CNF公式F,若其对应的因子图GF能够被划分为两个(3,2)-双向正则二部图,则F是可满足的.     

The Procedures of the CADE-13 ATP System Competition

This article describes the practical procedures that were used to run the CADE-13 ATP System Competition. The article describes the hardware and software environments, the system installation, the soundness testing performed, the preparation of problems for the competition, the choice of the number of problems and the time limit, and the execution of the systems.     

MathSAT: Tight Integration of SAT and Mathematical Decision Procedures

Recent improvements in propositional satisfiability techniques (SAT) made it possible to tackle successfully some hard real-world problems (e.g., model-checking, circuit testing, propositional planning) by encoding into SAT. However, a purely Boolean representation is not expressive enough for many other real-world applications, including the verification of timed and hybrid systems, of proof obligations in software, and of circuit design at RTL level. These problems can be naturally modeled as satisfiability in linear arithmetic logic (LAL), that is, the Boolean combination of propositional variables and linear constraints over numerical variables. In this paper we present MathSAT, a new, SAT-based decision procedure for LAL, based on the (known approach) of integrating a state-of-the-art SAT solver with a dedicated mathematical solver for LAL. We improve MathSAT in two different directions. First, the top‐level line procedure is enhanced and now features a tighter integration between the Boolean search and the mathematical solver. In particular, we allow for theory-driven backjumping and learning, and theory-driven deduction; we use static learning in order to reduce the number of Boolean models that are mathematically inconsistent; we exploit problem clustering in order to partition mathematical reasoning; and we define a stack-based interface that allows us to implement mathematical reasoning in an incremental and backtrackable way. Second, the mathematical solver is based on layering; that is, the consistency of (partial) assignments is checked in theories of increasing strength (equality and uninterpreted functions, linear arithmetic over the reals, linear arithmetic over the integers). For each of these layers, a dedicated (sub)solver is used. Cheaper solvers are called first, and detection of inconsistency makes call of the subsequent solvers superfluous. We provide a through experimental evaluation of our approach, by taking into account a large set of previously proposed benchmarks. We first investigate the relative benefits and drawbacks of each proposed technique by comparison with respect to a reference option setting. We then demonstrate the global effectiveness of our approach by a comparison with several state-of-the-art decision procedures. We show that the behavior of MathSAT is often superior to its competitors, both on LAL and in the subclass of difference logic. This work has been partly supported by ISAAC, a European-sponsored project, contract no. AST3-CT-2003-501848; by ORCHID, a project sponsored by Provincia Autonoma di Trento; and by a grant from Intel Corporation. The work of T. Junttila has also been supported by the Academy of Finland, project 53695. S. Schulz has also been supported by a grant of the Italian Ministero dell'Istruzione, dell'Università e della Ricerca and the University of Verona.     

浅谈世界技能大赛网站设计开发项目的应赛方案

世界技能大赛中的网站设计开发项目是指根据项目需求制作站点设计,实现能在各种终端上使用的页面、交互效果以及后台功能的竞赛项目。文章通过对该赛项和赛题的分析,结合作者几年指导参赛经验,针对如何做好应赛工作,提出了多方面的策略、措施和方法,重点论述了参赛选手指导方案。     

The Results - of the CADE-13 ATP System Competition

The CADE-13 ATP System Competition tested 18 ATP systems on 50 theorems, in five competition categories, with a time limit of 300 seconds imposed on each system run. This article records the results of the competition. Some analysis of these results is given, and interesting points are highlighted.     

Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures

Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication, abstract encryption/decryption. In this report we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions.     

The Design of the CADE-13 ATP System Competition

Running a competition for automated theorem proving (ATP) systems is a difficult and arguable venture. However, the potential benefits of such an event by far outweigh the controversial aspects. The motivations for running the CADE-13 ATP System Competition were to contribute to the evaluation of ATP systems, to stimulate ATP research and system development, and to expose ATP systems to researchers both within and outside the ATP community. This article identifies and discusses the issues that determine the nature of such a competition. Choices and motivated decisions for the CADE-13 competition, with respect to the issues, are given.     

平面广告设计课程的国际竞赛项目培养模式探析

国际竞赛项目是平面广告设计课程最富挑战的特色内容。它以学生为主体,教师为主导,以竞赛为载体,以真实项目为驱动,是一种理论与实践教学有机结合的高效教学方法。本文针对国际竞赛项目培养教育模式的实践内容和措施进行了积极地探讨。     

机器人足球仿真比赛回放平台的设计与实现

机器人足球仿真比赛回放平台在国内还不够成熟,因此设计一个回放平台帮助策略设计者通过比赛的回放分析策略是十分必要的。本文主要介绍机器人足球仿真比赛回放平台的结构设计和具体功能实现。该平台使用多线程技术和双缓冲技术,能够流畅地回放机器人足球仿真比赛。     

基于TRIZ冲突解决原理的多Agent人机协调设计系统

简要介绍了TRIZ冲突解决原理的基本概念、原理和解题思路。在此基础上提出了传统创新设计平台存在的问题和不足，包括不支持冲突发现、不能根据TRIZ通用解演绎创新解、很难集成现有的CAD系统、价格高、专业性差以及不适应分布式网络运行环境等。基于JADE开发工具，研究并设计了一个基于TRIZ冲突解决原理，支持冲突发现的人机协调设计平台，同时探讨了系统开发和实现的关键技术。     

体育竞赛场馆大屏幕显示与监控系统设计

提出了体育竞赛场馆大屏幕显示与监控系统的总体设计方案,系统采用C/S结构模式,利用可扩展性标记语言XML进行数据交换,实现了体育竞赛场馆大屏幕现代化的信息显示服务.系统已成功地在“第十一届全国运动会”赛事中使用,结果表明,该系统的性能完全能够满足大型运动会竞赛场馆大屏幕显示的需要.     

一种竞赛用机器人的设计与实现

为提高机器人在准确分拣前提下快速完成搬运任务的能力,对传统自动分拣搬运机器人从策略选择、硬件组成和外观结构进行了全新的设计,提出了一种竞赛用自动分拣搬运机器人的设计与实现方法。针对竞赛要求采用全新设计的非航行推测算法;硬件模块化设计,核心控制器采用了国内少见的双核形式,并采用多种传感器来满足竞赛要求;通过避障与路径选择的仿真调试,确定了机器人的外观结构及竞赛路径。实践检验了设计的有效性和先进性,研究结果对于提高竞赛用机器人的性能具有一定的参考价值。     

依托程序设计竞赛,提高计算机专业学生培养质量

程序设计能力是计算机专业学生最重要的能力之一。本文总结过去几年组织学生开展程序设计竞赛的经验,探索出一条运用程序设计竞赛提高学生程序设计能力的新途径,从而可为提高计算机专业学生的培养质量,进一步拓宽创新素质教育提供参考。     

From Numerical Intervals to Set Intervals (Interval-Related Results Presented at the First International Workshop on Applications and Theory of Random Sets)

Reliable Computing -