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

CPBPV: a constraint-programming framework for bounded program verification

14th international conference on principles and practice of constraint programming (CP 2008)

作者： Collavizza, Helene Rueher, Michel Van Hentenryck, Pascal Univ Nice Sophia Antipolis CNRS I3S F-06903 Sophia Antipolis France Brown Univ Providence RI 02912 USA

ISBN: (纸本)3540859578

this paper studies how to verify the conformity of a program with its specification and proposes a novel constraint-programming framework for bounded program verification (CPBPV). the CPBPV framework uses constraint stores to represent both the specification and the program and explores execution paths of bounded length nondeterministically. the CPBPV framework detects non-conformities and provides counter examples when a path of bounded length that refutes some properties exists. the input program is partially correct under the boundness restrictions, if each constraint store so produced implies the post-condition. CPBPV does not explore spurious execution paths, as it incrementally prunes execution paths early by detecting that the constraint store is not consistent. CPBPV uses the rich language of constraint programming to express the constraint store. Finally, CPBPV is parameterized with a list of solvers which are tried in sequence, starting with the least expensive and less general. Experimental results often produce orders of magnitude improvements over earlier approaches, running times being often independent of the size of the variable domains. Moreover, CPBPV was able to detect subtle errors in some programs for which other frameworks based on bounded model checking have failed.

关键词： Bounded program verification constraint-based symbolic execution Detection of nonconformities Test cases generation

来源：评论

学校读者我要写书评

暂无评论

An Integrated Business Rules and constraints Approach to Data Centre Capacity Management

An Integrated Business Rules and Constraints Approach to Dat...

引用

16th Annual international conference on the principles and practice of constraint programming

作者： van der Krogt, Roman Feldman, Jacob Little, James Stynes, David Univ Coll Cork Cork Constraint Computat Ctr Dept Comp Sci Cork Ireland

ISBN: (纸本)9783642153952

A recurring problem in data centres is that the constantly changing workload is not proportionally distributed over the available servers. Some resources may lay idle while others are pushed to the limits of their capacity. Tins in turn leads to decreased response times on the overloaded servers, a situation that the data centre provider wants to prevent. To solve this problem, an administrator may move (reallocate) applications or even entire virtual servers around in order to spread the load. Since there is a cost associated with moving applications (in the form of down time during the move, for example), we are interested in solutions with minimal changes. this paper describes a hybrid approach to solving such resource reallocation problems in data centres, where two technologies have to work closely together to solve this problem in an efficient manner. the first technology is a Business Rules Management System (BRMS), which is used to identify which systems are considered to be overloaded on a systematic basis. Data centres use complex rules to track the behaviour of the servers over time, in order to properly identify overloads. Representing these tracking conditions is what the BRMS is good for. It defines the relationships (business constraints) over time between different applications, processes and required resources that are specific to the data centre. As such, it also allows a high degree of customisation. Having identified which servers require reallocation of their processes, the BRMS then automatically creates an optimisation model solved with a constraint programming (CP) approach. A CP solver finds a feasible or the optimal solution to this CSP, which is used to provide recommendations on which workload should be moved and whereto. Notice that our use of a hybrid approach is a requirement, not a feature: employing only rules we would not be able to compute an optimal solution;using only CP we would not be able to specify the complex identification

关键词： constraint theory

来源：评论

学校读者我要写书评

暂无评论

Testing continuous double auctions with a constraint-based oracle

Testing continuous double auctions with a constraint-based o...

引用

16th international conference on principles and practice of constraint programming, CP 2010

作者： Castañeda Lozano, Roberto Schulte, Christian Wahlberg, Lars KTH - Royal Institute of Technology Sweden Cinnober Financial Technology AB Stockholm Sweden

Computer trading systems are essential for today9;s financial markets where the trading systems9; correctness is of paramount economical significance. Automated random testing is a useful technique to find bugs ... 详细信息

ISBN: (纸本)364215395X

