Domenico Salvagnin - Integration of AI and OR techniques in constraint programming: 14th international conference, CPAIOR 2017, Padua, Italy, June 5-8, 2017: proceedings

Integration of AI and OR techniques in constraint programming: 14th international conference, CPAIOR 2017, Padua, Italy, June 5-8, 2017: proceedings — read online for free the complete book (whole text) full work

Below is the text of the book, divided by pages. System saving the place of the last page read, allows you to conveniently read the book "Integration of AI and OR techniques in constraint programming: 14th international conference, CPAIOR 2017, Padua, Italy, June 5-8, 2017: proceedings" online for free, without having to search again every time where you left off. Put a bookmark, and you can go to the page where you finished reading at any time.

Light

Font size:

↓

↑

Georgia Tahoma Arial Verdana

Reset

Interval:

↓

↑

Bookmark:

Make

1234567...223

Technical Papers

Springer International Publishing AG 2017

Domenico Salvagnin and Michele Lombardi (eds.) Integration of AI and OR Techniques in Constraint Programming Lecture Notes in Computer Science 10335 10.1007/978-3-319-59776-8_1

Sharpening Constraint Programming Approaches for Bit-Vector Theory

Zakaria Chihani 1

(1)

CEA, LIST, Software Security Lab, Gif-sur-Yvette, France

Zakaria Chihani (Corresponding author)

Email:

Bruno Marre

Email:

Franois Bobot

Email:

Sbastien Bardin

Email:

Abstract

We address the challenge of developing efficient Constraint Programming-based approaches for solving formulas over the quantifier-free fragment of the theory of bitvectors (BV), which is of paramount importance in software verification. We propose CP(BV), a highly efficient BV resolution technique built on carefully chosen anterior results sharpened with key original features such as thorough domain combination or dedicated labeling. Extensive experimental evaluations demonstrate that CP(BV) is much more efficient than previous similar attempts from the CP community, that it is indeed able to solve the majority of the standard verification benchmarks for bitvectors, and that it already complements the standard SMT approaches on several crucial (and industry-relevant) aspects, notably in terms of scalability w.r.t. bit-width, theory combination or intricate mix of non-linear arithmetic and bitwise operators. This work paves the way toward building competitive CP-based verification-oriented solvers.

Work partially funded by ANR under grants ANR-14-CE28-0020 and ANR-12-INSE-0002. The CP solver COLIBRI is generously sponsored by IRSN, the French nuclear safety agency.

Introduction

Context. Not so long ago, program verification was such an ambitious goal that even brilliant minds decided it was bound to fail []. At the time, the authors concluded their controversial paper saying that if, despite all their reasons, verification still seems an avenue worth exploring, so be it. And so it was. Today, software verification is a well established field of research, and industrial adoption has been achieved is some key areas, such as safety-critical systems.

Since the early 2000s, there is a significant trend in the research community toward reducing verification problems to satisfiability problems of first-order logical formulas over well-chosen theories (e.g. bitvectors, arrays or floating-point arithmetic), leveraging the advances of modern powerful SAT and SMT solvers [].

The problem. While SMT and SAT are the de facto standard in verification, a few teams explore how Constraint Programming (CP) techniques can be used in that setting [].

Yet, currently, there is no good CP-based resolution technique for (the quantifier-free fragment of) the theory of bitvectors [], i.e. fixed-size arrays of bits equipped with standard low-level machine instructions, which is of paramount importance in verification since it allows to encode most of the basic datatypes found in any programming language.

Goal and challenge. We address the challenge of developing efficient Constraint Programming-based approaches for solving formulas over the quantifier-free fragment of the theory of bitvectors (BV). Our goal is to be able to solve many practical problems arising from verification (with the SMTCOMP challenge].

Proposal and contributions. We propose CP(BV), a highly efficient BV resolution technique built on carefully chosen anterior results [] sharpened with key original features such as thorough domain combination or dedicated labeling. Extensive experimental evaluations demonstrate that CP(BV) is much more efficient than previous similar attempts from the CP community, that it is indeed able to solve the majority of the standard verification benchmarks for bitvectors, and that it already complements the standard SMT approaches on several crucial (and industry-relevant) aspects, notably in terms of scalability w.r.t. bit-width, theory combination or intricate mix of non-linear arithmetic and bitwise operators. Our main contributions are the following:

