2 citations · 4 across the 3 of their papers we have counts for
3 papers
Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor
Louis-Emile Ploix, Alasdair Armstrong, Tom Melham +3
The CHERI architecture equips conventional RISC ISAs with significant architectural extensions that provide a hardware-enforced mechanism for memory protection and software compart…
Active Learning of Abstract System Models from Traces using Model Checking [Extended]
Natasha Yogananda Jeppu, Tom Melham, Daniel Kroening
We present a new active model-learning approach to generating abstractions of a system implementation, as finite state automata (FSAs), from execution traces. Given an implementati…
Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version)
Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer +2
Semiconductor companies have increasingly adopted a methodology that starts with a system-level design specification in C/C++/SystemC. This model is extensively simulated to ensure…