home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #26 / NN_1992_26.iso / spool / comp / theory / 2345 < prev    next >
Encoding:
Text File  |  1992-11-06  |  973 b   |  24 lines
  1. Newsgroups: comp.theory
  2. Path: sparky!uunet!charon.amdahl.com!pacbell.com!decwrl!spool.mu.edu!news.cs.indiana.edu!babbage.ece.uc.edu!don.ece.uc.edu!dsims
  3. From: dsims@don.ece.uc.edu (David Sims)
  4. Subject: Synthesizing loop invariants -- unsolvable?
  5. Message-ID: <1992Nov5.230648.23466@babbage.ece.uc.edu>
  6. Sender: root@babbage.ece.uc.edu (Operator)
  7. Nntp-Posting-Host: don.ece.uc.edu
  8. Organization: University of Cincinnati
  9. Date: Thu, 5 Nov 1992 23:06:48 GMT
  10. Lines: 12
  11.  
  12. I've been thrashing about with the problem of automatically generating
  13. loop invariants for the purposes of program verification.  Is the general
  14. case of automatically synthesizing a loop invariant for any given loop
  15. unsolvable?
  16.  
  17. I suspect it is but cannot come up with a proof.  Any help would be
  18. appreciated.
  19. -- 
  20. David Sims              Dept. of Electrical and Computer Engineering
  21. david.sims@uc.edu       University of Cincinnati
  22. (513) 556-2499          Cincinnati OH  45221-0030
  23.                         USA
  24.