1: \documentclass[mpicover]{mpireport-inf}

2: \usepackage{times}

3: \usepackage{url}

4: \usepackage{amsmath}

5: \usepackage{stmaryrd}

6: \usepackage{defs}

7: \usepackage{verbatim}

8: \usepackage{pstricks,pst-node}

9: \usepackage{graphicx}

10: \usepackage{cite}

11: \usepackage{amssymb}

12: 

13: \newgray{lgray}{.7}

14: 

15: \title{On Verifying Complex Properties using Symbolic Shape Analysis}

16: 

17: \author{Thomas Wies \and Viktor Kuncak \and \\ Karen Zee \and Andreas

18:   Podelski \and \\ Martin Rinard}

19: 

20: \begin{addresses}

21: Thomas Wies\\

22: Max-Planck-Institut f\"ur Informatik\\

23: Saarbr\"ucken, Germany \bigskip\\

24: Viktor Kuncak\\

25: MIT Computer Science and Artificial Intelligence Lab\\

26: Cambridge, USA \bigskip\\

27: Karen Zee\\

28: MIT Computer Science and Artificial Intelligence Lab\\

29: Cambridge, USA \bigskip\\

30: Andreas Podelski\\

31: Max-Planck-Institut f\"ur Informatik\\

32: Saarbr\"ucken, Germany \bigskip\\

33: Martin Rinard\\

34: MIT Computer Science and Artificial Intelligence Lab\\

35: Cambridge, USA\\

36: \end{addresses}

37: 

38: %\institute{Max-Planck-Institut f\"ur Informatik, Saarbr\"ucken, Germany\\

39: %\email{\{wies,podelski\}@mpi-inf.mpg.de} \and

40: %MIT Computer Science and Artificial Intelligence Lab, Cambridge, USA\\

41: %\email{\{vkuncak,kkz,rinard\}@csail.mit.edu}}

42: 

43: \repnumber{2--001}                 % mandatory

44: 

45: \setyear{2006}

46: \setrepyear{2006}

47: \setmonth{April}

48: 

49: \begin{document}

50: 

51: %\pagestyle{plain}

52: 

53: \input{abstract}

54: 

55: \makempicover

56: 

57: \tableofcontents

58: 

59: \input{introduction}

60: 

61: \input{example}

62: 

63: \input{algorithm}

64: 

65: \input{abstractpost}

66: 

67: \input{optimizations}

68: 

69: \input{experiments}

70: 

71: \input{conclusion}

72: 

73: \bibliographystyle{abbrv}

74: \bibliography{pnew}

75: 

76: %\mpireports

77: \end{document}

78: %

79: %

80: %

81: 

82: % ----------------------------------------

83: % So it would be good to write that you compute transitions by

84: % >

85: % >   (EX Pred. S & F)

86: % >

87: % > where F is

88: % >

89: % >   &_{p : Pred} (wlp#(c,Gamma,p) --> p') & (wlp#(c,Gamma,~p) --> ~p'))

90: % > [Pred/Pred']

91: % >

92: % > and therefore F does not depend on S, so you compute it only once for a

93: % > fixed Gamma.  Then it is easier to explain why it is useful to have the

94: % > \kappa approximation.

95: % >

96: % > 

97: % ----------------------------------------

98: % -Mention optimistic check for well-formedness in loop invariant inference

99: