Commit 26909ab9 authored by François Bobot's avatar François Bobot

[Index] add a picture

parent c4d770c2
......@@ -16,7 +16,7 @@ let page p b =
menu []
in
let menu = div ~a:[a_id "Menu"] menu in
let content = div ~a:[a_id "Content"] b in
let content = div ~a:[a_id "Content"] [div ~a:[a_class ["readable_div"]] b] in
let html =
html
(head (title (pcdata ("SOPRANO: "^p.long_title)))
......
......@@ -5,21 +5,20 @@ open Menu
let p_pcdata txt = p [pcdata txt]
let () = Generate.page main [
div ~a:[a_style "align:justify"] [
img
~src:"images/general.svg"
~alt:"General context"
~a:[a_style (Printf.sprintf "margin: 20px; \
float: right;")]
();
md "
Modern societies crucially rely on digital infrastructures, and it
is becoming clear that high-quality software can be obtained only
with the help of proper software verification tools. Today most
major verification approaches rely on automatic external solvers.
These solvers, however, do not fill the current and future needs for
verification: lack of satisfying model generation, lack of
reasoning on difficult theories (e.g. floating-point arithmetic),
lack of extensibility for specific or new needs.
The SOPRANO project aims at solving these problems and preparing the next
generation of verification-oriented solvers by gathering experts
from academia and industry.
The Soprano project is funded by the [The French National Research Agency]\
(http://www.agence-nationale-recherche.fr/en/\
project-based-funding-to-advance-french-research/)(ANR). Its main objective is
to improve the reasonning power of current software verification tools in order
to make them more powerful, more efficient and easier to use.
We will design a new framework for the
During this project, we will design a new framework for the
cooperation of solvers, focused on model generation and borrowing
principles from SMT (current standard) and CP (well-known in
optimization).
......@@ -34,43 +33,6 @@ is to implement these results in a new open-source platform. The
fourth objective is to ensure industrial-adequacy of the techniques
and tools developed through periodical evaluations
from the industrial partners.
Our main approach is to combine principles coming from both SMT
and CP. Roughly speaking, we seek to add to SMT the extensibility
of CP and its native handling of domains, and to CP the elegant
communication interfaces of SMT and its ability to reason over
formulas with complex boolean structures (conflict analysis) and
quantifiers. In a canonical SMT solver, the Boolean Theory enjoys
a privileged status. We want to explore how to break this
privileged status, in order to allow theory
solvers to contribute more directly to each part of the solving
process. For that, we will develop a notion of first-class domain
and first-class conflict analysis.
The major results of the project includes scientific,
technological, and industrial benefits.
The project has the potential to deliver significant breakthroughs
in automated solving and program analysis. The major
outcome will be a paradigm shift in the combination of automated
solvers, going beyond current standard cooperation frameworks in
terms of extensibility, model-synthesis abilities, and richness of
communication between theories.
The resulting solvers will be more widely applicable, easier to tune
for specific applications, and potentially more efficient, by
encompassing the best trade-offs from SMT and CP.
The major technological output will be the open-source platform
implementing the results, including the cooperation mechanism.
OCamlPro and AdaCore, the industrial partners, will take full
advantage of the project to improve their lines of products and
services. Finally, traditional industrial partners of CEA and
UPSud will directly benefit from improvements of the verification
tools of the project members.
The Consortium is composed of CEA (software verification tools and
CP solving), University of Paris-Sud (SMT solving and
floating-point theory), Inria Rennes (CP solving, floating-point theory),
OcamlPro (software editor and SMT solver developer),
Adacore (software solution for Ada programming language).
"
]
]
......@@ -51,6 +51,12 @@ a:hover {background-color:#eee;}
padding:10px;
}
.readable_div {
margin-left: auto;
margin-right: auto;
max-width: 700px;
}
#Menu {
position:absolute;
top:100px;
......
<!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"><p>No delivrables have been currently produced</p></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 /></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"><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 /></div></body></html>
\ No newline at end of file
This diff is collapsed.
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Home</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>Home</div><div id="Content"><div style="align:justify"><div class="doc doc_valid"><p class="doc_par">Modern societies crucially rely on digital infrastructures, and it is becoming clear that high-quality software can be obtained only with the help of proper software verification tools. Today most major verification approaches rely on automatic external solvers. These solvers, however, do not fill the current and future needs for verification: lack of satisfying model generation, lack of reasoning on difficult theories (e.g. floating-point arithmetic), lack of extensibility for specific or new needs. The SOPRANO project aims at solving these problems and preparing the next generation of verification-oriented solvers by gathering experts from academia and industry.</p><p class="doc_par">We will design a new framework for the cooperation of solvers, focused on model generation and borrowing principles from SMT (current standard) and CP (well-known in optimization). Our main scientific and technical objectives are the following. The first objective is to design a new collaboration framework for solvers, centered around synthesis rather than satisfiability and allowing cooperation beyond that of Nelson-Oppen while still providing minimal interfaces with theoretical guarantees. The second objective is to design new decision procedures for industry-relevant and hard-to-solve theories. The third objective is to implement these results in a new open-source platform. The fourth objective is to ensure industrial-adequacy of the techniques and tools developed through periodical evaluations from the industrial partners.</p><p class="doc_par">Our main approach is to combine principles coming from both SMT and CP. Roughly speaking, we seek to add to SMT the extensibility of CP and its native handling of domains, and to CP the elegant communication interfaces of SMT and its ability to reason over formulas with complex boolean structures (conflict analysis) and quantifiers. In a canonical SMT solver, the Boolean Theory enjoys a privileged status. We want to explore how to break this privileged status, in order to allow theory solvers to contribute more directly to each part of the solving process. For that, we will develop a notion of first-class domain and first-class conflict analysis.</p><p class="doc_par">The major results of the project includes scientific, technological, and industrial benefits. The project has the potential to deliver significant breakthroughs in automated solving and program analysis. The major outcome will be a paradigm shift in the combination of automated solvers, going beyond current standard cooperation frameworks in terms of extensibility, model-synthesis abilities, and richness of communication between theories. The resulting solvers will be more widely applicable, easier to tune for specific applications, and potentially more efficient, by encompassing the best trade-offs from SMT and CP. The major technological output will be the open-source platform implementing the results, including the cooperation mechanism. OCamlPro and AdaCore, the industrial partners, will take full advantage of the project to improve their lines of products and services. Finally, traditional industrial partners of CEA and UPSud will directly benefit from improvements of the verification tools of the project members.</p><p class="doc_par">The Consortium is composed of CEA (software verification tools and CP solving), University of Paris-Sud (SMT solving and floating-point theory), Inria Rennes (CP solving, floating-point theory), OcamlPro (software editor and SMT solver developer), Adacore (software solution for Ada programming language).</p></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 /></div></body></html>
\ No newline at end of file
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Home</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>Home</div><div id="Content"><div class="readable_div"><img src="images/general.svg" alt="General context" style="margin: 20px; float: right;" /><div class="doc doc_valid"><p class="doc_par">The Soprano project is funded by the <a class="doc_lnk" href="http://www.agence-nationale-recherche.fr/en/project-based-funding-to-advance-french-research/">The French National Research Agency</a>(ANR). Its main objective is to improve the reasonning power of current software verification tools in order to make them more powerful, more efficient and easier to use.</p><p class="doc_par">During this project, we will design a new framework for the cooperation of solvers, focused on model generation and borrowing principles from SMT (current standard) and CP (well-known in optimization). Our main scientific and technical objectives are the following. The first objective is to design a new collaboration framework for solvers, centered around synthesis rather than satisfiability and allowing cooperation beyond that of Nelson-Oppen while still providing minimal interfaces with theoretical guarantees. The second objective is to design new decision procedures for industry-relevant and hard-to-solve theories. The third objective is to implement these results in a new open-source platform. The fourth objective is to ensure industrial-adequacy of the techniques and tools developed through periodical evaluations from the industrial partners.</p></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 /></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"><ul><li>PhD</li><li>PostDoc</li></ul></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 /></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"><ul><li>PhD</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 /></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"><ul><li>Kick-Off</li></ul></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 /></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"><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 /></div></body></html>
\ No newline at end of file
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Members of the project</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>Members of the project</div><div id="Content"><img src="images/logo/cea_list.png" alt="CEA List" style="margin: 5px; margin-right: 20px; background:#ED1C24" /><img src="images/logo/upsud.svg" alt="Paris-Sud University" style="margin: 5px; margin-right: 20px; background:white" /><img src="images/logo/INRIA.png" alt="INRIA" style="margin: 5px; margin-right: 20px; background:white" /><img src="images/logo/ocamlpro.png" alt="OcamlPro" style="margin: 5px; margin-right: 20px; background:#1B325F" /><img src="images/logo/adacore.png" alt="Adacore" style="margin: 5px; margin-right: 20px; background:black" /></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 /></div></body></html>
\ No newline at end of file
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>SOPRANO: Members of the project</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>Members of the project</div><div id="Content"><div class="readable_div"><img src="images/logo/cea_list.png" alt="CEA List" style="margin: 5px; margin-right: 20px; background:#ED1C24" /><img src="images/logo/upsud.svg" alt="Paris-Sud University" style="margin: 5px; margin-right: 20px; background:white" /><img src="images/logo/INRIA.png" alt="INRIA" style="margin: 5px; margin-right: 20px; background:white" /><img src="images/logo/ocamlpro.png" alt="OcamlPro" style="margin: 5px; margin-right: 20px; background:#1B325F" /><img src="images/logo/adacore.png" alt="Adacore" style="margin: 5px; margin-right: 20px; background:black" /></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 /></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"><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 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 /></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></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 /></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><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 /></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></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 /></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