检索结果-内蒙古大学图书馆

3rd International TOOLympics Challenge

作者： De Angelis, Emanuele Krishnan, Hari Govind Vediramana CNR IASI Rome Italy Univ Waterloo Waterloo ON Canada

ISBN: (纸本)9783031676949;9783031676956

Constrained Horn Clauses (CHC) are a fragment of first-order logic that is expressive enough to represent many important software verification tasks, yet practical for fully automatic techniques. CHCs are used to verify the safety of hardware, software, and hybrid systems, infer refinement types, analyse program termination, and prove the correctness of smart contracts, among other applications. Over the years, many researchers have developed a variety of tools to check the satisfiability of CHCs. CHC-COMP strives to bring together these research efforts and compare the effectiveness of different CHC solvers on a unified set of benchmarks. Each year, CHC-COMP collects benchmarks provided by the CHC community, organizes them into tracks, and evaluates CHC solvers against those tracks. This annual competition is now in its sixth year. This report gives an overview of CHC-COMP and details of its sixth edition.

关键词： Constrained Horn Clauses constraint logic programming Satisfiability Modulo Theories constraint Solving

来源：评论

学校读者我要写书评

暂无评论

A Flexible Framework to Ensure Traceability, Consistency, and Propagation of KPIs Evolution

引用

JOURNAL OF SOFTWARE-EVOLUTION AND PROCESS 2025年第2期37卷

作者： Dominguez, Eladio Perez, Beatriz Rubio, angel L. Zapata, Maria A. Univ Zaragoza Dept Informat & Ingn Sistemas Zaragoza Spain Univ La Rioja Dept Matemat & Comp La Rioja Spain

Organizations use key performance indicators (KPIs) to assess the effectiveness and efficiency of their procedures and processes. In a world that is constantly evolving and hyperconnected via the internet, it is of great interest to analyze how changes (organizational, legal, technological or other) can lead to modifications in the KPIs involved. However, little attention has been paid to KPI evolution either in the scientific literature or in developed solutions. This paper presents A Flexible Framework for the Evolution, Consistency and Traceability of KPIs (AFFECTK) that aims at establishing the basis for suitable KPIs' evolution management. The feasibility of this proposal is demonstrated through a proof-of-concept developed using a reasoning tool based on constraint logic programming. The framework is further evaluated, using real KPI case studies, to assess the functional suitability of our approach.

关键词： consistency conditions constraint logic programming evolution framework KPIs propagation reasoning traceability

来源：评论

学校读者我要写书评

暂无评论

A Transformation-based implementation for CLP with qualification and proximity

引用

THEORY AND PRACTICE OF logic programming 2014年第1期14卷 1-63页

作者： Caballero, R. Rodriguez-Artalejo, M. Romero-Diaz, C. A. Univ Complutense Fac Informat Dept Sistemas Informat & Computac Madrid 28040 Spain

Uncertainty in logic programming has been widely investigated in the last decades, leading to multiple extensions of the classical logic programming paradigm. However, few of these are designed as extensions of the well-established and powerful constraint logic programming (CLP) scheme for CLP. In a previous work we have proposed the proximity-based qualified constraint logic programming (SQCLP) scheme as a quite expressive extension of CLP with support for qualification values and proximity relations as generalizations of uncertainty values and similarity relations, respectively. In this paper we provide a transformation technique for transforming SQCLP programs and goals into semantically equivalent CLP programs and goals, and a practical Prolog-based implementation of some particularly useful instances of the SQCLP scheme. We also illustrate, by showing some simple - and working - examples, how the prototype can be effectively used as a tool for solving problems where qualification values and proximity relations play a key role. Intended use of SQCLP includes flexible information retrieval applications.

关键词： constraint logic programming program transformation qualification domains and values similarity and proximity relations flexible information retrieval

来源：评论

学校读者我要写书评

暂无评论

Phase-coupled mapping of data flow graphs to irregular data paths

引用

DESIGN AUTOMATION FOR EMBEDDED SYSTEMS 1999年第2-3期4卷 119-165页

作者： Bashford, S Leupers, R Univ Dortmund Dept Comp Sci 12 D-44221 Dortmund Germany

