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)