期刊文献+

基于抽象解释的Prolog程序验证技术研究 被引量:1

Abstract Interpretation Based Verification of Prolog Programs
下载PDF
导出
摘要 作为一种通用的语义近似理论,抽象解释已广泛应用于各类程序的形式化验证中。现有基于抽象解释的逻辑程序验证技术未涉及与程序点相关联的程序性质的验证,设计能够描述此类性质的逻辑程序具体语义和抽象语义是构造相应验证工具的关键。本文给出了一种基于抽象解释的Prolog程序验证方法,该方法采用了具有路径信息的Prolog语义及其抽象作为语义基础,因而可用于验证与程序点相关联的程序特性。本文例子表明了该验证方法的有效性。 Abstract interpretation is a general theory of semantics approximation, which has been widely used in the verification of computer programs. Existing abstract interpretation based verification methods for logic programs do not deal with the properties associated with the program points. Based on our previous work on Prolog semantics, an abstract interpretation based verification method for Prolog programs is proposed in this paper, which makes use of a denotational semantics for Pro[og that contains path information about the execution of the goals in a program. Since the semantics is capable of describing program properties associated with program points, it's natural for our verification method to be able to verify such a class of properties. The applicability of our method is exemplified in this paper.
出处 《计算机科学》 CSCD 北大核心 2008年第7期261-268,共8页 Computer Science
基金 国家自然科学基金(60563005 60663005) 广西青年科学基金(桂科青0728093 0542036)
关键词 抽象解释 程序验证 PROLOG 不动点语义 Abstract interpretation, Program verification, Prolog, Fixpoint semantics
  • 相关文献

参考文献30

  • 1CousotP, CousotR. Abstract interpretation : A unified latticemodel for static analysis of programs by construction or approximation of fixpoints ff Proceedings of the 4th ACM Symposium on Principles of Programming Languages. Los Angeles,California,USA, 1977: 238-252.
  • 2Cousot P, Cousot R. Systematic design of program analysis frameworks//Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL' 79). 1979 : 269-282.
  • 3Barbuti R, Giaeobazzi R, Levi G. A General Framework for Semantics-Based Bottom-Up Abstract Interpretation of Logic Programs. ACM Transactions on Programming Languages and Systems, 1993,15 (1) : 133-181.
  • 4Charlier B L,Rossi S, Hentenryck P V. Sequence-based Abstract Interpretation of Prolog. Theory and Practice of Logic Programming,2002,2(1) :25-84.
  • 5Codish M, Dams D, Yardeni E. Bottom-up Abstract Interpretation of Logic Programs. Journal of Theoretical Computer Science, 1994,124 : 93-125.
  • 6Cousot P,Cousot R. Abstract Interpretation and Applications to Logic Programs. Journal of Logic Programming, 1992,13 (23) : 103-179.
  • 7MellishC. Abstract InterpretationofPrologPrograms // S. Abramsky and C. Hankin, eds, Abstract Interpretation of Declarative Languages. 1987:181-198.
  • 8Charlier B L, Leclere C,Rossi S,et al. Automated Verification of Prolog Programs. Journal of Logic Programming, 1999,39 ( 1/ 3):3-42.
  • 9Hermenegildo M, Puebla G,Bueno F, et al. Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor). Science of Computer Programming, 2005,58 (1/2) : 115-140.
  • 10Comini M, Gori R, Levi G, et al. Abstract interpretation based verification of logic programs. Science of Computer Programming,2003,49(1/3) :89-123.

二级参考文献24

  • 1Barbuti R, Codish M, Giacobazzi R, et al. Modeling Prolog control. Journal of Logic and Computation, 1993,3. 579-603.
  • 2Barbuti R, Codish M, Giacobazzi R, et al. Oracle Semantics for Prolog. In: Kirchner H, Levi G, eds. Algebraic and Logic Programming, Proceedings of the Third International Conference, Lecture Notes in Computer Science, vol 632, 1992. 100-114.
  • 3Barbuti R, Giacobazzi R, Levi G. A General Framework for Semantics-based Bottom-up Abstract Interpretation of Logic Programs. ACM Transactions on Programming Languages and Systems, 1993,15(1): 133-181.
  • 4Bossi A, Bugliesi M, Fabris M. Fixpoint Semantics for Prolog. In: Warren D S,ed. Proceedings of the Tenth International Conference on Logic Programming, Cambridge, MA.. MIP Prese, 1993. 374-389.
  • 5Borger E. A Logical Operational Semantics for Full Prolog. In: Borger E, Brining H K, Richter M M, eds. CSL' 89. Third Workshop on Computer Science Logic, Lecture Notes in ComputerScience, vol 440, 1990. 36-64.
  • 6Codish M, Dams D, Yardeni E. Bottom-up Abstract Interpretation of Logic Programs. Journal of Theoretical Computer Science, 1994,124:93-125.
  • 7Cousot P, Cousot R. Abstract Interpretation and Applications to Logic Programs. Journal of Logic Programming, 1992, 13 (23) : 103-179.
  • 8File G, Rossi S. Static Analysis of Prolog with Cut. LPAR, 1993. 134-145.
  • 9Fitting M. A Deterministic Prolog Fixpoint Semantics. Journal of Logic Programming, 1985,2(2) . 111-118.
  • 10Gabbrielli M, Levi G, Meo M C. Resultants Semantics for Prolog. Journal of Logic and Computation, 1996,6(4): 491-521.

同被引文献8

引证文献1

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部