8 citations · 9 across the 3 of their papers we have counts for
4 papers
Hardware/Software Co-verification Using Path-based Symbolic Execution
Rajdeep Mukherjee, Saurabh Joshi, John O'Leary +2
Conventional tools for formal hardware/software co-verification use bounded model checking techniques to construct a single monolithic propositional formula. Formulas generated in…
Learning Concise Models from Long Execution Traces
Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening +1
Abstract models of system-level behaviour have applications in design exploration, analysis, testing and verification. We describe a new algorithm for automatically extracting usef…
CREST: Hardware Formal Verification with ANSI-C Reference Specifications
Andreas Tiemeyer, Tom Melham, Daniel Kroening +1
This paper presents CREST, a prototype front-end tool intended as an add-on to commercial EDA formal verifcation environments. CREST is an adaptation of the CBMC bounded model chec…
Modeling Algorithms in SystemC and ACL2
John W. O'Leary, David M. Russinoff
We describe the formal language MASC, based on a subset of SystemC and intended for modeling algorithms to be implemented in hardware. By means of a special-purpose parser, an algo…