|
|
 |
|
Mardi 8 Avril
| Heure: |
12:00 - 13:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Split Cuts and Separable Underestimator for non-convex quadratic problems |
| Description: |
Emiliano Traversi In this work we investigate the computational potential of two tools
for solving non-convex quadratic problems: split inequalities and
separable underestimator.
Split inequalities were first introduced by Letchford and further
examined by Burer and Letchford. For small instances with
box-constraints, we show that the resulting dual bounds are very
tight.The gap can be further decreased by separating so-called
non-standard split inequalities, which we examine in the case of ternary variables.Separable
underestimator are used for solving constrained quadratic binary
programming. Dual bounds are computed by choosing appropriate
underestimators of the objective function that are separable but not
necessarily convex. We explain how to embed this approach into a
branch-and-bound algorithm and present experimental results for several
classes of combinatorial optimization problems, including the quadratic
shortest path problem, for which we provide the first exact approach
available in the literature. |
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Réunion des CS pour audition MdC et Prof |
Jeudi 10 Avril
| Heure: |
10:00 - 12:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Behavior driven design for tests and verification |
| Description: |
Ulrich Kühne In the course of an exploratory project on hardware and system design and verification, we are looking for new ways how to bridge the gap between early abstract models and later implementation phases. One possible approach is the adaptation of agile techniques to the hardware domain, enhanced by model checking techniques. While in the design of hardware systems, testing and verification are usually applied as a post-process, software developement is pushed towards agile techniques like Test Driven Development (TDD), where tests play a central role. Behavior driven development (BDD) extends TDD as a well established software development technique. Essentially, in both techniques testing and implementing is interleaved, with the test cases being written first. In BDD, test cases are written in natural language which enables the discussion with stakeholders and easy requirements tracking throughout the design. In this talk, I will present a BDD tool for the Verilog hardware design language, which extends BDD with formal techniques. From test cases, properties can be generalized, making the verification more reliable, without the need to manually specify temporal properties. |
Vendredi 11 Avril
| Heure: |
10:00 - 12:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Hypercoherence Spaces form a double-glued Category |
| Description: |
Hugh Steele Ehrhard's Hypercoherence Spaces proved a useful medium through which to
study strongly stable semantics. The category of hypercoherence spaces
(HypCoh) has also been shown to be the bedrock of one of the very few
fully complete models of unit-free multiplicative additive linear logic,
satisfying Joyal's softness condition. Much like in the category of
coherence spaces (Coh), an object of HypCoh is a set equipped with a
collection of its subsets, with morphisms being relations respecting
restrictions set by these `cliques'. However, unlike Coh, HypCoh has not
been formalised as a true double-glued category.
In this talk I show that HypCoh is indeed such a category (if you're
willing to bend the rules a little!). We also see how far the spirit of
the glueing construction may be generalised to produce categories with
similar properties. |
|
|