• We present CP(BV), an original framework for CP-based resolution of BV problems, which built on anterior results and extend them with several key new features in terms of thorough domain combination or dedicated labeling. This results in a competitive CP-based solver, excelling in key aspects such as scalability w.r.t. bitwidth and combination of theories. A comparison of CP(BV) with previous work is presented in Table .
• We perform a systematic and extensive evaluation of the effect of our different CP improvements on the efficiency of our implementation. This compares the options at our disposal and justifies those we retained, establishing a firm ground onto which future improvements can be made. It also shows the advantage of our approach relative to the other CP approaches applied to BV, and that our approach is able to solve a very substantial part of problems from the SMTCOMP challenge.
• Finally, we perform an extensive comparison against the best SMT solvers for BV problems, namely: Z3 []. This comparison exhibits the strenghts of CP over SMT approaches on particular instances. Specifically, our implementation surpasses several (and sometimes all ) solvers on some examples involving large bit-vectors and/or combination with floating-point arithmetic.

Table 1.

Overview of our method

	Bardin et al. []	Michel et al. []	CP(BV)
Bitvector domain	+	++	++ []
Arithmetic domain	++	+	++ []
Domain combination	+	+	++
Simplifications	+	x	++
BV-aware labeling	x	x	++
Implemented	Yes	No	Yes
Benchmark	Conjunctive formulas 200 formulas	Arbitrary formulas 30,000 formula

Discussion. Considering that our current CP(BV) approach is far from optimal compared to existing SMT solvers (implemented in Prolog, no learning), we consider this work as an important landmark toward building competitive CP-based verification-oriented solvers. Moreover, our approach clearly challenges the well-accepted belief that bitvector solving is better done through bitblasting, opening the way for a new generation of word-level solvers.

Motivation

The standard (SMT) approach for solving bit-vector problem, called bit-blasting [], we propose a high-level encoding of bitvector problems, seen as Constraint Satisfaction Problems (CSP) over finite (but potentially huge) domains. Each bitvector variable of the original BV problem is now considered as a (CSP) bounded-arithmetic variable, with dedicated domains and propagators.

Now illustrating with concrete examples, we show the kind of problems where our approach can surpass existing SMT solvers. Consider the three following formulas:

Next page

1234567...223

Light

Font size:

↓

↑

Georgia Tahoma Arial Verdana

Reset

Interval:

↓

↑

Bookmark:

Make

Similar books «Integration of AI and OR techniques in constraint programming: 14th international conference, CPAIOR 2017, Padua, Italy, June 5-8, 2017: proceedings»

Look at similar books to Integration of AI and OR techniques in constraint programming: 14th international conference, CPAIOR 2017, Padua, Italy, June 5-8, 2017: proceedings. We have selected literature similar in name and meaning in the hope of providing readers with more options to find new, interesting, not yet read works.

Bernabé Dorronsoro

Optimization and Learning: 4th International Conference, OLA 2021, Catania, Italy, June 21-23, 2021, Proceedings

Tomasz M. Gwizdałła (editor)

Cellular Automata: 14th International Conference on Cellular Automata for Research and Industry, ACRI 2020, Lodz, Poland, December 2–4, 2020, Proceedings (Lecture Notes in Computer Science, 12599)

Peter J. Stuckey

18th International Conference, CPAIOR 2021, Vienna, Austria, July 5–8, 2021, Proceedings

David Kreps

14th IFIP TC 9 International Conference on Human Choice and Computers, HCC14 2020, Tokyo, Japan, September 9–11, 2020, Proceedings

Pietrusiak Damian

Proceedings of the 13th International Scientific Conference: Computer Aided Engineering

Ortuño Guzmán Francisco M.

Bioinformatics and Biomedical Engineering: 5th International Work-Conference, IWBBIO 2017, Granada, Spain, April 26-28, 2017, Proceedings

Korytkowski Marcin.

Artificial Intelligence and Soft Computing: 16th International Conference, ICAISC 2017, Zakopane, Poland, June 11-15, 2017, Proceedings, Part I

Baumeister Hubert

Agile processes in software engineering and extreme programming: 18th International Conference, XP 2017, Cologne, Germany, May 22-26, 2017, proceedings

Amsaleg Laurent

MultiMedia Modeling: 23rd International Conference, MMM 2017, Reykjavik, Iceland, January 4-6, 2017, Proceedings, Part II

Amann Johanna

Passive and Active Measurement: 18th International Conference, PAM 2017, Sydney, NSW, Australia, March 30-31, 2017, Proceedings

Alves José C.

Robotic Sailing 2016 Proceedings of the 9th International Robotic Sailing Conference

Chen Weidong

Intelligent autonomous systems 14: proceedings of the 14th International Conference IAS-14

Discussion, reviews of the book Integration of AI and OR techniques in constraint programming: 14th international conference, CPAIOR 2017, Padua, Italy, June 5-8, 2017: proceedings and just readers' own opinions. Leave your comments, write what you think about the work, its meaning or the main characters. Specify what exactly you liked and what you didn't like, and why you think so.