Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:sign_analysis_of_expressions_and_programs [2008/05/07 23:16]
giuliano
sav08:sign_analysis_of_expressions_and_programs [2015/04/21 17:30] (current)
Line 7: Line 7:
  
 What is (quickly) the sign of What is (quickly) the sign of
-\[+\begin{equation*}
   (31283321 + 8629184) \times (-34234) \times (-4 + (123123 \times (-3)))   (31283321 + 8629184) \times (-34234) \times (-4 + (123123 \times (-3)))
-\]+\end{equation*}
 Why? Why?
 ++++| ++++|
-\[+\begin{equation*}
    (pos \oplus pos) \otimes neg \otimes (neg \oplus (pos \otimes neg)) = pos \otimes neg \otimes neg = pos    (pos \oplus pos) \otimes neg \otimes (neg \oplus (pos \otimes neg)) = pos \otimes neg \otimes neg = pos
-\]+\end{equation*}
 ++++ ++++
  
 What is (quickly) the sign of What is (quickly) the sign of
-\[+\begin{equation*}
     (28166461706 + (723497 \times (- 38931))) \times 42     (28166461706 + (723497 \times (- 38931))) \times 42
-\]+\end{equation*}
 ++++| ++++|
-\[+\begin{equation*}
    (pos \oplus (pos \otimes neg)) \otimes pos = (pos \oplus neg) \otimes pos = \top \otimes pos = \top    (pos \oplus (pos \otimes neg)) \otimes pos = (pos \oplus neg) \otimes pos = \top \otimes pos = \top
-\]+\end{equation*}
 ++++ ++++
  
Line 52: Line 52:
 \end{tabular} \end{tabular}
 $ $
 +
  
 ===== Sign Analysis of Programs ===== ===== Sign Analysis of Programs =====
Line 71: Line 72:
 </​code>​ </​code>​
  
-Abstract state: map each variable to element of $A$.+Abstract state: map each variable to element of $A$. Here we have $|A|^3$ possible states.
  
   * computation over control-flow graph   * computation over control-flow graph
 
sav08/sign_analysis_of_expressions_and_programs.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice