Examples

The following are examples of SVC formulas: shostak, function, ineq, array, record, bitvec.

Shostak

The example below is from Shostak's 1984 paper titled An Algorithm for Reasoning About Equality. The formula has been converted into SCV syntax.

(or 
 (/= z (f {+ x {* -1 y}}))
 (/= x {+ z y})
 (= y {+ x {* -1 (f (f z))}})
)

Function

Congruence closure is required in order to determine the validity of this formula.

(ite 
 (and 
  (= (f (f (f (f (f x))))) x)
  (= (f (f (f x))) x)
 )
 (= (f x) x)
 true
)

Ineq

This examples uses intrepreted linear arithmetic and linear inequalities. The variables are defined as common sub-expressions and are subsequently referred to by their expression number.

(=> 
 true 
 (or 
  (not 
   {<= 
    {+
      {* (4|3) $450:V450} 
      {* (4|3) $451:V451}
    } 
    $452:V452}
  ) 
  (or 
   {<= 
    {+ 
      {* 2 $453:V453} 
      {* (-2|3) $453}
    } 
    $454:V454
   } 
  )
  (or 
   (not {<= $452 $454}) 
   (not {< $453 {+ $450 $451}})
  )
 )
)

Array

This is an example that requires reasoning about unbounded arrays. The read and write expressions are interpreted.

(=> 
 (= {write S1 a1 v1} {write S2 a2 v2})
 (=>
  (and
   (/= b a1)
   (/= b a2))
  (= {read S1 b} {read S2 b})
 )
)

Record

This is an example that uses records.

 (= {recupdate [record @a rat @b rat r] @b 1}
    {record @a {recselect r @a} @b 1})

Bitvec

This is an example that uses bit-vectors.

(= {bitcat
     {bitsel {bitplus [bitvec 32 bv3] [bitvec 32 bv2]} 31 16}
     {bitsel {bitplus [bitvec 32 bv3] [bitvec 32 bv2]} 15 0}}
   {bitplus bv3 bv2})

SVC@verify.stanford.edu