diff --git a/poster/logo.jpg b/poster/logo.jpg
new file mode 100644
index 00000000..2c2c1e94
Binary files /dev/null and b/poster/logo.jpg differ
diff --git a/poster/poster.pdf b/poster/poster.pdf
new file mode 100644
index 00000000..84805d42
Binary files /dev/null and b/poster/poster.pdf differ
diff --git a/poster/poster.tex b/poster/poster.tex
new file mode 100644
index 00000000..c34c62d7
--- /dev/null
+++ b/poster/poster.tex
@@ -0,0 +1,100 @@
+\documentclass[portrait,a0,final]{a0poster}
+
+\usepackage[utf8]{inputenc}
+\usepackage[OT1]{fontenc}
+\usepackage[french]{babel}
+\usepackage{enumitem}
+\usepackage{verbatim}
+\usepackage{amsfonts, amsmath, amssymb, amsthm, dsfont}
+
+\usepackage{listings}
+\lstset{language=[Objective]Caml}
+
+\usepackage{bussproofs}
+\newcommand\typ[2]{\Gamma\vdash#1:#2}
+
+\input{template_deducteam.tex}
+
+\def\aez{\textsf{Alt-Ergo~Zero}}
+\def\altergo{\textsf{Alt-Ergo}}
+\def\ens{\textsf{ENS Paris-Saclay}}
+\def\inria{\textsf{Inria}}
+\def\lsv{\textsf{LSV}}
+\def\msat{\textsf{mSAT}}
+\def\opam{\textsf{opam}}
+
+\begin{document}
+
+\sffamily % Font Family
+
+\postertitle
+{\msat{}:~An~OCaml~SAT~Solver}
+{Guillaume \textsc{Bury}}
+{DEDUC$\vdash$EAM (INRIA) - LSV / CNRS\\
+\Large \textcolor{black}{\texttt{guillaume.bury@inria.fr}}}
+
+
+\begin{center}
+
+\begin{multicols}{2}
+
+\tblock{Introduction} % TODO
+{
+  \vspace{0cm} % Pour pas se faire manger par le titre
+
+  \msat{} is a SAT solving library written in OCaml. It allows to solve the satisfiability
+  of propositional problems in clausal normal form, and produce either a propositional model,
+  or a resolution proof of the problem's unsatisfiability.
+}
+
+\tblock{Conflict Driven Clause learning}
+{
+  \begin{description}
+    \item[Propagation] If there exists a clause $C = C' \lor a$, where
+      $C'$ is false in the partial model, then add $a \mapsto \top$ to
+      the partial model, and record $C$ as the reason for $a$.
+    \item[Decision] Take an atom $a$ which is not yet in the partial model,
+      and add $a \mapsto \top$ to the model.
+    \item[Conflict] A conflict is a clause $C$ that is false in the current partial
+      model.
+    \item[Analyze] Perform resolution between the analyzed clause and the reason
+      behind the propagation of its most recently assigned litteral, until
+      the analyzed clause is suitable for backumping
+    \item[Backjump] A clause is suitable for backjumping if its most recently
+      assigned litteral $a$ is a decision. We can then backtrack to before the
+      decision, and add the analyzed clause to the solver, which will then enable
+      to propagate $a \mapsto \bot$.
+    \item[SMT] Formulas using first-order theories can be handled using a theory.
+      Each formula propagated or decided is sent to the theory, which then
+      has the duty to check whether the conjunction of all formulas seen so
+      far is satisfiable, if not, it should return a theory tautology (as a clause),
+      that is not satisfied in the current partial model.
+  \end{description}
+}
+
+\columnbreak
+
+\tblock{Problem example}
+{
+
+}
+
+\cblock{Theory interface}
+{
+  \lstinputlisting{theory_intf.ml}
+}
+
+\cblock{Proof management}
+{
+  \lstinputlisting{proof_intf.ml}
+}
+
+
+\end{multicols}
+
+
+\Large \msat{} is available on \opam{} and on github: \texttt{https://github.com/Gbury/mSAT}
+
+\end{center}
+
+\end{document}
diff --git a/poster/proof_intf.ml b/poster/proof_intf.ml
new file mode 100644
index 00000000..52b01cb3
--- /dev/null
+++ b/poster/proof_intf.ml
@@ -0,0 +1,17 @@
+type clause_premise =
+    | Hyp | Local | Lemma of lemma
+    | History of clause list
+
+type proof = clause
+and proof_node = {
+  conclusion : clause;
+  step : step;
+}
+and step =
+  | Hypothesis
+  | Assumption
+  | Lemma of lemma
+  | Duplicate of proof * atom list
+  | Resolution of proof * proof * atom
+
+val expand : proof -> proof_node
diff --git a/poster/template_deducteam.tex b/poster/template_deducteam.tex
new file mode 100644
index 00000000..1199b2b5
--- /dev/null
+++ b/poster/template_deducteam.tex
@@ -0,0 +1,111 @@
+\usepackage{multicol}
+\usepackage[dvipsnames]{xcolor}
+\usepackage{graphicx}
+\usepackage{wrapfig}
+\usepackage{tikz}
+
+\usepackage[right=1cm,left=1cm,top=1cm,bottom=1cm]{geometry}
+\setlength{\parindent}{0.0cm}
+\renewcommand{\sfdefault}{lmss}
+
+\definecolor{orangeinria}{RGB}{227,55,41} % Orange INRIA
+\definecolor{color1}{RGB}{227,55,41} % Orange INRIA
+\definecolor{color2}{RGB}{116,101,110} % Blue INRIA
+\definecolor{orange}{RGB}{243,154,38}
+\definecolor{red}{RGB}{226,0,38}
+\definecolor{orange2}{RGB}{236,117,40}
+\definecolor{grey}{RGB}{50, 50, 50}
+
+% args: width, number, title, txt
+\newcommand{\tblock}[2]{
+%  \addtocounter{nblock}{1}
+  \begin{tikzpicture}
+    \tikzstyle{txtblock}=[draw=grey,rounded corners=40pt]
+    \draw node (zou) [txtblock, text width=0.9 \columnwidth, inner sep=25pt, line width=5pt, text justified] {
+	\Large #2
+    };
+    \draw node () at (zou.north) [line width=10pt,inner sep=15pt,anchor=center,fill=white] {
+      \begin{Huge}
+        \textcolor{orangeinria}{\textbf{#1}}
+      \end{Huge}
+    };
+  \end{tikzpicture}
+  \vspace{10mm}
+}
+
+\newcommand{\cblock}[2]{
+%  \addtocounter{nblock}{1}
+  \begin{tikzpicture}
+    \tikzstyle{txtblock}=[draw=grey,rounded corners=40pt,fill=gray!10]
+    \draw node (zou) [txtblock, text width=0.9 \columnwidth, inner sep=25pt, line width=5pt, text justified] {
+	\Large #2
+    };
+    \draw node () at (zou.north) [line width=10pt,inner sep=15pt,anchor=center,fill=white] {
+      \begin{Huge}
+        \textcolor{orangeinria}{\textbf{#1}}
+      \end{Huge}
+    };
+  \end{tikzpicture}
+  \vspace{10mm}
+}
+
+
+\newcommand{\block}[1]{
+%  \addtocounter{nblock}{1}
+  \begin{tikzpicture}
+    \tikzstyle{txtblock}=[draw=grey,fill=gray!10]
+    \draw node (zou) [txtblock, text width=0.9 \columnwidth, inner sep=25pt, line width=4pt, text justified] {
+      \Large #1
+    };
+  \end{tikzpicture}
+  \vspace{10mm}
+}
+
+% args: title, authors, affiliation
+\newcommand{\postertitle}[3]{
+  \begin{tikzpicture}
+    \draw node (titlebar) [inner sep=0cm, 
+                           inner ysep=10mm,
+                           text width=\textwidth, fill=orangeinria] {
+        \hspace{0.2 \textwidth}
+        \begin{minipage}[c]{0.79 \textwidth}
+            \begin{center}
+                \begin{VeryHuge}
+                    {\color{white} \bfseries
+                      #1
+                    }
+                \end{VeryHuge}
+              \end{center}
+            \end{minipage}
+};
+
+    \draw node (authors) at (titlebar.south) [anchor=north, yshift=-5mm,
+                           text width=\textwidth, inner xsep=0cm] {
+        \hspace{0.2 \textwidth}
+        \begin{minipage}[c]{0.79 \textwidth}
+            \begin{center}
+                \begin{huge}
+                  \color{orangeinria}
+                  \textbf{#2}
+
+                  \vspace{5mm}
+
+                  #3
+                \end{huge}
+            \end{center}
+        \end{minipage}
+    };
+
+    \node[xshift=0.1 \textwidth, yshift=-15mm] (logo) at (titlebar.west) {};
+
+    \foreach \s in {0, 0.25, ..., 2.5}
+    {
+      \node[xshift=\s mm, yshift=-\s mm,fill=grey,opacity=0.07,rounded corners=20pt,line width=2pt, minimum width=0.18 \textwidth, minimum height=0.18 \textwidth] () at (logo) {
+      };
+    }
+
+    \node[draw=grey,rounded corners=20pt,fill=white,line width=2pt, minimum width=0.18 \textwidth, minimum height=0.18 \textwidth] () at (logo) {
+      \includegraphics[width=0.16 \textwidth]{logo.jpg}
+    };
+\end{tikzpicture}
+}
diff --git a/poster/theory_intf.ml b/poster/theory_intf.ml
new file mode 100644
index 00000000..2283a5b7
--- /dev/null
+++ b/poster/theory_intf.ml
@@ -0,0 +1,20 @@
+
+type ('formula, 'proof) res =
+  | Sat | Unsat of 'formula list * 'proof
+
+type ('form, 'proof) slice = {
+  start : int;
+  length : int;
+  get : int -> 'form;
+  push : 'form list -> 'proof -> unit;
+}
+
+module type S = sig
+  val dummy : level
+  val backtrack : level -> unit
+  val current_level : unit -> level
+  val assume : (formula, proof) slice
+    -> (formula, proof) res
+  val if_sat : (formula, proof) slice
+    -> (formula, proof) res
+end