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

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

Diğer sürümleri göster (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...

Detaylı Bibliyografya
Asıl Yazarlar:	O'Leary, J, Kaivola, R, Melham, T
Materyal Türü:	Conference item
Baskı/Yayın Bilgisi:	2013

Benzer Materyaller

Relational STE and Theorem Proving for Formal Verification of Industrial Circuit Designs
Yazar:: O'Leary, J, ve diğerleri
Baskı/Yayın Bilgisi: (2013)

A Reflective Functional Language for Hardware Design and Theorem Proving
Yazar:: Grundy, J, ve diğerleri
Baskı/Yayın Bilgisi: (2006)

A Reflective Functional Language for Hardware Design and Theorem Proving
Yazar:: Grundy, J, ve diğerleri
Baskı/Yayın Bilgisi: (2003)

Xs Are for Trajectory Evaluation‚ Booleans Are for Theorem Proving
Yazar:: Aagaard, M, ve diğerleri
Baskı/Yayın Bilgisi: (1999)

Xs are for Trajectory Evaluation‚ Booleans are for Theorem Proving (Extended Version)
Yazar:: Aagaard, M, ve diğerleri
Baskı/Yayın Bilgisi: (2000)

Practical Formal Verification in Microprocessor Design
Yazar:: Jones, R, ve diğerleri
Baskı/Yayın Bilgisi: (2015)

An Industrially Effective Environment for Formal Hardware Verification
Yazar:: Seger, C, ve diğerleri
Baskı/Yayın Bilgisi: (2005)

A theorem proving framework for the formal verification of Web Services Composition
Yazar:: Petros Papapanagiotou, ve diğerleri
Baskı/Yayın Bilgisi: (2011-08-01)

Formal verification of Matrix based MATLAB models using interactive theorem proving
Yazar:: Ayesha Gauhar, ve diğerleri
Baskı/Yayın Bilgisi: (2021-03-01)

Accurate Theorem Proving for Program Verification
Yazar:: Cook, B, ve diğerleri
Baskı/Yayın Bilgisi: (2006)

A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving
Yazar:: Yassmeen Elderhalli, ve diğerleri
Baskı/Yayın Bilgisi: (2019-01-01)

Some Research Issues in Higher Order Logic Theorem Proving
Yazar:: Melham, T
Baskı/Yayın Bilgisi: (1996)

Cogent: Accurate theorem proving for program verification
Yazar:: Cook, B, ve diğerleri
Baskı/Yayın Bilgisi: (2005)

Abstract: Experience with Practical Formal Verification at an Industrial Scale
Yazar:: Melham, T
Baskı/Yayın Bilgisi: (2003)

Integrating Model Checking and Theorem Proving in a Reflective Functional Language
Yazar:: Melham, T
Baskı/Yayın Bilgisi: (2004)

A Study Of User Activity In Interactive Theorem Proving
Yazar:: Aitken, S, ve diğerleri
Baskı/Yayın Bilgisi: (1995)

Formal Analysis of Soft Errors using Theorem Proving
Yazar:: Sofiène Tahar, ve diğerleri
Baskı/Yayın Bilgisi: (2013-07-01)

Interactive Theorem Proving: An Empirical Study of User Activity
Yazar:: Aitken, J, ve diğerleri
Baskı/Yayın Bilgisi: (1998)

Formal reasoning about systems biology using theorem proving.
Yazar:: Adnan Rashid, ve diğerleri
Baskı/Yayın Bilgisi: (2017-01-01)

ProoFVer: Natural Logic Theorem Proving for Fact Verification
Yazar:: Amrith Krishna, ve diğerleri
Baskı/Yayın Bilgisi: (2022-01-01)

Hardware Verification by Formal Proof
Yazar:: Birtwistle, G, ve diğerleri
Baskı/Yayın Bilgisi: (1988)

Hardware Verification by Formal Proof
Yazar:: Birtwistle, G, ve diğerleri
Baskı/Yayın Bilgisi: (1988)

Formal Analysis of Language-Based Android Security Using Theorem Proving Approach
Yazar:: Wilayat Khan, ve diğerleri
Baskı/Yayın Bilgisi: (2019-01-01)

Contextualizing formal verification for systems security engineering
Yazar:: Shaked, A, ve diğerleri
Baskı/Yayın Bilgisi: (2024)

An AMBA−ARM7 Formal Verification Platform
Yazar:: Susanto, K, ve diğerleri
Baskı/Yayın Bilgisi: (2003)

A formal CHERI-C semantics for verification
Yazar:: Park, SH, ve diğerleri
Baskı/Yayın Bilgisi: (2023)

Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic
Yazar:: Melham, T
Baskı/Yayın Bilgisi: (1989)

Theorem proving [filem]
Baskı/Yayın Bilgisi: (1969)

Theorem proving [kasetvideo]
Baskı/Yayın Bilgisi: (1969)

A Methodology for Large−Scale Hardware Verification
Yazar:: Aagaard, M, ve diğerleri
Baskı/Yayın Bilgisi: (2000)

Theorem proving with analytic tableaux and related methods /
Yazar:: International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (4th : 1995 : St Goar, Germany), ve diğerleri
Baskı/Yayın Bilgisi: (1995)

Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems
Yazar:: Zheng Yang, ve diğerleri
Baskı/Yayın Bilgisi: (2018-01-01)

System verification : proving the design solution satisfies the requirements /
Yazar:: 251885 Grady, Jeffrey O.
Baskı/Yayın Bilgisi: (2007)

Elementary Geometry Theorem Proving
Yazar:: Goldstein, Ira
Baskı/Yayın Bilgisi: (2004)

Playing with LEGO and proving theorems
Yazar:: Tanswell, FS
Baskı/Yayın Bilgisi: (2017)

Toward the Formalization of Macroscopic Models of Traffic Flow Using Higher-Order-Logic Theorem Proving
Yazar:: Adnan Rashid, ve diğerleri
Baskı/Yayın Bilgisi: (2020-01-01)

Applications of real number theorem proving in PVS
Yazar:: Gottliebsen, H, ve diğerleri
Baskı/Yayın Bilgisi: (2013)

Assume−Guarantee Validation for STE Properties within an SVA Environment
Yazar:: Khasidashvili, Z, ve diğerleri
Baskı/Yayın Bilgisi: (2009)

Assume-guarantee validation for STE properties within an SVA environment
Yazar:: Khasidashvili, Z, ve diğerleri
Baskı/Yayın Bilgisi: (2009)

Formal analysis of 2D image processing filters using higher-order logic theorem proving
Yazar:: Adnan Rashid, ve diğerleri
Baskı/Yayın Bilgisi: (2022-06-01)