[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] What kind of decision procedure is used for integerlinear inequalities



Hello,

On Friday 08 July 2005 17:34, John Rushby wrote:
> By the way, the examples called "spider_benchmarks" in the QF_LRA
> (linear real arithmetic) category came from model checking conjectures
> from a PVS proof: See Lee Pike, Paul Miner, Wilfredo Torres. Model
> Checking Failed Conjectures in Theorem Proving: A Case Study. NASA
> Technical Memorandum NASA/TM-2004-213278, 2004.  Available at
> http://shemesh.larc.nasa.gov/fm/spider/spider_pubs.html

I should note those benchmarks actually came from another success of
ours using SAL: the formal verification of the SPIDER Reintegration
Protocol.  The technical report and the relevant SAL files can be
found at <http://shemesh.larc.nasa.gov/fm/spider/reint_sal/> (this
work will also be reported at EMSOFT
<http://www.princeton.edu/~wolf/EMSOFT-2005/>).

On Friday 08 July 2005 17:34, John Rushby wrote:
> Randomly generated tests are a poor way to evaluate decision
> procedures: you need representative real problems.

Yegor, you may also find Cesare Tinelli and Silvio Ranise's SMT
Library <http://combination.cs.uiowa.edu/smtlib/> of interest for your
purposes.

Regards,
Lee

-- 

NOTICE: 
  This email will be DEPRECATED on August 5th, 2005.  
  Please use the address <lepike@indiana.edu>.

-----------------------------------------------------
  Lee Pike
  Formal Methods Group
  NASA Langley Research Center

  http://www.cs.indiana.edu/~lepike/
  Ph.: 757 864 6193
  Fax: 757 864 4234
  Building 1220, Rm 129
-----------------------------------------------------
  The contents herein do not
  necessarily reflect the positions
  of the United States Government.
-----------------------------------------------------