Commit 406d5493 authored by François Bobot's avatar François Bobot

Website update

parent 61045ba8
......@@ -3,5 +3,13 @@ open Generate
open Menu
let () = Generate.page delivrables [
p [pcdata "No delivrables have been currently produced"]
md "
* D1.1 ([[downloads/D1_1.pdf|pdf]]): Requirement Analysis
* D1.2 ([[downloads/D1_2.pdf|pdf]], [[downloads/D1_2.tar.gz|tar.gz]]): Set of Benchmarks
* D1.3 ([[downloads/D1_3.pdf|pdf]], [[downloads/D1_3.tar.gz|tar.gz]]): Benchmark Environment (OCI)
* D4.1 ([[downloads/Deliverable-1.4-FPA-in-Alt-Ergo.tar.gz|tar.gz]]): Floating Point Arithmetic in Alt-Ergo
* D4.2 ([[downloads/D4_2.pdf|pdf]], [[downloads/D4_2.tar.gz|tar.gz]]): Preliminary Implementation of the SOPRANO-solver (Popop)
* D2.1 and D2.2 ([[downloads/D2_1-D2_2.pdf|pdf]]) : Combination frameworks
* D3.1 ([[downloads/D3_1.pdf|pdf]]): Floating Point Arithmetic Solver
"
]
......@@ -2,12 +2,4 @@ open Tyxml.Html
open Generate
open Menu
let () = Generate.page jobs [
ul [
li [a ~a:[a_href "http://mathieuacher.com/phdSOPRANO.html"]
[pcdata "PhD: Combining Decision Procedures for \
Constraint Programming and SMT"];
];
li [pcdata "PostDoc"];
]
]
let () = Generate.page jobs [ pcdata "No new position is currently available" ]
......@@ -3,7 +3,12 @@ open Generate
open Menu
let () = Generate.page meetings [
ul [
li [pcdata "Kick-Off"];
]
md "
* 14/01/2015: Kick-off ([[downloads/kickoff_intro.pdf|Introduction]], [[downloads/gatel_soprano.pdf|COLIBRI]], [[downloads/kickoff_popop.pdf|Popop (SOPRANO Solver)]])
* 05/06/2015: Floating Point Arithmetic ([[downloads/colibri_delta.pdf|Delta in COLIBRI]])
* 08/06/2015: Non-linear arithmetic
* 07/10/2015: Discussions about FPA in Alt-Ergo
* 08/01/2016: [[downloads/OCI.pdf|OCI]]; [[downloads/real_fp_behavior.pdf|Improvements of FPA on hard problems]]; [[downloads/bitvector_jan8.odp|Bitvectors in Colibri]]
* 01/07/2016: Improvement of FPA in Alt-Ergo; Lesson on the tentative of COLIBRI at SMTCOMP; States of Popop
"
]
......@@ -4,6 +4,8 @@ open Menu
let () = Generate.page private_ [
md "
[[downloads/soprano_propo.pdf|SOPRANO proposition]] et [[downloads/soprano_RetourCoordinateur.pdf|retour coordinateur]]
# Delivrables
* D1.1 ([[downloads/D1_1.pdf|pdf]]): Requirement Analysis
* D1.2 ([[downloads/D1_2.pdf|pdf]], [[downloads/D1_2.tar.gz|tar.gz]]): Set of Benchmarks
......@@ -18,7 +20,7 @@ let () = Generate.page private_ [
* Colibri ([[downloads/colibri.tar.gz|tar]])
* Popop (tar)
* OCI ([[http://github.com/bobot/OCI/|github]])
* ocplib-simplex ([[https://github.com/OCamlPro-Iguernlala/ocplib-simplex/|github]])
* Ocplib-simplex ([[https://github.com/OCamlPro-Iguernlala/ocplib-simplex/|github]])
# ANR
* Formulaire du compte-rendu intermédiaire ([[downloads/Formulaire_Compte-rendu_intermediaire.pdf|pdf]], [[downloads/Formulaire_Compte-rendu_intermediaire.docx|docx]])
......
......@@ -7,5 +7,8 @@ let () = Generate.page publications [
li [pcdata "CP meets SMT, François Bobot, Sébastien Bardin, \
and Bruno Marre. \
Workshop CP meets Verification 2014 (CPCAV 2014)"];
li [pcdata "Tight coupling between bit-vector and integer \
domains can surpass bit-blasting SMT solvers,Zakaria Chihani . \
Workshop CP meets Verification 2016"];
]
]
......@@ -3,4 +3,11 @@ open Generate
open Menu
let () = Generate.page software [
md "
* [[https://github.com/OCamlPro/alt-ergo|Alt-Ergo]]
* Colibri (Soon available as Freeware)
* Popop (Soon available as Open-Source)
* OCI ([[http://github.com/bobot/OCI/|github]])
* Ocplib-simplex ([[https://github.com/OCamlPro-Iguernlala/ocplib-simplex/|github]])
"
]
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Delivrables for the ANR</title><meta charset="utf-8"/><link rel="stylesheet" href="css/main.css"/><link rel="stylesheet" href="css/lambdoc.css"/></head><body><div id="Header"><a href="index.html" title="Home" style="font-size: 200%; margin-right:10px;">SOPRANO</a>Delivrables for the ANR</div><div id="Content"><div class="readable_div"><p>No delivrables have been currently produced</p></div></div><div id="Menu"><a href="index.html" title="Home">Home</a><br/><a href="partners.html" title="Members of the project">Partners</a><br/><a href="jobs.html" title="Job opportunities">Jobs</a><br/><a href="delivrables.html" title="Delivrables for the ANR">Delivrables</a><br/><a href="meetings.html" title="Meetings">Meetings</a><br/><a href="publications.html" title="Publications">Publications</a><br/><a href="software.html" title="Software">Software</a><br/><a href="private_.html" title="Private">Private</a><br/></div></body></html>
\ No newline at end of file
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Delivrables for the ANR</title><meta charset="utf-8"/><link rel="stylesheet" href="css/main.css"/><link rel="stylesheet" href="css/lambdoc.css"/></head><body><div id="Header"><a href="index.html" title="Home" style="font-size: 200%; margin-right:10px;">SOPRANO</a>Delivrables for the ANR</div><div id="Content"><div class="readable_div"><div class="doc doc_valid"><ul class="doc_itemize"><li class="doc_item"><p class="doc_par">D1.1 (<a class="doc_lnk" href="downloads/D1_1.pdf">pdf</a>): Requirement Analysis</p></li><li class="doc_item"><p class="doc_par">D1.2 (<a class="doc_lnk" href="downloads/D1_2.pdf">pdf</a>, <a class="doc_lnk" href="downloads/D1_2.tar.gz">tar.gz</a>): Set of Benchmarks</p></li><li class="doc_item"><p class="doc_par">D1.3 (<a class="doc_lnk" href="downloads/D1_3.pdf">pdf</a>, <a class="doc_lnk" href="downloads/D1_3.tar.gz">tar.gz</a>): Benchmark Environment (OCI)</p></li><li class="doc_item"><p class="doc_par">D4.1 (<a class="doc_lnk" href="downloads/Deliverable-1.4-FPA-in-Alt-Ergo.tar.gz">tar.gz</a>): Floating Point Arithmetic in Alt-Ergo</p></li><li class="doc_item"><p class="doc_par">D4.2 (<a class="doc_lnk" href="downloads/D4_2.pdf">pdf</a>, <a class="doc_lnk" href="downloads/D4_2.tar.gz">tar.gz</a>): Preliminary Implementation of the SOPRANO-solver (Popop)</p></li><li class="doc_item"><p class="doc_par">D2.1 and D2.2 (<a class="doc_lnk" href="downloads/D2_1-D2_2.pdf">pdf</a>) : Combination frameworks</p></li><li class="doc_item"><p class="doc_par">D3.1 (<a class="doc_lnk" href="downloads/D3_1.pdf">pdf</a>): Floating Point Arithmetic Solver</p></li></ul></div></div></div><div id="Menu"><a href="index.html" title="Home">Home</a><br/><a href="partners.html" title="Members of the project">Partners</a><br/><a href="jobs.html" title="Job opportunities">Jobs</a><br/><a href="delivrables.html" title="Delivrables for the ANR">Delivrables</a><br/><a href="meetings.html" title="Meetings">Meetings</a><br/><a href="publications.html" title="Publications">Publications</a><br/><a href="software.html" title="Software">Software</a><br/><a href="private_.html" title="Private">Private</a><br/></div></body></html>
\ No newline at end of file
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Job opportunities</title><meta charset="utf-8"/><link rel="stylesheet" href="css/main.css"/><link rel="stylesheet" href="css/lambdoc.css"/></head><body><div id="Header"><a href="index.html" title="Home" style="font-size: 200%; margin-right:10px;">SOPRANO</a>Job opportunities</div><div id="Content"><div class="readable_div"><ul><li><a href="http://mathieuacher.com/phdSOPRANO.html">PhD: Combining Decision Procedures for Constraint Programming and SMT</a></li><li>PostDoc</li></ul></div></div><div id="Menu"><a href="index.html" title="Home">Home</a><br/><a href="partners.html" title="Members of the project">Partners</a><br/><a href="jobs.html" title="Job opportunities">Jobs</a><br/><a href="delivrables.html" title="Delivrables for the ANR">Delivrables</a><br/><a href="meetings.html" title="Meetings">Meetings</a><br/><a href="publications.html" title="Publications">Publications</a><br/><a href="software.html" title="Software">Software</a><br/><a href="private_.html" title="Private">Private</a><br/></div></body></html>
\ No newline at end of file
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Job opportunities</title><meta charset="utf-8"/><link rel="stylesheet" href="css/main.css"/><link rel="stylesheet" href="css/lambdoc.css"/></head><body><div id="Header"><a href="index.html" title="Home" style="font-size: 200%; margin-right:10px;">SOPRANO</a>Job opportunities</div><div id="Content"><div class="readable_div">No new position is currently available</div></div><div id="Menu"><a href="index.html" title="Home">Home</a><br/><a href="partners.html" title="Members of the project">Partners</a><br/><a href="jobs.html" title="Job opportunities">Jobs</a><br/><a href="delivrables.html" title="Delivrables for the ANR">Delivrables</a><br/><a href="meetings.html" title="Meetings">Meetings</a><br/><a href="publications.html" title="Publications">Publications</a><br/><a href="software.html" title="Software">Software</a><br/><a href="private_.html" title="Private">Private</a><br/></div></body></html>
\ No newline at end of file
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Meetings</title><meta charset="utf-8"/><link rel="stylesheet" href="css/main.css"/><link rel="stylesheet" href="css/lambdoc.css"/></head><body><div id="Header"><a href="index.html" title="Home" style="font-size: 200%; margin-right:10px;">SOPRANO</a>Meetings</div><div id="Content"><div class="readable_div"><ul><li>Kick-Off</li></ul></div></div><div id="Menu"><a href="index.html" title="Home">Home</a><br/><a href="partners.html" title="Members of the project">Partners</a><br/><a href="jobs.html" title="Job opportunities">Jobs</a><br/><a href="delivrables.html" title="Delivrables for the ANR">Delivrables</a><br/><a href="meetings.html" title="Meetings">Meetings</a><br/><a href="publications.html" title="Publications">Publications</a><br/><a href="software.html" title="Software">Software</a><br/><a href="private_.html" title="Private">Private</a><br/></div></body></html>
\ No newline at end of file
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Meetings</title><meta charset="utf-8"/><link rel="stylesheet" href="css/main.css"/><link rel="stylesheet" href="css/lambdoc.css"/></head><body><div id="Header"><a href="index.html" title="Home" style="font-size: 200%; margin-right:10px;">SOPRANO</a>Meetings</div><div id="Content"><div class="readable_div"><div class="doc doc_valid"><ul class="doc_itemize"><li class="doc_item"><p class="doc_par">14/01/2015: Kick-off (<a class="doc_lnk" href="downloads/kickoff_intro.pdf">Introduction</a>, <a class="doc_lnk" href="downloads/gatel_soprano.pdf">COLIBRI</a>, <a class="doc_lnk" href="downloads/kickoff_popop.pdf">Popop (SOPRANO Solver)</a>)</p></li><li class="doc_item"><p class="doc_par">05/06/2015: Floating Point Arithmetic (<a class="doc_lnk" href="downloads/colibri_delta.pdf">Delta in COLIBRI</a>)</p></li><li class="doc_item"><p class="doc_par">08/06/2015: Non-linear arithmetic</p></li><li class="doc_item"><p class="doc_par">07/10/2015: Discussions about FPA in Alt-Ergo</p></li><li class="doc_item"><p class="doc_par">08/01/2016: <a class="doc_lnk" href="downloads/OCI.pdf">OCI</a>; <a class="doc_lnk" href="downloads/real_fp_behavior.pdf">Improvements of FPA on hard problems</a>; <a class="doc_lnk" href="downloads/bitvector_jan8.odp">Bitvectors in Colibri</a></p></li><li class="doc_item"><p class="doc_par">01/07/2016: Improvement of FPA in Alt-Ergo; Lesson on the tentative of COLIBRI at SMTCOMP; States of Popop</p></li></ul></div></div></div><div id="Menu"><a href="index.html" title="Home">Home</a><br/><a href="partners.html" title="Members of the project">Partners</a><br/><a href="jobs.html" title="Job opportunities">Jobs</a><br/><a href="delivrables.html" title="Delivrables for the ANR">Delivrables</a><br/><a href="meetings.html" title="Meetings">Meetings</a><br/><a href="publications.html" title="Publications">Publications</a><br/><a href="software.html" title="Software">Software</a><br/><a href="private_.html" title="Private">Private</a><br/></div></body></html>
\ No newline at end of file
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Private</title><meta charset="utf-8"/><link rel="stylesheet" href="css/main.css"/><link rel="stylesheet" href="css/lambdoc.css"/></head><body><div id="Header"><a href="index.html" title="Home" style="font-size: 200%; margin-right:10px;">SOPRANO</a>Private</div><div id="Content"><div class="readable_div"><div class="doc doc_valid"><h1 id="doc:a:1" class="doc_sec"><span class="doc_order">1</span><span>Delivrables</span></h1><ul class="doc_itemize"><li class="doc_item"><p class="doc_par">D1.1 (<a class="doc_lnk" href="downloads/D1_1.pdf">pdf</a>): Requirement Analysis</p></li><li class="doc_item"><p class="doc_par">D1.2 (<a class="doc_lnk" href="downloads/D1_2.pdf">pdf</a>, <a class="doc_lnk" href="downloads/D1_2.tar.gz">tar.gz</a>): Set of Benchmarks</p></li><li class="doc_item"><p class="doc_par">D1.3 (<a class="doc_lnk" href="downloads/D1_3.pdf">pdf</a>, <a class="doc_lnk" href="downloads/D1_3.tar.gz">tar.gz</a>): Benchmark Environment (OCI)</p></li><li class="doc_item"><p class="doc_par">D4.1 (<a class="doc_lnk" href="downloads/Deliverable-1.4-FPA-in-Alt-Ergo.tar.gz">tar.gz</a>): Floating Point Arithmetic in Alt-Ergo</p></li><li class="doc_item"><p class="doc_par">D4.2 (<a class="doc_lnk" href="downloads/D4_2.pdf">pdf</a>, <a class="doc_lnk" href="downloads/D4_2.tar.gz">tar.gz</a>): Preliminary Implementation of the SOPRANO-solver (Popop)</p></li><li class="doc_item"><p class="doc_par">D2.1 and D2.2 (<a class="doc_lnk" href="downloads/D2_1-D2_2.pdf">pdf</a>) : Combination frameworks</p></li><li class="doc_item"><p class="doc_par">D3.1 (<a class="doc_lnk" href="downloads/D3_1.pdf">pdf</a>): Floating Point Arithmetic Solver</p></li></ul><h1 id="doc:a:2" class="doc_sec"><span class="doc_order">2</span><span>Softwares</span></h1><ul class="doc_itemize"><li class="doc_item"><p class="doc_par">Alt-Ergo with floating point (tar)</p></li><li class="doc_item"><p class="doc_par">Colibri (<a class="doc_lnk" href="downloads/colibri.tar.gz">tar</a>)</p></li><li class="doc_item"><p class="doc_par">Popop (tar)</p></li><li class="doc_item"><p class="doc_par">OCI (<a class="doc_lnk" href="http://github.com/bobot/OCI/">github</a>)</p></li><li class="doc_item"><p class="doc_par">ocplib-simplex (<a class="doc_lnk" href="https://github.com/OCamlPro-Iguernlala/ocplib-simplex/">github</a>)</p></li></ul><h1 id="doc:a:3" class="doc_sec"><span class="doc_order">3</span><span>ANR</span></h1><ul class="doc_itemize"><li class="doc_item"><p class="doc_par">Formulaire du compte-rendu intermédiaire (<a class="doc_lnk" href="downloads/Formulaire_Compte-rendu_intermediaire.pdf">pdf</a>, <a class="doc_lnk" href="downloads/Formulaire_Compte-rendu_intermediaire.docx">docx</a>)</p></li><li class="doc_item"><p class="doc_par">Accord de consortium (<a class="doc_lnk" href="downloads/Accord_de_consortium_X22760.pdf">pdf</a>)</p></li></ul><h1 id="doc:a:4" class="doc_sec"><span class="doc_order">4</span><span>Meetings</span></h1><ul class="doc_itemize"><li class="doc_item"><p class="doc_par">14/01/2015: Kick-off (<a class="doc_lnk" href="downloads/kickoff_intro.pdf">Introduction</a>, <a class="doc_lnk" href="downloads/gatel_soprano.pdf">COLIBRI</a>, <a class="doc_lnk" href="downloads/kickoff_popop.pdf">Popop (SOPRANO Solver)</a>)</p></li><li class="doc_item"><p class="doc_par">05/06/2015: Floating Point Arithmetic (<a class="doc_lnk" href="downloads/colibri_delta.pdf">Delta in COLIBRI</a>)</p></li><li class="doc_item"><p class="doc_par">08/06/2015: Non-linear arithmetic</p></li><li class="doc_item"><p class="doc_par">07/10/2015: Discussions about FPA in Alt-Ergo</p></li><li class="doc_item"><p class="doc_par">08/01/2016: <a class="doc_lnk" href="downloads/OCI.pdf">OCI</a>; <a class="doc_lnk" href="downloads/real_fp_behavior.pdf">Improvements of FPA on hard problems</a>; <a class="doc_lnk" href="downloads/bitvector_jan8.odp">Bitvectors in Colibri</a></p></li><li class="doc_item"><p class="doc_par">01/07/2016: Improvement of FPA in Alt-Ergo; Lesson on the tentative of COLIBRI at SMTCOMP; States of Popop</p></li></ul><h1 id="doc:a:5" class="doc_sec"><span class="doc_order">5</span><span>Communications</span></h1><ul class="doc_itemize"><li class="doc_item"><p class="doc_par">Bit-vectors and Integer domains for SMT solving (<a class="doc_lnk" href="downloads/bv_cpmeetverif_abstract.pdf">abstract</a>,<a class="doc_lnk" href="downloads/CPmeetsVerifV3.odp">slides</a>), Zakaria Chihani, CP meets Verification 2016 Workshop</p></li><li class="doc_item"><p class="doc_par">OCI : For all you Continuous Integration and Benchmarking needs (<a class="doc_lnk" href="downloads/OCI.pdf">slides</a>) , François Bobot, OCaml User in PariS (OUPS)</p></li></ul></div></div></div><div id="Menu"><a href="index.html" title="Home">Home</a><br/><a href="partners.html" title="Members of the project">Partners</a><br/><a href="jobs.html" title="Job opportunities">Jobs</a><br/><a href="delivrables.html" title="Delivrables for the ANR">Delivrables</a><br/><a href="meetings.html" title="Meetings">Meetings</a><br/><a href="publications.html" title="Publications">Publications</a><br/><a href="software.html" title="Software">Software</a><br/><a href="private_.html" title="Private">Private</a><br/></div></body></html>
\ No newline at end of file
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Private</title><meta charset="utf-8"/><link rel="stylesheet" href="css/main.css"/><link rel="stylesheet" href="css/lambdoc.css"/></head><body><div id="Header"><a href="index.html" title="Home" style="font-size: 200%; margin-right:10px;">SOPRANO</a>Private</div><div id="Content"><div class="readable_div"><div class="doc doc_valid"><p class="doc_par"><a class="doc_lnk" href="downloads/soprano_propo.pdf">SOPRANO proposition</a> et <a class="doc_lnk" href="downloads/soprano_RetourCoordinateur.pdf">retour coordinateur</a></p><h1 id="doc:a:1" class="doc_sec"><span class="doc_order">1</span><span>Delivrables</span></h1><ul class="doc_itemize"><li class="doc_item"><p class="doc_par">D1.1 (<a class="doc_lnk" href="downloads/D1_1.pdf">pdf</a>): Requirement Analysis</p></li><li class="doc_item"><p class="doc_par">D1.2 (<a class="doc_lnk" href="downloads/D1_2.pdf">pdf</a>, <a class="doc_lnk" href="downloads/D1_2.tar.gz">tar.gz</a>): Set of Benchmarks</p></li><li class="doc_item"><p class="doc_par">D1.3 (<a class="doc_lnk" href="downloads/D1_3.pdf">pdf</a>, <a class="doc_lnk" href="downloads/D1_3.tar.gz">tar.gz</a>): Benchmark Environment (OCI)</p></li><li class="doc_item"><p class="doc_par">D4.1 (<a class="doc_lnk" href="downloads/Deliverable-1.4-FPA-in-Alt-Ergo.tar.gz">tar.gz</a>): Floating Point Arithmetic in Alt-Ergo</p></li><li class="doc_item"><p class="doc_par">D4.2 (<a class="doc_lnk" href="downloads/D4_2.pdf">pdf</a>, <a class="doc_lnk" href="downloads/D4_2.tar.gz">tar.gz</a>): Preliminary Implementation of the SOPRANO-solver (Popop)</p></li><li class="doc_item"><p class="doc_par">D2.1 and D2.2 (<a class="doc_lnk" href="downloads/D2_1-D2_2.pdf">pdf</a>) : Combination frameworks</p></li><li class="doc_item"><p class="doc_par">D3.1 (<a class="doc_lnk" href="downloads/D3_1.pdf">pdf</a>): Floating Point Arithmetic Solver</p></li></ul><h1 id="doc:a:2" class="doc_sec"><span class="doc_order">2</span><span>Softwares</span></h1><ul class="doc_itemize"><li class="doc_item"><p class="doc_par">Alt-Ergo with floating point (tar)</p></li><li class="doc_item"><p class="doc_par">Colibri (<a class="doc_lnk" href="downloads/colibri.tar.gz">tar</a>)</p></li><li class="doc_item"><p class="doc_par">Popop (tar)</p></li><li class="doc_item"><p class="doc_par">OCI (<a class="doc_lnk" href="http://github.com/bobot/OCI/">github</a>)</p></li><li class="doc_item"><p class="doc_par">Ocplib-simplex (<a class="doc_lnk" href="https://github.com/OCamlPro-Iguernlala/ocplib-simplex/">github</a>)</p></li></ul><h1 id="doc:a:3" class="doc_sec"><span class="doc_order">3</span><span>ANR</span></h1><ul class="doc_itemize"><li class="doc_item"><p class="doc_par">Formulaire du compte-rendu intermédiaire (<a class="doc_lnk" href="downloads/Formulaire_Compte-rendu_intermediaire.pdf">pdf</a>, <a class="doc_lnk" href="downloads/Formulaire_Compte-rendu_intermediaire.docx">docx</a>)</p></li><li class="doc_item"><p class="doc_par">Accord de consortium (<a class="doc_lnk" href="downloads/Accord_de_consortium_X22760.pdf">pdf</a>)</p></li></ul><h1 id="doc:a:4" class="doc_sec"><span class="doc_order">4</span><span>Meetings</span></h1><ul class="doc_itemize"><li class="doc_item"><p class="doc_par">14/01/2015: Kick-off (<a class="doc_lnk" href="downloads/kickoff_intro.pdf">Introduction</a>, <a class="doc_lnk" href="downloads/gatel_soprano.pdf">COLIBRI</a>, <a class="doc_lnk" href="downloads/kickoff_popop.pdf">Popop (SOPRANO Solver)</a>)</p></li><li class="doc_item"><p class="doc_par">05/06/2015: Floating Point Arithmetic (<a class="doc_lnk" href="downloads/colibri_delta.pdf">Delta in COLIBRI</a>)</p></li><li class="doc_item"><p class="doc_par">08/06/2015: Non-linear arithmetic</p></li><li class="doc_item"><p class="doc_par">07/10/2015: Discussions about FPA in Alt-Ergo</p></li><li class="doc_item"><p class="doc_par">08/01/2016: <a class="doc_lnk" href="downloads/OCI.pdf">OCI</a>; <a class="doc_lnk" href="downloads/real_fp_behavior.pdf">Improvements of FPA on hard problems</a>; <a class="doc_lnk" href="downloads/bitvector_jan8.odp">Bitvectors in Colibri</a></p></li><li class="doc_item"><p class="doc_par">01/07/2016: Improvement of FPA in Alt-Ergo; Lesson on the tentative of COLIBRI at SMTCOMP; States of Popop</p></li></ul><h1 id="doc:a:5" class="doc_sec"><span class="doc_order">5</span><span>Communications</span></h1><ul class="doc_itemize"><li class="doc_item"><p class="doc_par">Bit-vectors and Integer domains for SMT solving (<a class="doc_lnk" href="downloads/bv_cpmeetverif_abstract.pdf">abstract</a>,<a class="doc_lnk" href="downloads/CPmeetsVerifV3.odp">slides</a>), Zakaria Chihani, CP meets Verification 2016 Workshop</p></li><li class="doc_item"><p class="doc_par">OCI : For all you Continuous Integration and Benchmarking needs (<a class="doc_lnk" href="downloads/OCI.pdf">slides</a>) , François Bobot, OCaml User in PariS (OUPS)</p></li></ul></div></div></div><div id="Menu"><a href="index.html" title="Home">Home</a><br/><a href="partners.html" title="Members of the project">Partners</a><br/><a href="jobs.html" title="Job opportunities">Jobs</a><br/><a href="delivrables.html" title="Delivrables for the ANR">Delivrables</a><br/><a href="meetings.html" title="Meetings">Meetings</a><br/><a href="publications.html" title="Publications">Publications</a><br/><a href="software.html" title="Software">Software</a><br/><a href="private_.html" title="Private">Private</a><br/></div></body></html>
\ No newline at end of file
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Publications</title><meta charset="utf-8"/><link rel="stylesheet" href="css/main.css"/><link rel="stylesheet" href="css/lambdoc.css"/></head><body><div id="Header"><a href="index.html" title="Home" style="font-size: 200%; margin-right:10px;">SOPRANO</a>Publications</div><div id="Content"><div class="readable_div"><ul><li>CP meets SMT, François Bobot, Sébastien Bardin, and Bruno Marre. Workshop CP meets Verification 2014 (CPCAV 2014)</li></ul></div></div><div id="Menu"><a href="index.html" title="Home">Home</a><br/><a href="partners.html" title="Members of the project">Partners</a><br/><a href="jobs.html" title="Job opportunities">Jobs</a><br/><a href="delivrables.html" title="Delivrables for the ANR">Delivrables</a><br/><a href="meetings.html" title="Meetings">Meetings</a><br/><a href="publications.html" title="Publications">Publications</a><br/><a href="software.html" title="Software">Software</a><br/><a href="private_.html" title="Private">Private</a><br/></div></body></html>
\ No newline at end of file
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Publications</title><meta charset="utf-8"/><link rel="stylesheet" href="css/main.css"/><link rel="stylesheet" href="css/lambdoc.css"/></head><body><div id="Header"><a href="index.html" title="Home" style="font-size: 200%; margin-right:10px;">SOPRANO</a>Publications</div><div id="Content"><div class="readable_div"><ul><li>CP meets SMT, François Bobot, Sébastien Bardin, and Bruno Marre. Workshop CP meets Verification 2014 (CPCAV 2014)</li><li>Tight coupling between bit-vector and integer domains can surpass bit-blasting SMT solvers,Zakaria Chihani . Workshop CP meets Verification 2016</li></ul></div></div><div id="Menu"><a href="index.html" title="Home">Home</a><br/><a href="partners.html" title="Members of the project">Partners</a><br/><a href="jobs.html" title="Job opportunities">Jobs</a><br/><a href="delivrables.html" title="Delivrables for the ANR">Delivrables</a><br/><a href="meetings.html" title="Meetings">Meetings</a><br/><a href="publications.html" title="Publications">Publications</a><br/><a href="software.html" title="Software">Software</a><br/><a href="private_.html" title="Private">Private</a><br/></div></body></html>
\ No newline at end of file
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Software</title><meta charset="utf-8"/><link rel="stylesheet" href="css/main.css"/><link rel="stylesheet" href="css/lambdoc.css"/></head><body><div id="Header"><a href="index.html" title="Home" style="font-size: 200%; margin-right:10px;">SOPRANO</a>Software</div><div id="Content"><div class="readable_div"></div></div><div id="Menu"><a href="index.html" title="Home">Home</a><br/><a href="partners.html" title="Members of the project">Partners</a><br/><a href="jobs.html" title="Job opportunities">Jobs</a><br/><a href="delivrables.html" title="Delivrables for the ANR">Delivrables</a><br/><a href="meetings.html" title="Meetings">Meetings</a><br/><a href="publications.html" title="Publications">Publications</a><br/><a href="software.html" title="Software">Software</a><br/><a href="private_.html" title="Private">Private</a><br/></div></body></html>
\ No newline at end of file
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Software</title><meta charset="utf-8"/><link rel="stylesheet" href="css/main.css"/><link rel="stylesheet" href="css/lambdoc.css"/></head><body><div id="Header"><a href="index.html" title="Home" style="font-size: 200%; margin-right:10px;">SOPRANO</a>Software</div><div id="Content"><div class="readable_div"><div class="doc doc_valid"><ul class="doc_itemize"><li class="doc_item"><p class="doc_par"><a class="doc_lnk" href="https://github.com/OCamlPro/alt-ergo">Alt-Ergo</a></p></li><li class="doc_item"><p class="doc_par">Colibri (Soon available as Freeware)</p></li><li class="doc_item"><p class="doc_par">Popop (Soon available as Open-Source)</p></li><li class="doc_item"><p class="doc_par">OCI (<a class="doc_lnk" href="http://github.com/bobot/OCI/">github</a>)</p></li><li class="doc_item"><p class="doc_par">Ocplib-simplex (<a class="doc_lnk" href="https://github.com/OCamlPro-Iguernlala/ocplib-simplex/">github</a>)</p></li></ul></div></div></div><div id="Menu"><a href="index.html" title="Home">Home</a><br/><a href="partners.html" title="Members of the project">Partners</a><br/><a href="jobs.html" title="Job opportunities">Jobs</a><br/><a href="delivrables.html" title="Delivrables for the ANR">Delivrables</a><br/><a href="meetings.html" title="Meetings">Meetings</a><br/><a href="publications.html" title="Publications">Publications</a><br/><a href="software.html" title="Software">Software</a><br/><a href="private_.html" title="Private">Private</a><br/></div></body></html>
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment