Integrating model checking and theorem proving in a reflective functional language

被引：0
|
作者：
Melham, T [1 ]
机构：
[1] Univ Oxford, Comp Lab, Oxford OX1 3QD, England
来源：
INTEGRATED FORMAL METHODS, PROCEEDINGS | 2004年 / 2999卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Forte is a formal verification system developed by Intel's Strategic CAD Labs for applications in hardware design and verification. Forte integrates model checking and theorem proving within a functional programming language, which both serves as an extensible specification language and allows the system to be scripted and customized. The latest version of this language, called reFL(ect), has quotation and antiquotation constructs that build and decompose expressions in the language itself. This provides combination of pattern-matching and reflection features tailored especially for the Forte approach to verification. This short paper is an abstract of an invited presentation given at the International Conference on Integrated Formal Methods in 2004, in which the philosophy and architecture of the Forte system are described and an account is given of the role of reFLect in the system.
引用
收藏
页码：36 / 39
页数：4
相关论文
共 50 条
  • [31] Formal Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking
    Elderhalli, Yassmeen
    Hasan, Osman
    Ahmad, Waqar
    Tahar, Sofiene
    NASA FORMAL METHODS, NFM 2018, 2018, 10811 : 139 - 156
  • [32] Proving sequential consistency by model checking
    Braun, T
    Condon, A
    Hu, AJ
    Juse, KS
    Laza, M
    Leslie, M
    Sharma, R
    SIXTH IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2001, : 103 - 108
  • [33] THEOREM PROVING FOR PRENEX GODEL LOGIC WITH Δ: CHECKING VALIDITY AND UNSATISFIABILITY
    Baaz, Matthias
    Ciabattoni, Agata
    Fermueller, Christian G.
    LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (01)
  • [34] Proving Functional Equivalence of two AES Implementations using Bounded Model Checking
    Post, Hendrik
    Sinz, Carsten
    SECOND INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION, AND VALIDATION, PROCEEDINGS, 2009, : 31 - 40
  • [35] Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems
    Din, Crystal Chang
    Owe, Olaf
    Bubel, Richard
    PROCEEDINGS OF THE 2014 2ND INTERNATIONAL CONFERENCE ON MODEL-DRIVEN ENGINEERING AND SOFTWARE DEVELOPMENT (MODELSWARD 2014), 2014, : 480 - 487
  • [36] A Short Introduction to Two Approaches in Formal Verification of Security Protocols: Model Checking and Theorem Proving
    Pourpouneh, Mohsen
    Ramezanian, Rasoul
    ISECURE-ISC INTERNATIONAL JOURNAL OF INFORMATION SECURITY, 2016, 8 (01): : 3 - 24
  • [37] From Width-Based Model Checking toWidth-Based Automated Theorem Proving
    Oliveira, Mateus de Oliveira
    Vadiee, Farhad
    THIRTY-SEVENTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, VOL 37 NO 5, 2023, : 6297 - 6304
  • [38] Integrated formal verification: Using model checking with automated abstraction, invariant generation, and theorem proving
    Rushby, J
    THEORETICAL AND PRACTICAL ASPECTS OF SPIN MODEL CHECKING, 1999, 1680 : 1 - 11
  • [39] A knowledge markup language and distributed theorem proving
    Xu, ZQ
    Wang, JB
    Wang, NC
    PARALLEL AND DISTRIBUTED COMPUTING, APPLICATIONS AND TECHNOLOGIES, PDCAT'2003, PROCEEDINGS, 2003, : 127 - 131
  • [40] ATS: A language that combines programming with theorem proving
    Cui, S
    Donnelly, K
    Xi, HW
    FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS, 2005, 3717 : 310 - 320
12345