Sciweavers

FMCAD
2009
Springer
14 years 4 months ago
Industrial strength refinement checking
This paper discusses a methodology used on an industrial hardware development project to validate various cache-coherence protocol components. The idea is to use a high level model...
Jesse D. Bingham, John Erickson, Gaurav Singh, Fle...
FMCAD
2009
Springer
14 years 4 months ago
Generalized, efficient array decision procedures
Abstract--The theory of arrays is ubiquitous in the context of software and hardware verification and symbolic analysis. The basic array theory was introduced by McCarthy and allow...
Leonardo Mendonça de Moura, Nikolaj Bj&osla...
FMCAD
2009
Springer
14 years 5 months ago
Hardware/software co-verification of cryptographic algorithms using Cryptol
Levent Erkök, Magnus Carlsson, Adam Wick
FMCAD
2009
Springer
14 years 7 months ago
Finding heap-bounds for hardware synthesis
Abstract—Dynamically allocated and manipulated data structures cannot be translated into hardware unless there is an upper bound on the amount of memory the program uses during a...
Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey...
FMCAD
2009
Springer
14 years 7 months ago
MCC: A runtime verification tool for MCAPI user applications
Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer,...
FMCAD
2009
Springer
14 years 7 months ago
Software model checking via large-block encoding
Abstract—Several successful approaches to software verificabased on the construction and analysis of an abstract reachability tree (ART). The ART represents unwindings of the co...
Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M...
FMCAD
2009
Springer
14 years 7 months ago
Formal verification of correctness and performance of random priority-based arbiters
Krishnan Kailas, Viresh Paruthi, Brian Monwai
FMCAD
2009
Springer
14 years 7 months ago
Debugging formal specifications using simple counterstrategies
Robert Könighofer, Georg Hofferek, Roderick B...
FMCAD
2009
Springer
14 years 7 months ago
SAT-based synthesis of clock gating functions using 3-valued abstraction
Valued Abstraction Oleg Rokhlenko Joint work with Eli Arbel and Karen Yorav IBM Haifa Research Labs
Eli Arbel, Oleg Rokhlenko, Karen Yorav
FMCAD
2009
Springer
14 years 7 months ago
Connecting pre-silicon and post-silicon verification
Sandip Ray, Warren A. Hunt Jr.