#################################################################### Minutes of the Vecolib Meeting February 27th, 2015 @ Verimag #################################################################### =================================================================== Morning, 9:30-12:30 and 13:30-14:30 =================================================================== Scientific presentations, see [http://vecolib.imag.fr/index.php/Grenoble_meeting_27_February_2015]. Participants: Marius BOZGA, Verimag David BUHLER, CEA-LIST Claire DROSS, AdaCore Peter HABERMEHL, LIAFA Nicolas HALBWACHS, Verimag Radu IOSIF, Verimag Matthieu LEMERRE, CEA-LIST David MONNIAUX, Verimag Yannick MOY, AdaCore Cristina SERBAN, Verimag Mihaela SIGHIREANU, LIAFA Marek TRTIK, Verimag Boris YAKOBOWSKI, CEA-LIST Zhilin WU, LIAFA =================================================================== Afternoon, 14:30-17:30 =================================================================== Working meeting ''''''''''''''''''''''''''''' Deliverable 4.1: Case studies ''''''''''''''''''''''''''''' The draft of the deliverable has been presented. It provides an overview of the container libraries available in Ada & SPARK, C, C++, and Java. The main observation is that all these libraries are using similar data structures based on vectors (dynamic arrays), doubly linked lists, binary search trees and red-black trees, and hash tables. Because the verification and analysis tools developed by the members of the project consider C as the input language, the container libraries considered as case studies shall be written in C and specified using the ACSL norm. AdaCore partners support this choice because they are interested by the solvers developed (in the SMTLIB format). Moreover, the Ada & SPARK containers could be translated in C due to an ongoing project for such a compiler at AdaCore. Case studies for programs using collections have been identified to be - C implementation of a memory allocator obtained by translation of a EventB model which is using sets and maps. - Programs in Ada using containers provided by AdaCore clients. - Programs in C from the gtk. ''''''''''''''''''''''''''''' Discussions ''''''''''''''''''''''''''''' News AdaCore: The new laboratory AdaCore&INRIA, ProofInUse, had his kickoff meeting in February, see [http://www.spark-2014.org/proofinuse/kickoff]. News CEA-LIST: The Frama-C Day will take place March 13th, 2015 at CEA, see [http://frama-c.com/framaCDay.html]. New LIAFA: Starting organization of the second edition of SL-COMP, competition of Separation Logic solvers. Hiring of post-docs: 5 candidates, the most interesting ones don't have yet a PhD; hopes to have a person at the end of this year. A Master 1 from University of Paris Diderot intern will work in the summer on the translation to C of the Ada and Spark libraries. News Verimag: Submitted papers at CAV'15 and CADE'15 on decision procedures for Separation Logic. Tom King, former PhD in the CVC4 team at NYU, is doing his post-doc at Verimag and contributes at the definition of the new format for Separation Logic theory in SMT-LIB. Working group on tools for abstract interpretation over logical domains: meeting to be fixed in April. Working group on translation of case studies from Ada to C: meeting to be fixed in June, at AdaCore or Liafa, at the starting of the Master 1 internship. Next meeting: in Paris at AdaCore or Liafa, in June. Suggestion for invited peoples: o Bart Jacobs from Univ. Leuven, developer of VeriFast verification and analysis tool with SL o Nikos Gorogiannis from UCL, developer of CYCLIST solver