diff --git a/src/index.page.ml b/src/index.page.ml index de49ccada5ade298eb6af4a012257e9e3b66f5d2..16e7e3db578f79d932eac4c32288337a65bab3e6 100644 --- a/src/index.page.ml +++ b/src/index.page.ml @@ -2,6 +2,79 @@ open Html5.M open Generate open Menu +let p_pcdata txt = p [pcdata txt] + let () = Generate.page main [ - p [pcdata "C'est ça!"] -] + div ~a:[a_style "align:justify"] [ + p_pcdata " +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_pcdata " +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_pcdata " +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_pcdata " +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_pcdata " +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). +" + ] + ] diff --git a/www/index.html b/www/index.html index 3138d0f4f18a004b993f6758ec5a696cb3499756..4271d8fe7652284a30b7c138f916486eefd79e37 100644 --- a/www/index.html +++ b/www/index.html @@ -1,2 +1,64 @@ -SOPRANO: Home

C'est ça!

\ No newline at end of file +SOPRANO: Home

+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.

+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.

+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). +

\ No newline at end of file