Relational STE and theorem proving for formal verification of industrial circuit designs

Relational STE and theorem proving for formal verification of industrial circuit designs

Показать другие версии (1)

Model checking by symbolic trajectory evaluation, orchestrated in a flexible functional-programming framework, is a well-established technology for correctness verification of industrial-scale circuit designs. Most verifications in this domain require decomposition into subproblems that symbolic tra...

Полное описание

Библиографические подробности
Главные авторы:	O'Leary, J, Kaivola, R, Melham, T
Формат:	Conference item
Опубликовано:	2013

Схожие документы

Relational STE and Theorem Proving for Formal Verification of Industrial Circuit Designs
по: O'Leary, J, и др.
Опубликовано: (2013)

A Reflective Functional Language for Hardware Design and Theorem Proving
по: Grundy, J, и др.
Опубликовано: (2006)

A Reflective Functional Language for Hardware Design and Theorem Proving
по: Grundy, J, и др.
Опубликовано: (2003)

Xs Are for Trajectory Evaluation‚ Booleans Are for Theorem Proving
по: Aagaard, M, и др.
Опубликовано: (1999)

Xs are for Trajectory Evaluation‚ Booleans are for Theorem Proving (Extended Version)
по: Aagaard, M, и др.
Опубликовано: (2000)

Practical Formal Verification in Microprocessor Design
по: Jones, R, и др.
Опубликовано: (2015)

An Industrially Effective Environment for Formal Hardware Verification
по: Seger, C, и др.
Опубликовано: (2005)

A theorem proving framework for the formal verification of Web Services Composition
по: Petros Papapanagiotou, и др.
Опубликовано: (2011-08-01)

Formal verification of Matrix based MATLAB models using interactive theorem proving
по: Ayesha Gauhar, и др.
Опубликовано: (2021-03-01)

Accurate Theorem Proving for Program Verification
по: Cook, B, и др.
Опубликовано: (2006)

A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving
по: Yassmeen Elderhalli, и др.
Опубликовано: (2019-01-01)

Some Research Issues in Higher Order Logic Theorem Proving
по: Melham, T
Опубликовано: (1996)

Cogent: Accurate theorem proving for program verification
по: Cook, B, и др.
Опубликовано: (2005)

Abstract: Experience with Practical Formal Verification at an Industrial Scale
по: Melham, T
Опубликовано: (2003)

Integrating Model Checking and Theorem Proving in a Reflective Functional Language
по: Melham, T
Опубликовано: (2004)

A Study Of User Activity In Interactive Theorem Proving
по: Aitken, S, и др.
Опубликовано: (1995)

Formal Analysis of Soft Errors using Theorem Proving
по: Sofiène Tahar, и др.
Опубликовано: (2013-07-01)

Interactive Theorem Proving: An Empirical Study of User Activity
по: Aitken, J, и др.
Опубликовано: (1998)

Formal reasoning about systems biology using theorem proving.
по: Adnan Rashid, и др.
Опубликовано: (2017-01-01)

ProoFVer: Natural Logic Theorem Proving for Fact Verification
по: Amrith Krishna, и др.
Опубликовано: (2022-01-01)

Hardware Verification by Formal Proof
по: Birtwistle, G, и др.
Опубликовано: (1988)

Hardware Verification by Formal Proof
по: Birtwistle, G, и др.
Опубликовано: (1988)

Formal Analysis of Language-Based Android Security Using Theorem Proving Approach
по: Wilayat Khan, и др.
Опубликовано: (2019-01-01)

Contextualizing formal verification for systems security engineering
по: Shaked, A, и др.
Опубликовано: (2024)

An AMBA−ARM7 Formal Verification Platform
по: Susanto, K, и др.
Опубликовано: (2003)

A formal CHERI-C semantics for verification
по: Park, SH, и др.
Опубликовано: (2023)

Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic
по: Melham, T
Опубликовано: (1989)

Theorem proving [filem]
Опубликовано: (1969)

Theorem proving [kasetvideo]
Опубликовано: (1969)

A Methodology for Large−Scale Hardware Verification
по: Aagaard, M, и др.
Опубликовано: (2000)

Theorem proving with analytic tableaux and related methods /
по: International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (4th : 1995 : St Goar, Germany), и др.
Опубликовано: (1995)

Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems
по: Zheng Yang, и др.
Опубликовано: (2018-01-01)

System verification : proving the design solution satisfies the requirements /
по: 251885 Grady, Jeffrey O.
Опубликовано: (2007)

Elementary Geometry Theorem Proving
по: Goldstein, Ira
Опубликовано: (2004)

Playing with LEGO and proving theorems
по: Tanswell, FS
Опубликовано: (2017)

Toward the Formalization of Macroscopic Models of Traffic Flow Using Higher-Order-Logic Theorem Proving
по: Adnan Rashid, и др.
Опубликовано: (2020-01-01)

Applications of real number theorem proving in PVS
по: Gottliebsen, H, и др.
Опубликовано: (2013)

Assume−Guarantee Validation for STE Properties within an SVA Environment
по: Khasidashvili, Z, и др.
Опубликовано: (2009)

Assume-guarantee validation for STE properties within an SVA environment
по: Khasidashvili, Z, и др.
Опубликовано: (2009)

Formal analysis of 2D image processing filters using higher-order logic theorem proving
по: Adnan Rashid, и др.
Опубликовано: (2022-06-01)