source: src/ASM/CPP2012-policy/conclusion.tex @ 2084

Last change on this file since 2084 was 2084, checked in by boender, 7 years ago
  • changed bibliography style
  • added CerCo? thanks
  • some words of conclusion
File size: 687 bytes
Line 
1\section{Conclusion}
2
3In the previous sections, we have discussed the branch displacement optimisation
4problem, presented an optimised solution, and discussed the proof of
5termination and correctness for this algorithm, as formalised in Matita.
6
7\subsection{Related work}
8
9As far as we are aware, this is the first formal discussion of the branch
10displacement algorithm.
11
12(Piton? CompCert?)
13
14\subsection{Formal development}
15
16All Matita files related to this development can be found on the CerCo
17website, \url{http://cerco.cs.unibo.it}. The specific part that contains the
18branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
19whose name starts with {\tt Policy}.
Note: See TracBrowser for help on using the repository browser.