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)