SOPRANO proposition et retour coordinateur

1Delivrables

• D1.1 (pdf): Requirement Analysis

• D1.2 (pdf, tar.gz): Set of Benchmarks

• D1.3 (pdf, tar.gz): Benchmark Environment (OCI)

• D4.1 (tar.gz): Floating Point Arithmetic in Alt-Ergo

• D4.2 (pdf, tar.gz): Preliminary Implementation of the SOPRANO-solver (Popop)

• D2.1 and D2.2 (pdf) : Combination frameworks

• D3.1 (pdf): Floating Point Arithmetic Solver

2Softwares

• Alt-Ergo with floating point (tar)

• Colibri (tar)

• Popop (tar)

• OCI (github)

• Ocplib-simplex (github)

3ANR

• Formulaire du compte-rendu intermédiaire (pdf, docx)

• Accord de consortium (pdf)

• Présentation revue mi-parcours (pdf)

4Meetings

• 14/01/2015: Kick-off (Introduction, COLIBRI, Popop (SOPRANO Solver))

• 05/06/2015: Floating Point Arithmetic (Delta in COLIBRI)

• 08/06/2015: Non-linear arithmetic

• 07/10/2015: Discussions about FPA in Alt-Ergo

• 08/01/2016: OCI; Improvements of FPA on hard problems; Bitvectors in Colibri

• 01/07/2016: Improvement of FPA in Alt-Ergo; Lesson on the tentative of COLIBRI at SMTCOMP; States of Popop

5Communications

• Bit-vectors and Integer domains for SMT solving (abstract,slides), Zakaria Chihani, CP meets Verification 2016 Workshop

• OCI : For all you Continuous Integration and Benchmarking needs (slides) , François Bobot, OCaml User in PariS (OUPS)