Proving Partial Correctness and Termination of Mutually Recursive Programs

被引：0
|
作者：
Popov, Nikolaj [1 ]
Jebelean, Tudor [1 ]
机构：
[1] Johannes Kepler Univ Linz, Symbol Computat Res Inst, Linz, Austria
来源：
12TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC 2010) | 2011年
关键词：
D O I：
10.1109/SYNASC.2010.65
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present an environment for proving correctness of mutually recursive functional programs. As usual, correctness is transformed into a set of first-order predicate logic formulae-verification conditions. As a distinctive feature of our method, these formulae are not only sufficient, but also necessary for the correctness.
引用
收藏
页码：153 / 156
页数：4
相关论文
共 50 条
  • [21] PROVING TERMINATION OF GENERAL PROLOG PROGRAMS
    APT, KR
    PEDRESCHI, D
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 526 : 265 - 289
  • [22] Proving termination of tree manipulating programs
    Habermehl, Peter
    Iosif, Radu
    Rogalewicz, Adam
    Vojnar, Tomas
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2007, 4762 : 145 - +
  • [23] A METHODOLOGY FOR PROVING TERMINATION OF LOGIC PROGRAMS
    WANG, B
    SHYAMASUNDAR, RK
    JOURNAL OF LOGIC PROGRAMMING, 1994, 21 (01): : 1 - 30
  • [24] PROVING TOTAL CORRECTNESS OF NONDETERMINISTIC PROGRAMS IN INFINITARY LOGIC
    BACK, RJR
    ACTA INFORMATICA, 1981, 15 (03) : 233 - 249
  • [25] Customised induction rules for proving correctness of imperative programs
    Olsson, O
    Wallenburg, A
    SEFM 2005: Third IEEE International Conference on Software Engineering and Formal Methods, Proceedings, 2005, : 180 - 189
  • [26] Proving correctness and completeness of normal programs - a declarative approach
    Drabent, W
    Milkowska, M
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2005, 5 : 669 - 711
  • [27] An inductive theorem on the correctness of general recursive programs
    Bohorquez, Jaime Alejandro
    LOGIC JOURNAL OF THE IGPL, 2007, 15 (5-6) : 373 - 399
  • [28] CORRECTNESS OF RECURSIVE PARALLEL NONDETERMINISTIC FLOW PROGRAMS
    GOGUEN, JA
    MESEGUER, J
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1983, 27 (02) : 268 - 290
  • [29] Transformational methodology for proving termination of logic programs
    Rao, MRKK
    Kapur, D
    Shyamasundar, RK
    JOURNAL OF LOGIC PROGRAMMING, 1998, 34 (01): : 1 - 41
  • [30] A TRANSFORMATIONAL METHODOLOGY FOR PROVING TERMINATION OF LOGIC PROGRAMS
    RAO, MRKK
    KAPUR, D
    SHYAMASUNDAR, RK
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 626 : 213 - 226
12345