alt-ergo

    2熱度

    1回答

    SMT證明產量「未知」儘管有強有力的成熟的斷言

    假設我們有下面的C註釋代碼： #define L 3 int a[L] = {0}; /*@ requires \valid(a+(0..(L - 1))); ensures \forall int j; 0 <= j < L ==> (a[j] == j); */ int main() { int i = 0; /*@ loop assigns i, a[
    z3 verification frama-c alt-ergo 2015-07-20

    2熱度

    1回答

    是否存在不可解釋函數的理論（同餘分析）？

    我有一組符號變量的： int a, b, c, d, e; 一組未知函數，由若干公理的約束： f1(a, b) = f2(c, b) f1(d, e) = f1(e, d) f3(b, c, e) = f1(b, e) c = f1(a, b) b = d 在此功能f1，f2，f3是未知的，但固定的。所以它不是uninterpreted functions的理論。 我要證明以下斷言
    z3 verification smt stp alt-ergo 2016-08-29

    1熱度

    1回答

    如何使用Alt-Ergo執行以下SMT-LIB代碼

    以下SMT-LIB代碼在Z3，MathSat和CVC4中運行時沒有問題，但它不在Alt-Ergo中運行，請讓我知道會發生什麼，非常感謝： (set-logic QF_UF) (set-option :incremental true) (set-option :produce-models true) (declare-fun m() Bool) (declare-fun p() Bool
    z3 smt cvc4 alt-ergo 2013-06-01

    1熱度

    1回答

    確保證明代碼有缺陷？

    在下面，當相關的C代碼被註釋掉時，行爲neg_limit的後置條件如何被證明是真實的？ 安全 - >檢查算術溢出之一是不可證明的，如預期的，但它似乎像neg_limit也應該是無法證明的。 語境：我使用的郵資-C-硼，傑西，並通過gWhy，按住Alt鍵人體工程學，以學習如何編寫規範和證明功能的滿足他們。任何關於規範策略，工具等的提示，RTFMing等也是值得讚賞的。到目前爲止，我正在閱讀ACSL
    frama-c alt-ergo 2013-07-30

    1熱度

    1回答

    郵資-C WP常量變量和常量數組

    我想證明與郵資-C的WP插件一些C代碼，並與下面的例子有問題： typedef unsigned char uint8_t; const uint8_t globalStringArray[] = "demo"; const int STRING_LEN = 5; /*@ requires \valid(src) && \valid(dest) && len < 32 ; */ voi
    c frama-c alt-ergo 2015-10-05

    5熱度

    2回答

    依賴無符號整數溢出的代碼證明？

    我應該如何處理驗證代碼的正確性，以避免效率低下，依賴於模塊化算法？ #include <stdint.h> uint32_t my_add(uint32_t a, uint32_t b) { uint32_t r = a + b; if (r < a) return UINT32_MAX; return r; } 我已經嘗試過WP的「INT」的模
    frama-c alt-ergo 2013-08-02

    3熱度

    1回答

    郵資-C WP插件無法驗證從手動

    交換函數如何使frama-c -wp驗證從wp manual的示例 - 一個微不足道swap函數（swap.c）： /* @ requires \valid(a) && \valid(b); @ ensures A: *a == \old(*b); @ ensures B: *b == \old(*a); @ assigns *a,*b; @*/ void
    frama-c alt-ergo 2015-09-04
最新問題