Merge pull request #81 from freespek/igor/abstract

add an abstract

reports/discussion.tex

@@ -61,7 +61,7 @@
 
 \paragraph{Value of producing examples.} Even though checking accountable
 safety proved to be challenging, our specifications are not limited to proving
-the property. They are also quite useful for producing examples. For
+only accountable safety. They are also quite useful for producing examples. For
 instance, both Apalache and Alloy are able to quickly produce examples of
 configurations that contain justified and finalized checkpoints. We highlight
 this unique value of specifications that are supported by model checkers:
@@ -70,8 +70,8 @@
 
   \item Executable specifications in Python require the user to provide program
     inputs. These inputs can be also generated randomly, though in the case of
-    3SF, this would be challenging. However, the probability of hitting
-    ``interesting'' values, such as producing finalizing checkpoints, would be
+    3SF, this would be challenging: We expect the probability of hitting
+    ``interesting'' values, such as producing finalizing checkpoints, to be
     quite low.
 
   \item Specifications in the languages supported by proof systems usually do

reports/report.tex

@@ -26,7 +26,7 @@
     \and
     Thanh Hai Tran \\ \small Consensys
 }
-\date{\today}
+\date{}
 
 \input{preambule}
 
@@ -35,7 +35,25 @@
 \maketitle
 
 \begin{abstract}
-  \colorbox{yellow}{TODO}
+
+We explore automated model-checking of the Ethereum specification, specifically
+the accountable safety of the 3SF protocol. We use~\tlap{} as our primary
+specification language and the Apalache model checker with the Z3 SMT solver as
+a backend. As a first step, we manually translate the Python specification
+into~\tlap{}. This reveals the high combinatorial complexity related to the
+definitions of accountable safety in the 3SF protocol.
+
+To address these challenges, we apply multiple layers of manual abstractions,
+such as (1) using folds instead of recursion, (2) integers in place of abstract
+graphs, and (3) decomposing chain configurations. We also develop
+specifications in SMT and Alloy. Despite the challenges, our results show that
+exhaustive verification of accountable safety is feasible for small
+instances with up to 7 checkpoints and 24 validator votes, and we found no
+falsification of accountable safety in slightly larger configurations. Our
+study underscores the value of manual abstraction and expertise in enhancing
+model-checking efficiency and highlights \tlap{}'s flexibility in handling
+abstractions.
+
 \end{abstract}
 
 \setcounter{tocdepth}{2}  % hide anything at or below \subsubsection