Showing 1–2 of 2 results for author: Périn, M

Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra

Authors: Alexis Fouilhé, David Monniaux, Michaël Périn

Abstract: Polyhedra form an established abstract domain for inferring runtime properties of programs using abstract interpretation. Computations on them need to be certified for the whole static analysis results to be trusted. In this work, we look at how far we can get down the road of a posteriori verification to lower the overhead of certification of the abstract domain of polyhedra. We demonstrate metho… ▽ More Polyhedra form an established abstract domain for inferring runtime properties of programs using abstract interpretation. Computations on them need to be certified for the whole static analysis results to be trusted. In this work, we look at how far we can get down the road of a posteriori verification to lower the overhead of certification of the abstract domain of polyhedra. We demonstrate methods for making the cost of inclusion certificate generation negligible. From a performance point of view, our single-representation, constraints-based implementation compares with state-of-the-art implementations. △ Less

Submitted 3 April, 2013; originally announced April 2013.

Gentzen-Prawitz Natural Deduction as a Teaching Tool

Authors: Jean-François Monin, Cristian Ene, Michaël Périn

Abstract: We report a four-years experiment in teaching reasoning to undergraduate students, ranging from weak to gifted, using Gentzen-Prawitz's style natural deduction. We argue that this pedagogical approach is a good alternative to the use of Boolean algebra for teaching reasoning, especially for computer scientists and formal methods practionners. We report a four-years experiment in teaching reasoning to undergraduate students, ranging from weak to gifted, using Gentzen-Prawitz's style natural deduction. We argue that this pedagogical approach is a good alternative to the use of Boolean algebra for teaching reasoning, especially for computer scientists and formal methods practionners. △ Less

Submitted 21 July, 2009; originally announced July 2009.