The 2017 Edition

http://cp2017.a4cp.org/related_events/



Pictures of the event can be found here.

Preliminary Plan:

8:30-9h15 Laurent Simon: Why SAT solvers are so efficient ? More questions than answers ! 

     SAT solvers are widely used in industry and model checking. However, somehow paradoxically, if we know how to build them, we lack any satisfying explanation for their efficiency.  In this talk, I will quickly present the history of SAT solvers, and explain how all the components of SAT solvers are turned towards efficiency rather than theory, making them really hard to understand. 

     I will raise some questions about their efficiency that still have no clear answers. This talk will be illustrated by a number of empirical evidences showing that CDCL solvers should probably be considered as complex systems, needing new methods to study them.
9h15-10:00 Michel Rueher: Searching Critical Counter Examples

    Programs with floating-point computations are often derived from mathematical models or designed with the semantics of the real numbers in mind. However, for a given input, the computed path with floating-point numbers may significantly differ from the path corresponding to the same computation with real numbers. Abstract interpretation based error analysis of finite precision implementations computes an over-approximation of the errors due to floating-point operations.  As a consequence, developers do not know whether the program can actually produce very unexpected outputs.   
    In this talk, I will first introduce a constraint-based approach that searches for test cases in the part of the over-approximation where errors due to floating-point arithmetic could lead to unexpected decisions. The point is that the search of such counter-examples is a long, tedious and costly task for programs performing floating point computations. Indeed, available search strategies for constraints systems are dedicated to finite domains and, to a lesser extent, to continuous domains. So, in the second part of the talk, I will introduce new strategies dedicated to floating point constraints. They take advantage of the properties of floating point domains and of floating point constraints to improve the search for floating point constraint problems. Preliminary experiments on a set of realistic benchmarks show that such dedicated strategies outperform standard search and splitting strategies.
10:00-10:30 Coffee break
10:30-11:15 Marie Pelleau : AbSolute: From Static Analyzer to Constraint Solver
      Abstract Interpretation is a method to design approximate semantics of programs and provide sound answers to questions about their run-time behaviors. Constraint Programming aims at solving, with reusable techniques, hard combinatorial problems expressed declaratively.

      I will show how to apply Abstract Interpretation techniques to Constraint Programming. More precisely how to use abstract domains in order to solve Constraint Satisfaction Problems.
11:15-12:00 Quentin Plazar : Efficient and Complete FD-Solving for Extended Array Constraints.

     Array constraints are essential for handling data structures in automated reasoning and software verification. Unfortunately, the use of a typical finite domain (FD) solver based on local consistency-based filtering has strong limitations when constraints on indexes are combined with constraints on array elements and size. This paper proposes an efficient and complete FD-solving technique for extended constraints over (possibly unbounded) arrays. We describe a simple but particularly powerful transformation for building an equisatisfiable formula that can be efficiently solved using standard FD reasoning over arrays, even in the unbounded case. Experiments show that the proposed solver significantly outperforms FD solvers, and successfully competes with the best SMT-solvers.
12:00-13:30
  Lunch break
13:30-14:30 Christian Schulte (bio): Rethinking Code Generation in Compilers.

     Code generation in compilers can be improved by using constraint programming (CP) as a method for solving combinatorial optimization problems. The talk presents how register allocation (assigning program variables to processor registers) and instruction scheduling (reordering processor instructions to increase throughput) can be modeled and solved using CP.

     The combinatorial model that integrates global register allocation with instruction scheduling captures advanced aspects such as ultimate coalescing, spill code optimization, register packing, and multiple register banks. The model is significant as it addresses the same aspects as traditional code generation algorithms, yet is simple and can robustly generate code. The generated code is better than code generated with traditional approaches, such as LLVM as a state-of-the-art compiler infrastructure.

     The talk will include a brief sketch of the Unison project that implements the model as an open-source project on top of LLVM. Joint work with Mats Carlsson, Roberto Castañeda Lozano, Frej Drejhammar, and Gabriel Hjort Blindell.
