Difference between revisions of "Paris meeting 3 June 2015"
| (6 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
'''Location:''' [https://www.google.fr/maps/place/46+Rue+d%27Amsterdam,+75009+Paris/@48.8785888,2.3270623,17z/data=!4m7!1m4!3m3!1s0x47e66e4a5a15ccaf:0x5cdb82160a7919b0!2s46+Rue+d%27Amsterdam,+75009+Paris!3b1!3m1!1s0x47e66e4a5a15ccaf:0x5cdb82160a7919b0 Ada Core] | '''Location:''' [https://www.google.fr/maps/place/46+Rue+d%27Amsterdam,+75009+Paris/@48.8785888,2.3270623,17z/data=!4m7!1m4!3m3!1s0x47e66e4a5a15ccaf:0x5cdb82160a7919b0!2s46+Rue+d%27Amsterdam,+75009+Paris!3b1!3m1!1s0x47e66e4a5a15ccaf:0x5cdb82160a7919b0 Ada Core] | ||
| − | + | 9h00 '''Coffee+croissants''' | |
| − | + | 9h30 '''Invited speaker:''' '''Nikos Gorogiannis''' (Middlesex University London) ''Proving entailments in separation logic with inductive definitions using cyclic proof'' | |
Augmenting most logics with inductive definitions poses well-known problems: undecidability of entailment usually follows, and heuristic proof search for entailment encounters difficulties common in inductive theorem proving. Cyclic proof provides an alternative to proof by explicit induction that is more flexible as well as potentially more amenable to automation. | Augmenting most logics with inductive definitions poses well-known problems: undecidability of entailment usually follows, and heuristic proof search for entailment encounters difficulties common in inductive theorem proving. Cyclic proof provides an alternative to proof by explicit induction that is more flexible as well as potentially more amenable to automation. | ||
| Line 16: | Line 16: | ||
* present some additional facilities added to Cyclist over time. | * present some additional facilities added to Cyclist over time. | ||
| − | + | 10h30 '''Constantin Enea''' (Liafa) ''Monitoring Refinement via Symbolic Reasoning'' | |
Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to reference implementations — or in formal terms, one risks violating observational refinement. Precisely testing this refinement even within a single execution is intractable, limiting existing approaches to executions with very few object invocations. | Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to reference implementations — or in formal terms, one risks violating observational refinement. Precisely testing this refinement even within a single execution is intractable, limiting existing approaches to executions with very few object invocations. | ||
| Line 22: | Line 22: | ||
We develop scalable and effective algorithms for detecting refinement violations. Our algorithms are founded on incremental, symbolic reasoning, and exploit foundational insights into the refinement-checking problem. Our approach is sound, in that we detect only actual violations, and scales far beyond existing violation-detection algorithms. Empirically, we find that our approach is practically complete, in that we detect the violations arising in actual executions. | We develop scalable and effective algorithms for detecting refinement violations. Our algorithms are founded on incremental, symbolic reasoning, and exploit foundational insights into the refinement-checking problem. Our approach is sound, in that we detect only actual violations, and scales far beyond existing violation-detection algorithms. Empirically, we find that our approach is practically complete, in that we detect the violations arising in actual executions. | ||
| − | 12h00 Lunch | + | 11h30 '''Mihaela Sighireanu''' (Liafa) ''Report on SL-COMP'14'' |
| + | |||
| + | A competition of solvers for Separation Logic was held in May 2014, as an unofficial satellite event of the FLoC Olympic Games. | ||
| + | Six solvers participated in the competition; the success and performance of each solver was measured over an appropriate subset of a library of benchmarks accumulated for the purpose. The benchmarks consisted of satisfiability and entailment problems over formulas in the fragment of symbolic heaps with inductive definitions, which is the fragment of Separation Logic that is most used in program analysis and verification tools. This talk will present the competition rules, the participants, the results, the findings, and the future of this event. | ||
| + | |||
| + | 12h00 '''Lunch''' | ||
13h30 '''Radu Iosif''' (Verimag) ''Decidable Horn Systems with Difference Constraints Arithmetic'' | 13h30 '''Radu Iosif''' (Verimag) ''Decidable Horn Systems with Difference Constraints Arithmetic'' | ||
| − | This paper tackles the problem of the existence of solutions for recursive systems of Horn clauses with second-order variables interpreted as integer relations, and harnessed by a simple first-order theory, such as difference bounds arithmetic. We start by the definition of a simple class of Horn systems with one second-order variable and one non-linear recursive rule, for which we prove the decidability of the problem "does the system | + | This paper tackles the problem of the existence of solutions for |
| + | recursive systems of Horn clauses with second-order variables | ||
| + | interpreted as integer relations, and harnessed by a simple | ||
| + | first-order theory, such as difference bounds arithmetic. We start by | ||
| + | the definition of a simple class of Horn systems with one second-order | ||
| + | variable and one non-linear recursive rule, for which we prove the | ||
| + | decidability of the problem "does the system have a solution ?". The | ||
| + | proof relies on a construction of a tree automaton recognizing all | ||
| + | cycles in the weighted graph corresponding to every unfolding tree of | ||
| + | the Horn system. We constrain the tree to recognize only cycles of | ||
| + | negative weight by adding a Presburger formula that harnesses the | ||
| + | number of times each rule is fired, and reduce our problem to the | ||
| + | universality of a Presburger-constrained tree automaton. We studied | ||
| + | the complexity of this problem and found it to be in 2-Exptime | ||
| + | with a Exptime-hard lower bound. In the second part, we drop | ||
| + | the univariate restriction and consider multivariate second-order Horn | ||
| + | systems with a structural restriction, called flatness. Finally, we | ||
| + | show the decidability of the more general class of systems, within the | ||
| + | same complexity bounds. | ||
14h30 '''Emmanuel Briot''' (AdaCore) ''Traits-based generic containers'' | 14h30 '''Emmanuel Briot''' (AdaCore) ''Traits-based generic containers'' | ||
| Line 40: | Line 63: | ||
15h30 '''Cristina Serban''' (Verimag) ''Formalizing Separation Logic using Multi-sorted First Order Logic'' | 15h30 '''Cristina Serban''' (Verimag) ''Formalizing Separation Logic using Multi-sorted First Order Logic'' | ||
| − | This talk presents the status of an on-going work that aims to provide semantics for basic Separation Logic (with no inductive definitions) via a translation into multi-sorted First Order Logic. The purpose of this translation is to serve | + | This talk presents the status of an on-going work that aims to provide semantics for basic Separation Logic (with no inductive definitions) via a translation into multi-sorted First Order Logic. The purpose of this translation is to serve as basis for a common format for writing SL formulae, using SMT-LIBv2.5. |
| − | 16h00-17h00 Business Meeting | + | 16h00-17h00 '''Business Meeting''' |
Latest revision as of 16:34, 28 May 2015
Location: Ada Core
9h00 Coffee+croissants
9h30 Invited speaker: Nikos Gorogiannis (Middlesex University London) Proving entailments in separation logic with inductive definitions using cyclic proof
Augmenting most logics with inductive definitions poses well-known problems: undecidability of entailment usually follows, and heuristic proof search for entailment encounters difficulties common in inductive theorem proving. Cyclic proof provides an alternative to proof by explicit induction that is more flexible as well as potentially more amenable to automation.
Cyclist is a theorem prover that searches for cyclic proofs of entailments employing inductive definitions, and does so generically, in that it has been applied to several logics. Its separation logic instantiation allows proof search for symbolic heap entailments with user-defined inductive predicates.
In this talk I will
- give an overview of the core concepts behind cyclic proof;
- show how it can be applied to separation logic entailments;
- discuss how it is currently implemented in Cyclist;
- demonstrate Cyclist on a few examples;
- present some additional facilities added to Cyclist over time.
10h30 Constantin Enea (Liafa) Monitoring Refinement via Symbolic Reasoning
Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to reference implementations — or in formal terms, one risks violating observational refinement. Precisely testing this refinement even within a single execution is intractable, limiting existing approaches to executions with very few object invocations.
We develop scalable and effective algorithms for detecting refinement violations. Our algorithms are founded on incremental, symbolic reasoning, and exploit foundational insights into the refinement-checking problem. Our approach is sound, in that we detect only actual violations, and scales far beyond existing violation-detection algorithms. Empirically, we find that our approach is practically complete, in that we detect the violations arising in actual executions.
11h30 Mihaela Sighireanu (Liafa) Report on SL-COMP'14
A competition of solvers for Separation Logic was held in May 2014, as an unofficial satellite event of the FLoC Olympic Games. Six solvers participated in the competition; the success and performance of each solver was measured over an appropriate subset of a library of benchmarks accumulated for the purpose. The benchmarks consisted of satisfiability and entailment problems over formulas in the fragment of symbolic heaps with inductive definitions, which is the fragment of Separation Logic that is most used in program analysis and verification tools. This talk will present the competition rules, the participants, the results, the findings, and the future of this event.
12h00 Lunch
13h30 Radu Iosif (Verimag) Decidable Horn Systems with Difference Constraints Arithmetic
This paper tackles the problem of the existence of solutions for recursive systems of Horn clauses with second-order variables interpreted as integer relations, and harnessed by a simple first-order theory, such as difference bounds arithmetic. We start by the definition of a simple class of Horn systems with one second-order variable and one non-linear recursive rule, for which we prove the decidability of the problem "does the system have a solution ?". The proof relies on a construction of a tree automaton recognizing all cycles in the weighted graph corresponding to every unfolding tree of the Horn system. We constrain the tree to recognize only cycles of negative weight by adding a Presburger formula that harnesses the number of times each rule is fired, and reduce our problem to the universality of a Presburger-constrained tree automaton. We studied the complexity of this problem and found it to be in 2-Exptime with a Exptime-hard lower bound. In the second part, we drop the univariate restriction and consider multivariate second-order Horn systems with a structural restriction, called flatness. Finally, we show the decidability of the more general class of systems, within the same complexity bounds.
14h30 Emmanuel Briot (AdaCore) Traits-based generic containers
This presentation will describe an implementation for standard Ada containers based on a traits paradigm. This makes the implementation of the containers configurable at compile time, giving user full control over aspects such as bounded/unbounded containers, definite/indefinite elements and memory allocation. Users can specialize the implementation of any such aspect while sharing the rest of the code for the containers. These containers are meant to be both efficient and with minimal runtime overhead for full Ada applications, or provable in the context of SPARK applications.
15h30 Cristina Serban (Verimag) Formalizing Separation Logic using Multi-sorted First Order Logic
This talk presents the status of an on-going work that aims to provide semantics for basic Separation Logic (with no inductive definitions) via a translation into multi-sorted First Order Logic. The purpose of this translation is to serve as basis for a common format for writing SL formulae, using SMT-LIBv2.5.
16h00-17h00 Business Meeting
