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
sav07_lecture_9_skeleton [2007/04/17 19:58]
vkuncak
sav07_lecture_9_skeleton [2007/04/19 11:53] (current)
vkuncak
Line 86: Line 86:
  
 === Reduced product === === Reduced product ===
- 
-===== ASTREE Static Analyzer ===== 
- 
-=== A Static Analyzer for Large Safety-Critical Software === 
- 
-[[http://​www.di.ens.fr/​~cousot/​COUSOTpapers/​PLDI03.shtml|Link to paper]] 
- 
-Section 5.4: A remark on notation: 
-  * if $\rho$ denotes the state and $S$ is a deterministic statement, then $[\![S]\!]^s(\rho)$ represents the new state after executing the statement; the relation corresponding to statement semantics would be $\{(S,​[\![S]\!]^s(\rho)) \mid \rho \mbox{ is a state, mapping variables to their values \}$. 
-  * this function is extended to map sets of states to sets of states, which gives function mapping $E$ to $[\![S]\!]^c(E)$ and is what we called strongest postcondition $sp(S,E)$. 
-  * this is abstracted to abstract domain 
- 
-=== The Octagon Abstract Domain === 
- 
-[[http://​www.di.ens.fr/​~mine/​publi/​article-mine-HOSC06.pdf|Link to paper]] 
- 
-=== Combination of Abstractions in the ASTRÉE Static Analyzer === 
- 
-  * [[http://​www.di.ens.fr/​~cousot/​COUSOTpapers/​ASIAN06.shtml|Link to paper]] 
  
 
sav07_lecture_9_skeleton.txt · Last modified: 2007/04/19 11:53 by vkuncak
 
© EPFL 2018 - Legal notice