Hardware description languages (HDLs) are used today to describe circuits at all levels. In large HDL programs, there is a need for source code reduction techniques to address a my...
Edmund M. Clarke, Masahiro Fujita, Sreeranga P. Ra...
Abstract. This paper describes a semantic connection between the symbolic trajectory evaluation model-checking algorithm and relational verification in higher-order logic. We prov...