Computer trading systems are essential for today's financial markets where the trading systems' correctness is of paramount economical significance. Automated random testing is a useful technique to find bugs in these systems, but it requires an independent system to decide the correctness of the system under test (known as oracle problem). this paper introduces a constraint-based oracle for random testing of a real-world trading system. the oracle provides the expected results by generating and solving constraint models of the trading system's continuous double auction. constraint programming is essential for the correctness of the test oracle as the logic for calculating trades can be mapped directly to constraint models. the paper shows that the generated constraint models can be solved efficiently. Most importantly, the approach is shown to be successful by finding errors in a deployed financial trading system and in its specification. © 2010 Springer-Verlag.

关键词： Commerce

来源：评论

学校读者我要写书评

暂无评论

A new framework for sharp and efficient resolution of NCSP with manifolds of solutions

引用

14th international conference on principles and practice of constraint programming (CP 2008)

作者： Goldsztejn, Alexandre Granvilliers, Laurent CNRS Lab Informat Nantes Atlantique Nantes France Univ Nantes Lab Informat Nantes Atlantique Nantes France

ISBN: (纸本)3540859578

When numerical CSPs are used to solve systems of n equations with n variables, the preconditioned interval Newton operator plays two key roles: First it allows handling the n equations as a global constraint, hence achieving a powerful contraction. Second it can prove rigorously the existence of solutions. However, none of these advantages can be used for under-constrained systems of equations, which have manifolds of solutions. A new framework is proposed in this paper to extend the advantages of the preconditioned interval Newton to under-constrained systems of equations. this is achieved simply by allowing domains of the NCSP to be parallelepipeds, which generalize the boxes usually used as domains.

关键词： Interval analysis Branch and prune algorithm Preconditioned interval Newton Global constraint for under-constrained systems of equations

来源：评论

学校读者我要写书评

暂无评论

A branch and bound algorithm for numerical Max-CSP

引用

14th international conference on principles and practice of constraint programming (CP 2008)

作者： Normand, Jean-Marie Goldsztejn, Alexandre Christie, Marc Benhamou, Frederic Univ Nantes LINA Nantes France Univ Barcelona EVENT Lab Barcelona Spain Univ Nantes CNRS Nantes France INRIA IRISA Rennes France

ISBN: (纸本)3540859578

the constraint Satisfaction Problem (CSP) framework allows users to define problems in a declarative way, quite independently from the solving process. However, when the problem is over-constrained, the answer "no solution" is generally unsatisfactory. A Max-CSP P-m = < V, D, C > is a triple defining a constraint problem whose solutions maximize the number of satisfied constraints. In this paper, we focus on numerical CSPs, which are defined on real variables represented as floating point intervals and which constraints are numerical relations defined in intension. Solving such a problem (i.e., exactly characterizing its solution set) is generally undecidable and thus consists in providing approximations. We propose a Branch and Bound algorithm that provides under and over approximations of a solution set that maximize the maximum number m(P) of satisfied constraints. the technique is applied on three numeric applications and provides promising results.

关键词： Numerical Max-CSP constraint programming Numerical constraints

来源：评论

学校读者我要写书评

暂无评论

An MDD-based generalized arc consistency algorithm for positive and negative table constraints and some global constraints

引用

constraintS 2010年第2期15卷 265-304页

作者： Cheng, Kenil C. K. Yap, Roland H. C. Chinese Univ Hong Kong Dept Comp Sci & Engn Hong Kong Hong Kong Peoples R China Natl Univ Singapore Sch Comp Singapore 117548 Singapore

A table constraint is explicitly represented as its set of solutions or non-solutions. this ad hoc (or extensional) representation may require space exponential to the arity of the constraint, making enforcing GAC expensive. In this paper, we address the space and time inefficiencies simultaneously by presenting the mddc constraint. mddc is a global constraint that represents its (non-)solutions with a multi-valued decision diagram (MDD). the MDD-based representation has the advantage that it can be exponentially smaller than a table. the associated GAC algorithm (called mddc) has time complexity linear to the size of the MDD, and achieves full incrementality in constant time. In addition, we show how to convert a positive or negative table constraint into an mddc constraint in time linear to the size of the table. Our experiments on structured problems, car sequencing and still-life, show that mddc is also a fast GAC algorithm for some global constraints such as sequence and regular. We also show that mddc is faster than the state-of-the-art generic GAC algorithms in Gent et al. (2007), Lecoutre and Szymanek (2006), Lhomme and R,gin (2005) for table constraint.

