Section: Overall Objectives

Highlights

A new trend emerging in 2010-2011 is the construction of international program verification benchmarks and program verification competitions. Benchmarks include the VACID0 challenges (http://vacid.codeplex.com/   [76] ) and the VerifyThis collection (http://verifythis.cost-ic0701.org/ ). We took our part in these efforts by proposing our own gallery of verified programs (http://proval.lri.fr/gallery/index.en.html ). Regarding competitions, we proposed our own solutions to the first (informal) VSTTE competition (http://proval.lri.fr/gallery/vscomp2010.en.html ), we participated to the first FoVeOOS competition (Turin, Italy, Sep. 2011) and were ranked as first, ex-aequo with two other teams (http://proval.lri.fr/gallery/cost11comp.en.html ) and last but not least, we indeed organized the first formal VSTTE program verification competition (November 2011, https://sites.google.com/site/vstte2012/compet ).

A paper by S. Conchon, E. Contejean and M. Iguernelala [24] presenting their work on automated reasoning modulo associative-commutative theories got the best theoretical paper award of ETAPS Conferences http://www.eatcs.org/index.php/best-etaps-paper .

Best Paper Award :

[24] Canonized Rewriting and Ground AC Completion Modulo Shostak Theories in Tools and Algorithms for the Construction and Analysis of Systems.

S. Conchon, É. Contejean, M. Iguernelala.