资 源 简 介
如何得到循环不变式
OCaml: http://caml.inria.fr/
Frama-C: http://frama-c.com/
Interproc: http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/index.html
APRON: http://apron.cri.ensmp.fr/library/
InvGen: http://pub.ist.ac.at/~agupta/invgen/
Tools and Libs: http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/
IDE:
1 Emacs下TypeRex:http://www.typerex.org
2 Eclipse下ocaIDE:http://www.algo-prog.info/ocaide
文 件 列 表
frama-c-api
report
style.css
frama-c.png
index.html
from
intro_wp.txt
wp
slicing
impact
intro_plugin.txt
users
intro_scope.txt
intro_kernel_plugin.txt
pdg
semantic_callgraph
html
intro_pdg.txt
aorai
postdominators
constant_propagation
scope
value
syntactic_callgraph
intro_slicing.txt
occurrence
security_slicing
intro_occurrence.txt
rte
intro_sparecode.txt
sparecode
metrics
inout