关键词： Ad hoc constraint Global constraint Table constraint Positive constraint Negative constraint Multi-valued decision diagram Generalized arc consistency

来源：评论

学校读者我要写书评

暂无评论

An MDD-based generalized arc consistency algorithm for positive and negative table constraints and some global constraints

An MDD-based generalized arc consistency algorithm for posit...

引用

14th international conference on principles and practice of constraint programming (CP 2008)

作者： Cheng, Kenil C. K. Yap, Roland H. C. Chinese Univ Hong Kong Dept Comp Sci & Engn Hong Kong Hong Kong Peoples R China Natl Univ Singapore Sch Comp Singapore 117548 Singapore

关键词： Ad hoc constraint Global constraint Table constraint Positive constraint Negative constraint Multi-valued decision diagram Generalized arc consistency

来源：评论

学校读者我要写书评

暂无评论

On-line timetabling software

On-line timetabling software

引用

8th international conference on the practice and theory of Automated Timetabling, PATAT 2010

作者： Devin, Florent Le Nir, Yannick EISTI 26 avenue des Lilas 64062 Pau Cedex 9 Guadeloupe

Timetable design is a really important and difficult task. Timetable handbuilding consumes a lot of time. In this paper we address two main difficulties of automatic timetabling, that is data acquisition and timetable computation. the former task is made using new advanced technologies in the area of Rich Internet Application. this offers very powerful, and easy to use, interfaces to acquire data. the latter task is the computation of the timetable itself. We use the constraint programming and one implementation in swi-prolog to compute the timetable. Finally we show some results of our application on a real case study.

关键词： Scheduling

来源：评论

学校读者我要写书评

暂无评论

A new hybrid tractable class of soft constraint problems

A new hybrid tractable class of soft constraint problems

引用

16th international conference on principles and practice of constraint programming, CP 2010

作者： Cooper, Martin C. Živný, Stanislav IRIT University of Toulouse III 31062 Toulouse France Computing Laboratory University of Oxford OX1 3QD Oxford United Kingdom

ISBN: (纸本)364215395X

the constraint satisfaction problem (CSP) is a central generic problem in artificial intelligence. Considerable effort has been made in identifying properties which ensure tractability in such problems. In this paper we study hybrid tractability of soft constraint problems;that is, properties which guarantee tractability of the given soft constraint problem, but properties which do not depend only on the underlying structure of the instance (such as being tree-structured) or only on the types of soft constraints in the instance (such as submodularity). We firstly present two hybrid classes of soft constraint problems defined by forbidden subgraphs in the structure of the instance. these classes allow certain combinations of binary crisp constraints together with arbitrary unary soft constraints. We then introduce the joint-winner property, which allows us to define a novel hybrid tractable class of soft constraint problems with soft binary and unary constraints. this class generalises the SoftAllDiff constraint with arbitrary unary soft constraints. We show that the joint-winner property is easily recognisable in polynomial time and present a polynomial-time algorithm based on maximum-flows for the class of soft constraint problems satisfying the joint-winner property. Moreover, we show that if cost functions can only take on two distinct values then this class is maximal. © 2010 Springer-Verlag.

关键词： constraint satisfaction problems

来源：评论

学校读者我要写书评

暂无评论

RuLAM project: Speculative parallelization for java using software transactional memory

RuLAM project: Speculative parallelization for java using so...

引用

Work-in-Progress Session, P3JW 2010 - At the 8th international conference on the principles and practice of programming in Java, PPPJ 2010

作者： Anjo, Ivo Cachopo, João Rua Alves Redol 9 1000-029 Lisboa Portugal

the era of multicore processors, capable of running multiple tasks concurrently, has arrived. Sadly, most existing software and even new applications being developed are not ready to take advantage of these new multiprocessing capabilities, and, thus, more processing cores do not translate into better performance when executing these applications. To tackle this problem, we envision the creation of a runtime environment that is able to parallelize automatically existing sequential applications without requiring any manual modification to those applications. To achieve this goal, we are exploring thread-level speculation supported by a Software Transactional Memory (STM), rather than relying on hardware-based mechanisms. In this paper, we present our work in the RuLAM project, which targets speculative parallelization on the Java platform.

关键词： Java programming language

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：