--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on October 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Approach to compute if-else in Wp and Why



Hello,

what approach do Wp or Why use to avoid the exponential growth of the 
VCs due to the computation of the selection (branching) rule? Do you use 
"passification" as proposed by Leino? Any references?
-- 
Best regards,
Boris