Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:proof_and_code_generation_in_lcf_systems [2009/03/05 13:45]
vkuncak
sav08:proof_and_code_generation_in_lcf_systems [2009/03/05 13:52] (current)
vkuncak
Line 39: Line 39:
  
 then this shows that function deriveFact always produces a valid theorem. ​ Whenever we use expression on LHS, we could hace used expression on RHS.  While RHS constructs a theorem, the LHS directly computes it, without invoking primitive rules, so it can be much faster. ​ It is the theorem prover in the usual sense. then this shows that function deriveFact always produces a valid theorem. ​ Whenever we use expression on LHS, we could hace used expression on RHS.  While RHS constructs a theorem, the LHS directly computes it, without invoking primitive rules, so it can be much faster. ​ It is the theorem prover in the usual sense.
 +
  
 ===== Proving Software ===== ===== Proving Software =====
Line 56: Line 57:
   - can be more difficult to combine with program analyses: program analysis may need to be programmed as a tactic in the interactive prover   - can be more difficult to combine with program analyses: program analysis may need to be programmed as a tactic in the interactive prover
   - no need to trust verification-condition generator   - no need to trust verification-condition generator
-  - limitations in terms of generated code+  - limitations in terms of generated ​code, especially to generate imperative and concurrent ​code
   - need to trust code generator   - need to trust code generator
  
 
sav08/proof_and_code_generation_in_lcf_systems.txt · Last modified: 2009/03/05 13:52 by vkuncak
 
© EPFL 2018 - Legal notice