14:30-15:30 Xavier Urbain (bio): Towards Formal Proof for Swarms of Mobile Robots

     Mobile robot networks emerged in the past few years as a promising distributed computing model, and received increasing attention from the Distributed Computing community. On the one hand, the use of cooperative swarms of inexpensive robots to achieve various complex tasks in potentially hazardous environments is a promising option to reduce human and material costs and assess the relevance of Distributed Computing in a practical setting. On the other hand, execution model differences warrant extreme care when revisiting "classical results'' from Distributed Computing, as very small changes in assumed hypotheses may completely change the feasibility of a particular problem. 

     To ensure the correctness of distributed protocols in that context, formal methods have recently been applied to robotic swarms, namely model-checking, program synthesis, and mechanised formal proof.  I will present a formal proof framework for localised distributed protocols in mobile robotic networks, based on the Coq Proof Assistant. The framework allows for a relatively easy specification of context, protocols, and properties. It was successfully used to certify impossibility results, and to establish formally the correctness of distributed protocols.
15:30-16:00 Coffee break
16:00-17:00 Vijay Ganesh (bio): On The Unreasonable Effectiveness of Boolean SAT Solvers

     Modern conflict-driven clause-learning (CDCL) Boolean SAT solvers routinely solve very large industrial SAT instances in relatively short periods of time. This phenomenon has stumped both theoreticians and practitioners since Boolean satisfiability is an NP-complete problem widely believed to be intractable. It is clear that these solvers somehow exploit the structure of real-world instances. However, to-date there have been few results that precisely characterize this structure or shed any light on why these SAT solvers are so efficient. 
     In this talk, I will present results that provide a deeper empirical understanding of why CDCL SAT solvers are so efficient, which may eventually lead to a complexity-theoretic result. Our results can be divided into two parts. First, I will talk about structural parameters that can characterize industrial instances and shed light on why they are easier to solve even though they may contain millions of variables. Second, I will talk about internals of CDCL SAT solvers, and describe why they are particularly suited to solve industrial instances.
17:00-18:00 Discussion on the future of the workshop's theme

See a summary of the speaker's short bio here.

Submissions

The 8th CSTVA edition invites all interested participants to submit an abstract of a talk to be presented during the workshop, through Easychair, at the following address:



Talks may present both original or already published work, tool developments as well as work in progress. Talks with emphasis on novel ideas or challenges are particularly welcome! Abstracts of at most three pages (excluding references), in text or PDF form, should be submitted by the deadline given below.

 Submission deadline
Notification date
Workshop date
June 25th, 2017 
July 7th, 2017
August 28th, 2017


The talks most compliant with the workshop theme and objectives will be selected for presentation in a full-day workshop. For all inquiries, please contact the main organizers.

Proceedings

The workshop will not require paper submission and will not publish proceedings, but the presenters will be invited to submit the slides of their talks for publication on the workshop website. This makes the CSTVA workshop particularly suited as a first occasion to present novel work.

All researchers and practitioners interested in the scope of the workshop, whether presenters or not, are invited to attend the workshop and to participate in discussions.

Organization

The 8th edition of CSTVA will take place at the CP2017 conference in Melbourne, Australia. This year, CP is collocated with SAT, ICLP and follows IJCAI. In addition, it offers two tracks, one for CP and Verification, and one for CP and SAT, making it an ideal venue for this year's CSTVA edition.

Organizing committee

  •     Sébastien Bardin (CEA, France)
  •     Zakaria Chihani (CEA, France)
  •     Arnaud Gotlieb  (Simula, Norway)
  •     Nikolai Kosmatov (CEA, France)

Steering committee
  •     Sébastien Bardin (CEA, France)
  •     Pierre Flener (Uppsala University, Sweden)
  •     Vijay Ganesh (University of Waterloo, Canada)
  •     Arnaud Gotlieb (Simula, Norway)
  •     Nicky Williams (CEA, France)