Many software compilers for embedded processors produce machine code of insufficient quality. Since for most applications software must meet tight code speed and size constraints, embedded software is still largely developed in assembly language. In order to eliminate this bottleneck and to enable the use of high-level language compilers also for embedded software, new code generation and optimization techniques are required. This paper describes a novel code generation technique for embedded processors with irregular data path architectures, such as typically found in fixed-point DSPs. The proposed code generation technique maps data flow graph representation of a program into highly efficient machine code for a target processor modeled by instruction set behavior. High code quality is ensured by tight coupling of different code generation phases. In contrast to earlier works, mainly based on heuristics, our approach is constraint-based. An initial set of constraints on code generation are prescribed by the given processor model. Further constraints arise during code generation based on decisions concerning code selection, register allocation, and scheduling. Whenever possible, decisions are postponed until sufficient information about a good decision has been collected. The constraints are active in the "background" and guarantee local satisfiability at any point of time during code generation. This mechanism permits to simultaneously cope with special-purpose registers and instruction level parallelism. We describe the detailed integration of code generation phases. The implementation is based on the constraint logic programming (CLP) language ECLiPSe. For a standard DSP, we show that the quality of generated code comes close to hand-written assembly code. Since the input processor model can be edited by the user, also retargetability of the code generation technique is achieved within a certain processor class.

关键词： code generation embedded processors phase coupling constraint logic programming

来源：评论

学校读者我要写书评

暂无评论

Typing Linear constraints

引用

ACM TRANSACTIONS ON programming LANGUAGES AND SYSTEMS 2010年第6期32卷 21-21:42页

作者： Ruggieri, Salvatore Mesnard, Fred Univ Pisa Dipartimento Informat I-56127 Pisa Italy Univ Reunion IREMIA LIM F-97715 St Denis Messag 9 France

We present a type system for linear constraints over the reals intended for reasoning about the input-output directionality of variables. Types model the properties of definiteness, range width or approximation, lower and upper bounds of variables in a linear constraint. Several proof procedures are presented for inferring the type of a variable and for checking validity of type assertions. We rely on theory and tools for linear programming problems, linear algebra, parameterized polyhedra and negative constraints. An application of the type system is proposed in the context of the static analysis of constraint logic programs. Type assertions are at the basis of the extension of well-moding from pure logic programming. The proof procedures (both for type assertion validity and for well-moding) are implemented and their computational complexity is discussed. We report experimental results demonstrating the efficiency in practice of the proposed approach.

关键词： Languages Verification Linear constraints polyhedra constraint logic programming well-moding definiteness

来源：评论

学校读者我要写书评

暂无评论

Hierarchical constraint satisfaction of multilateral trade matching in commodity auction markets

引用

ANNALS OF OPERATIONS RESEARCH 1997年第s期71卷 317-334页

作者： Ryu, YU UNIV TEXAS DEPT DECIS SCIRICHARDSONTX 75083

A commodity auction market provides a trading intermediary whose role is to find optimal trade matching between buyers and sellers that satisfies their trading constraints. Some commodity auction markets utilize forms of electronic trading intermediary systems in order to improve the efficiency and effectiveness of trading of huge volumes of transactions during short periods of time. Previous research works on electronic trading intermediary systems focus on the maximization of the trade volume obtained by satisfying mainly price and quantity constraints. The principal restriction of these approaches is that the heterogeneity of the commodity is ignored or at least not significantly considered. The objective of the study in this paper is to propose a computable mechanism of trading intermediaries for commodity auction markets, supporting not only ordinary trading constraints of prices and quantities but also other qualitative and quantitative constraints on the commodity properties and trading conditions.

关键词： commodity auction market constraint logic programming electronic market hierarchical constraint reasoning stable matching

来源：评论

学校读者我要写书评

暂无评论

A distributed constraint-based scheduler

引用

ARTIFICIAL INTELLIGENCE IN ENGINEERING 1997年第2期11卷 91-105页

作者： Lamma, E Mello, P Milano, M DEIS Vide Risorgimento 2 I-40136 Bologna Italy

This paper presents the design and implementation of a distributed advisory system which helps different human experts in the management and control of traffic within railway stations and along railway branches. Our approach allows the management of a whole railway line in a modular, expandable and scalable way. The scheduling of trains along a railway line is performed by several modules each one controlling a certain number of resources. These modules solve the scheduling of trains by interacting and communicating with each other. Each module has to deal with temporal constraints, priority between trains and constraints due to the structure of the station and railway branches. Our approach is based on the constraint logic programming (CLP) paradigm for solving the constraints involved in the problem. Therefore, this paper shows the versatility and adequacy of the CLP approach for the problems of this type. (C) 1997 Elsevier Science Ltd.

