LMF2015: Comienzo del curso
Las clases del curso Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) comenzarán el lunes 9 de febrero en el aula 02 del Edificio Central.
Reseña: Verifying fast and sparse SSA-based optimizations in Coq
Se ha publicado un artículo de razonamiento formalizado en Coq sobre
compiladores titulado Verifying fast and sparse SSA-based optimizations in Coq .
Sus autores son Delphine Demange, David Pichardie y Léo Stefanesco (del grupo Celtique en el INRIA Rennes, Francia).
Su resumen es
The Static Single Assignment (SSA) form is a predominant technology in modern compilers, enabling powerful and fast program optimizations. Despite its great success in the implementation of pro- duction compilers, it is only very recently that this technique has been introduced in verified compilers. As of today, few evidence exist on that, in this context, it also allows faster and simpler optimizations. This work builds on the CompCertSSA verified compiler (an SSA branch of the verified CompCert C compiler). We implement and verify two prevail- ing SSA optimizations: Sparse Conditional Constant Propagation and Global Value Numbering. For both transformations, we mechanically prove their soundness in the Coq proof assistant. Both optimization proofs are embedded in a single sparse optimization framework, factoring out many of the dominance-based reasoning steps required in proofs of SSA-based optimizations. Our experimental evaluations indicate both a better precision, and a significant compilation time speedup.
El trabajo se presentará en CC 2015 (24th International Conference on Compiler Construction).
El código de las correspondientes teorías en Coq se encuentra aquí.
Reseña: Formal proofs for nonlinear optimization
Se ha publicado un artículo de razonamiento formalizado en Coq titulado Formal proofs for nonlinear optimization.
Sus autores son
- Victor Magron (del grupo Circuits and Systems en el Imperial College de Londres, Reino Unido),
- Xavier Allamigeon (del grupo Maxplus del INRIA y del CMAP, École Polytechnique, CNRS, Palaiseau, Francia),
- Stéphane Gaubert (del grupo Maxplus del INRIA y del CMAP, École Polytechnique, CNRS, Palaiseau, Francia) y
- Benjamin Werner (del LIX, École Polytechnique, CNRS, Palaiseau, Francia)
Su resumen es
We present a formally verified global optimization framework. Given a semialgebraic or transcendental function f and a compact semialgebraic domain K, we use the nonlinear maxplus template approximation algorithm to provide a certified lower bound of f over K.
This method allows to bound in a modular way some of the constituents of f by suprema of quadratic forms with a well chosen curvature. Thus, we reduce the initial goal to a hierarchy of semialgebraic optimization problems, solved by sums of squares relaxations.
Our implementation tool interleaves semialgebraic approximations with sums of squares witnesses to form certificates. It is interfaced with Coq and thus benefits from the trusted arithmetic available inside the proof assistant. This feature is used to produce, from the certificates, both valid underestimators and lower bounds for each approximated constituent.
The application range for such a tool is widespread; for instance Hales’ proof of Kepler’s conjecture yields thousands of multivariate transcendental inequalities. We illustrate the performance of our formal framework on some of these inequalities as well as on examples from the global optimization literature.
El trabajo se ha publicado en el Journal of Formalized Reasoning.
El código de las correspondientes teorías en Coq se encuentra aquí.
Reseña: Mutual exclusion by four shared bits with not more than quadratic complexity
Se ha publicado un artículo de razonamiento formalizado en PVS sobre concurrencia titulado Mutual exclusion by four shared bits with not more than quadratic complexity.
Su autor es Wim H. Hesselink (de la Universidad de Groninga, Países Bajos).
Su resumen es
For years, the mutual exclusion algorithm of Lycklama and Hadzilacos (1991) was the optimal mutual exclusion algorithm with the first-come-first-served property, with a minimal number of (non-atomic) communication variables (5 bits per thread). Recently, Aravind published an improvement of it, which uses 4 bits per threads and has simplified waiting conditions. This algorithm is extended here with fault tolerance, and it is verified by assertional methods, using the proof assistant PVS. Progress is proved by means of UNITY logic. The paper proposes a new measure of concurrent time complexity, and proves that the concurrent complexity for throughput of the present algorithm is not more than quadratic in the number of threads.
El código de las correspondientes teorías en PVS se encuentra aquí.
Reseña: Bind induction: Extracting monadic programs from proofs
Se ha publicado un artículo de razonamiento formalizado en Coq sobre titulado Bind induction: Extracting monadic programs from proofs.
Sus autores son Hadi Shafei y James Caldwell (de la Univ. de Wyoming).
Su resumen es
Container types can be modeled as foldable monads that support the MonadPlus operations together with a membership operation. In this paper we present a new typeclass we call -Monad that supports a membership operator for instances of the MonadPlus typeclass. The laws for the -Monad typeclass specify how membership behaves with respect to the monad and monad plus operators. Using -Monads we are able write specifications of properties of generic containers. We also present an induction rule for monads we call bind induction. The new proof rule is proved to be sound. The computational content of the new induction rule is a bind operator, using this rule we are able to extract monadic programs from proofs. We present an example that uses the rule to extract a monadic program from a proof of a specification. We have used the Coq theorem prover to formalize the definitions presented here and to prove properties of the formalization. We rely on the Coq Type Class mechanism for our formalization.
El trabajo se ha presentado en el Symposium on Trends in Functional Programming 2014.
El código de las correspondientes teorías en Coq se encuentra en epsilon-Monad.v y decomposition.v.