CP meets Verification 2016 Workshop

Constraint programming (CP) is a programming paradigm for the modelling and solving of constrained problems, such as complex problems in resource allocation, scheduling, configuration, and design. The success of CP comes from the fact that it provides high-level languages for declaratively modelling a problem by means of constraints that capture combinatorial substructures (and by means of an objective function) and for writing an efficient search procedure that solves the problem.

Computer-aided program verification has found widespread applications in both academia and industry in ensuring that systems are dependable and secure. The discipline is based on fundamental mathematical theories such as logic and automata, and covers algorithmic techniques for formal analysis and synthesis, such as model checking, satisfiability (SAT) solving, and satisfiability modulo theories (SMT). These techniques have become essential tools for the design and analysis of hardware and software systems.

This workshop gathers researchers and practitioners from constraint programming (CP), formal verification, and software engineering, in order to address the CP-based solving of challenging constraint problems in formal verification and software engineering. Solvers of CP technology are orthogonal but complementary to solvers of technologies like SAT, SAT modulo theories (SMT), integer programming (IP), and mixed integer programming (MIP).

The objectives of this workshop are:

• The delegates with a non-CP background present challenging constraint problems in formal verification and software engineering, as well as current solution approaches (whether ad hoc or based on SAT, SMT, IP, or MIP technology), towards an investigation on using a (hybrid with a) CP solver.
• The delegates with a CP background present either CP solvers or how they have successfully used CP technology for challenging constraint problems in formal verification and software engineering.
• All delegates, whether presenters or not, discuss synergy opportunities as well as challenges in formal verification, software engineering, and the underlying constraint solving tools.

As the workshop aims at fostering lively discussions and debates between participants, it will be organized around:

• several invited talks given by experts of the corresponding domains,
• accepted talks based on a lightweight reviewing of submitted abstracts (see call for contributions),
• space for questions and discussions.

This workshop follows a first edition as a one-week seminar in 2012 (CP meets CAV 2012) and a second edition co-located with CP 2014 (CP meets Verification 2014).

Call for Contributions

The CP meets Verification 2016 workshop invites all interested participants to submit an abstract of a talk to be presented during the workshop. 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 one page, in text or PDF form, should be submitted by Email by the deadline given below. 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.

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.

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.

Important Dates

• July 2016
• Submission

  July 4, 2016

• Notification

  July 15, 2016

• September 2016
• CP meets Verification 2016 Workshop

  September 5, 2016

List of talks

Invited talks given by:

“Model-Constructing Satisfiabilty Calculus”,
Dejan Jovanović, SRI International, USA.

I'll present the MCSAT approach to solving satisfiability modulo theory (SMT) problems. The MCSAT framework builds on the ideas found in modern CDCL-style SAT solvers and generalizes them to first-order setting. Although the main ideas in MCSAT come from SAT solving, in the first-order setting there are many connections to CP: a MCSAT solver operates over a domain where it maintains local consistency using dedicated propagators. The appeal of the new approach is its simplicity, deductive power, extensibility, and effectiveness on real-world problems. MCSAT has been very successful in attacking complex domains such as non-linear real and integer arithmetic.

Dejan Jovanović is a computer scientist in the Computer Science Laboratory at SRI International. His research interests are automated reasoning, satisfiability, and model-checking. He is involved in development of Yices2 and CVC4 SMT solvers. He received his Ph.D. degree in computer science from New York University.

“Constraint Satisfaction over Bit-Vectors”,
Laurent Michel, University of Connecticut, USA

Reasoning over bit-vectors arises in a variety of applications in verification and cryptography. This talk considers a bit-vector domain for constraint programming and its associated filtering algorithms. The domain supports all the traditional bit operations and correctly models modulo-arithmetic and overflows. The domain implementation uses bit operations of the underlying architecture, avoiding the drawback of a bit-blasting approach. The filtering algorithms implement either domain consistency on the bit-vector domain or bit consistency. Filtering algorithms for logical and structural constraints typically run in constant time, while arithmetic constraints such as addition run in time linear in the size of the bit-vectors. The talk will discuss how to channel bit-vector variables with an integer variable and how to make use of the infrastructure to tackle problems commonly found in the Bit Vector Theory of the SMT-LIB benchmark suite. This is a joint work with P. Van Hentenryck (U. Michigan) , G. Johnson (U. Connecticut).

Laurent's primary research interests lie at the intersection of Programming Language and Combinatorial Optimization. His efforts are directed to the construction of software tools that considerably simplify the development of complex application (most belong to the NP class) for discrete and continuous optimization problems. He co-authored COMET, the first Platform for Constraint-Based Local Search and is now focusing on the Objective-CP systems meant to support hybrid efforts in optimization technology. The open-source and hybrid-friendly platform features a clean separation of modeling from solving and search and features a diverse collection of constraint technologies including LP, MIP, CP, CBLS. Its CP capabilities including finite domain reasoning, reasoning over the reals, floats and bit-vectors.

“Challenges of Program Verification with SPARK”,
Yannick Moy, AdaCore, France

SPARK is an industrially supported formal verification toolset for critical software written in the Ada programming language. SPARK technology is based on the Why3 intermediate language and toolset for formal program verification, and the Alt-Ergo, CVC4 and Z3 automatic provers. SPARK is used to formally verify properties of critical software ranging from absence of run-time errors to functional correctness. Current challenges for automatic proof are the ability to deal with nonlinear arithmetic, conversions between types (bitvectors, integers, floats, reals), handling of floating-point arithmetic and the combination of all these with quantification arising from both user specifications and the encoding of programming language specifications. We present the achievements of current projects ProofInUse and SOPRANO, and the roadmap for better use of automatic provers in formal program verification.

Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK 2014, a product he presents in articles, conferences, classes and blogs (in particular www.spark-2014.org ). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.

“The use of Constraint Programming in testing and analysis of a telecommunication protocol”,
Justin Pearson, Uppsala University, Sweden

In this talk I will summarise some of the work that I have been doing in collaboration with Ericsson and SICS on using constraint programming to model telecommunication protocols. The case study used is the Public Warning System service, which is a part of the Long Term Evolution (LTE) 4G standard. Various parts of the protocol were modelled in MiniZinc, which allowed the derivations of test cases and the ability analysis existing protocol logs. Very early on we were able to find errors in an existing bespoke test harness for this protocol. I will talk about the general approach and how other protocols could be modelled and the use of constraint programming as a test harness.

Justin Pearson is a senior lecturer(Docent) at the department of IT at Uppsala University. His main focus of research is on constraint programming, its theory, its implementation through propagator design, and its applications. He has worked on applications of constraint programming in diverse areas from air-traffic control with Eurocontrol, to software testing with Ericsson. His research in software testing has included the use of using constraint programming to model a complex telecommunications protocol in order to derive test cases and analyse real protocol logs. His work on implementation and propagator design has included work on string variables and their associated global constraints. String variables and constraints are of particular interest in software verification.

“Network Verification: When less is more, but not always.”
Andrey Rybalchenko, Microsoft Research, Cambridge, UK.

We are building a new logic engine, called Network Logic Solver, to support the verification of Microsoft networks. In addition to dealing with the large scale of the problem, our engine must cope with a logic extended with operations used to model routing protocols: specifically, aggregation (min, max) and non-monotonic negation. These features make the problem significantly harder to solve, and are not tackled by tools currently developed in (software) verification community. This is a joint work with Nuno Lopes.

Andrey Rybalchenko is a senior researcher at Microsoft Research. He focuses on automated methods and tools for formal software and network verification. In the past, Andrey was a professor at Technische Universität München, a researcher at Max Planck Institute for Software Systems, EPFL, MSR Cambridge, Max Planck Institute for Informatics, and University of Saarland. Andrey was selected for MIT TR35 (2010) and Otto Hahn Medal (2005), received an ERC Starting grant (2012) and a Microsoft Research European Fellowship (2006).

“Optimization Modelling for Software Developers, or How to convert procedural code to constraints!”,
Peter Stuckey, University of Melbourne, Australia.

Software developers are an ideal channel for the distribution of discrete optimization (DO) technology. Unfortunately, including even basic optimisation functionality in an application currently requires the use of an entirely separate paradigm with which most software developers are not familiar. We suggest an alternative interface to DO designed to overcome this barrier. The interface allows an optimisation problem to be defined in terms of procedures rather than decision variables and constraints. Optimisation is seamlessly integrated into a wider application through automatic conversion between this definition and a conventional model solved by an external solver.

The core of the method is translating procedural object oriented code into constraints. This translation is also useful for other applications such as symbolic execution of the code, e.g. in Congolic testing. We discuss how to create the best translation of procedural code, better than existing DO and SMT approaches, and how we can translate bounded loops more effectively. Finally we briefly describe a global constraint for reaching definitions, which encapsulates the essential problem of converting procedural code to constraints.

This work is joint with Kathryn Francis.

Peter Stuckey is a Professor in Computer Science at the University of Melbourne. His research interests focus on constraints and constraint solving, which has widespread use in discrete optimization, program analysis, constraint based graphics, and bioinformatics. He has a long standing interest in (constraint) programming/modelling languages having helped develop CLP(R), HAL, Zinc and MiniZinc.

Accepted regular talks:

• Mohammed Said Belaid, Claude Michel, Yahia Lebbah and Michel Rueher.
  On Finding program input values maximizing the rounding-off error.
• Marie Pelleau, Emmanuel Rauzy, Ghiles Ziat, Charlotte Truchet and Antoine Miné.
  Mixing Polyedra and Boxes Abstract Domain for Constraint Solving.
• Zakaria Chihani.
  Tight coupling between bit-vector and integer domains can surpass bit-blasting SMT solvers.
• Anicet Bart, Benoît Delahaye, Éric Monfroy and Charlotte Truchet.
  An Improved Constraint Programming Model for Parametric Interval Markov Chain Verification.
• Mehdi Maamar, Noureddine Aribi, Nadjib Lazaar, Yahia Lebbah and Samir Loudni.
  F-CPminer* : A new approach for fault localization using constraint-based data mining.

Proceedings and Presentation Slides

It is not planned to publish workshop proceedings. Presentation slides will be published online on the workshop webpage.

Chairs

• Sébastien Bardin, CEA LIST, France
• François Bobot, CEA LIST, France
• Nikolai Kosmatov, CEA LIST, France

Contact: cpmeetsverif16@cea.fr