699 |
700 |
700 \item \alert{our solution:} take a middle ground and record precisely the information |
701 \item \alert{our solution:} take a middle ground and record precisely the information |
701 of the initial state, but be less precise about every newly created object. |
702 of the initial state, but be less precise about every newly created object. |
702 \end{itemize} |
703 \end{itemize} |
703 |
704 |
704 \end{frame}} |
705 \end{frame} |
705 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
706 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
706 |
707 |
707 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
708 \begin{frame}[c] |
708 \begin{frame}[c] |
709 \frametitle{Random Number Generators} |
709 \frametitle{Big Proofs in CS} |
|
710 |
|
711 Formal proofs in CS sound like science fiction? Completely irrelevant! |
|
712 Lecturer gone mad?\pause |
|
713 |
|
714 \begin{itemize} |
|
715 \item in 2008, verification of a small C-compiler |
|
716 \begin{itemize} |
|
717 \item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour'' |
|
718 \item is as good as \texttt{gcc -O1}, but much less buggy |
|
719 \end{itemize} |
|
720 \medskip |
|
721 \item in 2010, verification of a micro-kernel operating system (approximately 8700 loc) |
|
722 \begin{itemize} |
|
723 \item 200k loc of proof |
|
724 \item 25 - 30 person years |
|
725 \item found 160 bugs in the C code (144 by the proof) |
|
726 \end{itemize} |
|
727 \end{itemize} |
|
728 |
|
729 \end{frame} |
|
730 |
|
731 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
732 \begin{frame}[c] |
|
733 \frametitle{Goal} |
|
734 |
|
735 Remember the Bridges example? |
|
736 |
|
737 \begin{itemize} |
|
738 \item Can we look at our programs and somehow ensure |
|
739 they are secure/bug free/correct?\pause\bigskip |
|
740 |
|
741 \item Very hard: Anything interesting about programs is equivalent |
|
742 to halting problem, which is undecidable.\pause\bigskip |
|
743 |
|
744 \item \alert{Solution:} We avoid this ``minor'' obstacle by |
|
745 being as close as possible of deciding the halting |
|
746 problem, without actually deciding the halting problem. |
|
747 $\quad\Rightarrow$ static analysis |
|
748 \end{itemize} |
710 |
749 |
711 \end{frame} |
750 \end{frame} |
712 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
751 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
752 |
|
753 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
754 \begin{frame}[c] |
|
755 \frametitle{What is Static Analysis?} |
|
756 |
|
757 \begin{center} |
|
758 \includegraphics[scale=0.4]{../pics/state.png} |
|
759 \end{center} |
|
760 |
|
761 \begin{itemize} |
|
762 \item depending on some initial input, a program |
|
763 (behaviour) will ``develop'' over time. |
|
764 \end{itemize} |
|
765 |
|
766 \end{frame} |
|
767 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
768 |
|
769 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
770 \begin{frame}[c] |
|
771 \frametitle{What is Static Analysis?} |
|
772 |
|
773 \begin{center} |
|
774 \includegraphics[scale=0.4]{../pics/state2.png} |
|
775 \end{center} |
|
776 |
|
777 \end{frame} |
|
778 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
779 |
|
780 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
781 \begin{frame}[c] |
|
782 \frametitle{What is Static Analysis?} |
|
783 |
|
784 \begin{center} |
|
785 \includegraphics[scale=0.4]{../pics/state3.jpg} |
|
786 \end{center} |
|
787 |
|
788 \end{frame} |
|
789 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
790 |
|
791 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
792 \begin{frame}[c] |
|
793 \frametitle{What is Static Analysis?} |
|
794 |
|
795 \begin{center} |
|
796 \includegraphics[scale=0.4]{../pics/state4.jpg} |
|
797 \end{center} |
|
798 |
|
799 \begin{itemize} |
|
800 \item to be avoided |
|
801 \end{itemize} |
|
802 |
|
803 \end{frame} |
|
804 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
805 |
|
806 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
807 \begin{frame}[c] |
|
808 \frametitle{What is Static Analysis?} |
|
809 |
|
810 \begin{center} |
|
811 \includegraphics[scale=0.4]{../pics/state5.png} |
|
812 \end{center} |
|
813 |
|
814 \begin{itemize} |
|
815 \item this needs more work |
|
816 \end{itemize} |
|
817 |
|
818 \end{frame} |
|
819 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
820 |
|
821 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
822 \begin{frame}[c] |
|
823 \frametitle{What is Static Analysis?} |
|
824 |
|
825 \begin{center} |
|
826 \includegraphics[scale=0.4]{../pics/state6.png} |
|
827 \end{center} |
|
828 |
|
829 \end{frame} |
|
830 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
831 |
|
832 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
833 \begin{frame}[fragile] |
|
834 \frametitle{\large Concrete Example: Sign-Analysis} |
|
835 \mbox{}\\[-20mm]\mbox{} |
|
836 |
|
837 \bl{\begin{plstx}[rhs style=,one per line] |
|
838 : \meta{Exp} ::= \meta{Exp} + \meta{Exp} |
|
839 | \meta{Exp} * \meta{Exp} |
|
840 | \meta{Exp} = \meta{Exp} |
|
841 | \meta{num} |
|
842 | \meta{var}\\ |
|
843 : \meta{Stmt} ::= \meta{label} : |
|
844 | \meta{var} := \meta{Exp} |
|
845 | jump? \meta{Exp} \meta{label} |
|
846 | goto \meta{label}\\ |
|
847 : \meta{Prog} ::= \meta{Stmt} \ldots\\ |
|
848 \end{plstx}} |
|
849 |
|
850 \end{frame} |
|
851 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
852 |
|
853 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
854 \begin{frame}[fragile] |
|
855 \frametitle{\large Concrete Example: Sign-Analysis} |
|
856 \mbox{}\\[-20mm]\mbox{} |
|
857 |
|
858 \bl{\begin{plstx}[rhs style=,one per line] |
|
859 : \meta{Exp} ::= \meta{Exp} + \meta{Exp} |
|
860 | \meta{Exp} * \meta{Exp} |
|
861 | \meta{Exp} = \meta{Exp} |
|
862 | \meta{num} |
|
863 | \meta{var}\\ |
|
864 : \meta{Stmt} ::= \meta{label} : |
|
865 | \meta{var} := \meta{Exp} |
|
866 | jump? \meta{Exp} \meta{label} |
|
867 | goto \meta{label}\\ |
|
868 : \meta{Prog} ::= \meta{Stmt} \ldots\\ |
|
869 \end{plstx}} |
|
870 |
|
871 \begin{textblock}{0}(7.8,2.5) |
|
872 \small |
|
873 \begin{bubble}[5.6cm] |
|
874 \begin{lstlisting}[numbers=none, |
|
875 basicstyle=\ttfamily, |
|
876 language={},xleftmargin=3] |
|
877 a := 1 |
|
878 n := 5 |
|
879 top: jump? n = 0 done |
|
880 a := a * n |
|
881 n := n + -1 |
|
882 goto top |
|
883 done: |
|
884 \end{lstlisting} |
|
885 \end{bubble} |
|
886 \end{textblock} |
|
887 |
|
888 \end{frame} |
|
889 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
890 |
|
891 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
892 \begin{frame}[fragile] |
|
893 \frametitle{\large Concrete Example: Sign-Analysis} |
|
894 \mbox{}\\[-20mm]\mbox{} |
|
895 |
|
896 \bl{\begin{plstx}[rhs style=,one per line] |
|
897 : \meta{Exp} ::= \meta{Exp} + \meta{Exp} |
|
898 | \meta{Exp} * \meta{Exp} |
|
899 | \meta{Exp} = \meta{Exp} |
|
900 | \meta{num} |
|
901 | \meta{var}\\ |
|
902 : \meta{Stmt} ::= \meta{label} : |
|
903 | \meta{var} := \meta{Exp} |
|
904 | jump? \meta{Exp} \meta{label} |
|
905 | goto \meta{label}\\ |
|
906 : \meta{Prog} ::= \meta{Stmt} \ldots\\ |
|
907 \end{plstx}} |
|
908 |
|
909 \begin{textblock}{0}(7.8,3.5) |
|
910 \small |
|
911 \begin{bubble}[5.6cm] |
|
912 \begin{lstlisting}[numbers=none, |
|
913 basicstyle=\ttfamily, |
|
914 language={},xleftmargin=3] |
|
915 n := 6 |
|
916 m1 := 0 |
|
917 m2 := 1 |
|
918 top: jump? n = 0 done |
|
919 tmp := m2 |
|
920 m2 := m1 + m2 |
|
921 m1 := tmp |
|
922 n := n + -1 |
|
923 goto top |
|
924 done: |
|
925 \end{lstlisting} |
|
926 \end{bubble} |
|
927 \end{textblock} |
|
928 |
|
929 \end{frame} |
|
930 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
931 |
|
932 |
|
933 |
713 \end{document} |
934 \end{document} |
|
935 |
|
936 % n := 5 |
|
937 % top: jump? n = 0 done |
|
938 % a := a * n |
|
939 % n := n + -1 |
|
940 % goto top |
|
941 % done: |
|
942 |
714 |
943 |
715 %%% Local Variables: |
944 %%% Local Variables: |
716 %%% mode: latex |
945 %%% mode: latex |
717 %%% TeX-master: t |
946 %%% TeX-master: t |
718 %%% End: |
947 %%% End: |