Loading…
CP 2016 has ended
Workshop: Verification [clear filter]
Monday, September 5
 

09:00

CP meets Verification - Invited talk: Challenges of Program Verification with SPARK
    See presentations
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.

Moderators
Speakers
avatar for Yannick Moy

Yannick Moy

Senior Software Engineer, AdaCore SAS
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... Read More →


Monday September 5, 2016 09:00 - 09:35
B202 Bosco building

09:00

CP meets Verification Workshop
  • 09:00. Openning
  • 09:00 - 09:35. Invited talk: Challenges of Program Verification with SPARK, Yannick Moy. Abstract: 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.
  • 09:35 - 10:00. Regular talk: Mixing Polyedra and Boxes Abstract Domain for Constraint Solving, Marie Pelleau, Emmanuel Rauzy, Ghiles Ziat, Charlotte Truchet, Antoine Miné.

Speakers
avatar for Yannick Moy

Yannick Moy

Senior Software Engineer, AdaCore SAS
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... Read More →
avatar for Marie Pelleau

Marie Pelleau

UPMC - Lip6


Monday September 5, 2016 09:00 - 10:00
B202 Bosco building

09:35

CP meets Verification Workshop
    See presentations
  • 09h35-10h00: Mixing Polyedra and Boxes Abstract Domain for Constraint Solving, Marie Pelleau, Emmanuel Rauzy, Ghiles Ziat, Charlotte Truchet, Antoine Miné.

Moderators
Speakers
avatar for Marie Pelleau

Marie Pelleau

UPMC - Lip6


Monday September 5, 2016 09:35 - 10:00
B202 Bosco building

10:30

CP meets Verification - Invited talk: Model-Constructing Satisfiabilty Calculus
    See presentations
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.

Moderators
Speakers
avatar for Dejan Jovanovic

Dejan Jovanovic

SRI International
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... Read More →


Monday September 5, 2016 10:30 - 11:05
B202 Bosco building

11:05

CP meets Verification - Invited talk: Optimization Modelling for Software Developers, or How to convert procedural code to constraints!
    See presentations
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.

Moderators
Speakers
avatar for Peter Stuckey

Peter Stuckey

Professor, University of Melbourne and Data61
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... Read More →


Monday September 5, 2016 11:05 - 11:40
B202 Bosco building

11:40

CP meets Verification Workshop
    See presentations
  • 11h40-12h05: An Improved Constraint Programming Model for Parametric Interval Markov Chain Verification, Anicet Bart, Benoît Delahaye, Éric Monfroy, Charlotte Truchet

Moderators
Speakers
avatar for Anicet Bart

Anicet Bart

LINA - Ecole des Mines de Nantes


Monday September 5, 2016 11:40 - 12:00
B202 Bosco building

13:30

CP meets Verification - Invited talk: Constraint Satisfaction over Bit-Vectors
    See presentations
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).

Moderators
Speakers
avatar for Laurent Michel

Laurent Michel

Associate Professor, University of 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... Read More →


Monday September 5, 2016 13:30 - 14:05
B202 Bosco building

14:05

CP meets Verification Workshop
    See presentations
  • 14h05-14h30: Tight coupling between bit-vector and integer domains can surpass bit-blasting SMT solvers, Zakaria Chihani
  • 14h30-14h55: On Finding program input values maximizing the rounding-off error, Mohammed Said Belaid, Claude Michel, Yahia Lebbah, Michel Rueher

Moderators
Speakers
avatar for Claude Michel

Claude Michel

laboratoire I3S


Monday September 5, 2016 14:05 - 14:55
B202 Bosco building

15:30

CP meets Verification - Invited talk: The use of Constraint Programming in the testing and analysis of a telecommunications protocol
    See presentations
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.

Moderators
Speakers
avatar for Justin Pearson

Justin Pearson

Senior Lecturer, Uppsala universitet
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... Read More →



Monday September 5, 2016 15:30 - 16:05
B202 Bosco building

16:05

CP meets Verification - Invited talk: Network Verification: When less is more, but not always
    See presentations
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.          

Moderators
Speakers
avatar for Andrey Rybalchenko

Andrey Rybalchenko

Senior Researcher, Microsoft Research
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... Read More →


Monday September 5, 2016 16:05 - 16:40
B202 Bosco building

16:40

CP meets Verification Workshop
    See presentations
  • 16h40-17h05: F-CPminer* : A new approach for fault localization using constraint-based data mining, Mehdi Maamar, Noureddine Aribi, Nadjib Lazaar, Yahia Lebbah, Samir Loudni
  • 17h05-17h30: Discussions.

Moderators
Speakers
avatar for Mehdi Maamar

Mehdi Maamar

University of Oran1, Lab LITIO. and University of Montpellier, Lab LIRMM.


Monday September 5, 2016 16:40 - 17:30
B202 Bosco building