Ignore:
Timestamp:
Jan 14, 2014, 3:09:15 PM (6 years ago)
Author:
boender
Message:
  • changes for proceedings of TACAS 2014
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/TACAS2013-policy/proof.tex

    r3393 r3415  
    1818  &&&&& (pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction < 2^{16}\ \vee\notag\\
    1919  &&&&& (\forall ppc'.ppc' < |instr\_list| \rightarrow ppc < ppc' \rightarrow \notag\\
    20         &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\
     20        &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ \mathbf{in} \notag\\
    2121        &&&&&\ \mathtt{instruction\_size}\ sigma\ ppc'\ instruction' = 0)\ \wedge \notag\\
    2222        &&&&& pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction = 2^{16})
Note: See TracChangeset for help on using the changeset viewer.