关键词： railway traffic control scheduling temporal reasoning constraint logic programming distribution

来源：评论

学校读者我要写书评

暂无评论

Effective algorithm for handling constraints in generator maintenance scheduling

引用

IEE PROCEEDINGS-GENERATION TRANSMISSION AND DISTRIBUTION 2002年第3期149卷 274-282页

作者： Huang, KY Yang, HT Cheng Shiu Inst Technol Dept Elect Engn Kaohsiung 833 Taiwan Chung Yuan Christian Univ Dept Elect Engn Chungli 32023 Taiwan

An effective algorithm for handling constraints to solve the generator maintenance scheduling (GMS) problem is presented. The proposed algorithm of constraint logic programming (CLP) synthesises logic programming, constraint satisfaction technique (CST), and branch and bound search schemes to provide an efficient and flexible approach to the problem. The constraints of the problem cannot only be conveniently managed by the logic programming but also be actively used to reduce the search space by the CST. Once the infeasible solutions are pruned away from the search space, the depth-first branch and bound search strategy is then used for determining the optimal solution. The practical GMS problem of Taiwan Power (Taipower) system is solved by the proposed CLP algorithm for demonstrating its effectiveness. To exhibit the efficiency of the proposed algorithm, the results obtained are compared with those from the established methods of simulated annealing (SA) and lagrangian relaxation (LR).

关键词： search space reduction Lagrangian relaxation logic programming Power engineering computing generator maintenance scheduling constraints handling maintenance engineering power engineering computing electric generators logic programming a.c. machines Taiwan Power Generating stations and plants simulated annealing Taipower Maintenance and reliability constraint handling branch and bound search schemes constraint logic programming constraint satisfaction technique depth-first branch and bound search strategy d.c. machines power generation scheduling Plant engineering, maintenance and safety

来源：评论

学校读者我要写书评

暂无评论

A hybrid approach to the single line scheduling problem with multiple products and sequence-dependent time

引用

COMPUTERS & INDUSTRIAL ENGINEERING 2003年第4期45卷 573-583页

作者： Spina, R Galantucci, LM Dassisti, M Politecn Bari DIMeG I-70126 Bari Italy

The present paper presents a hybrid approach for solving manufacturing scheduling problems, based on the integration between constraint logic programming (CLP) and Genetic Algorithm (GA) approaches. The proposed methodology is applied to a single line with multiple products and sequence-dependent time. This system model derives from a real case of a company producing sheets for catalytic converters. A sensitivity analysis of the hybrid methodology is carried out to compare the performance of the CLP, GA and integrated CLP-GA approaches. (C) 2003 Elsevier Ltd. All rights reserved.

关键词： scheduling genetic algorithm constraint logic programming

来源：评论

学校读者我要写书评

暂无评论

Using OBDDs to handle dynamic constraints

引用

INFORMATION PROCESSING LETTERS 1997年第3期62卷 111-120页

作者： Bouquet, F Jegou, P CMI CNRSURA 1787LIMF-13453 MARSEILLE 13FRANCE

For many real-life problems naturally modelled as constraints systems, we have to manage dynamically systems of constraints. So, a model based on the formalism of finite constraint Satisfaction Problems (CSPs) (Montanari, 1974) has been proposed with Dynamic CSPs (DCSPs) to handle this kind of problem (Dechter and Dechter, 1988;Janssen et al., 1990). Some classical techniques defined in the field of CSPs are usable in DCSPs, but the management of dynamicity induces new problems such as management of over-constrained systems and consistency maintenance. At present, constraint programming tools generally do not offer a framework for integrating dynamic constraints. The purpose of this paper is to introduce an efficient way to solve DCSPs based on a logical approach. We use and extend Ordered Binary Decision Diagrams (OBDDs) (Bryant, 1986) and propose a particular coding for dynamicity. We show that our approach allows to solve some major questions in the field of DCSPs. (C) 1997 Elsevier Science B.V.

关键词： algorithms constraint satisfaction dynamic constraints Ordered Binary Decision Diagrams constraint logic programming

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：