Hiromi Hiraishi
Carnegie Mellon University(US)
Publications by Year
Research Areas
Formal Methods in Verification, Radiation Effects in Electronics, VLSI and Analog Circuit Testing, Embedded Systems Design Techniques, Model-Driven Software Engineering Techniques
Most-Cited Works
- → Verification of the Futurebus+ cache coherence protocol(1995)169 cited
- → Verification of the Futurebus+ Cache Coherence Protocol**This research was sponsored in part by the Avionics Laboratory, Wright Research and Development Center, Aeronautical Systems Division (AFSC), U.S. Air Force, Wright-Patterson AFB, Ohio 45433-6543 under Contract F33615-90-C-1465, ARPA Order No. 7597 and in part by the National Science Foundation under Grant no. CCR-9005992 and in part by the Semiconductor Research Corporation under Contract 92-DJ-294 and in part by the U.S.-Israeli Binational Science Foundation and in part by a Japan-U.S. cooperative research grant from the Japanese Society for the Promotion of Scientific Research and in part by U.S.-Japan cooperative research grant number INT-90-16694 from the National Science Foundation.The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. government.(1993)102 cited
- → Branching time regular temporal logic for model checking with linear time complexity(2005)12 cited
- → Vectorized symbolic model checking of computation tree logic for sequential machine verification(1992)7 cited
- Locally exhaustive testing of combinational circuits using linear logic circuits(1988)
- → Formal verification of speed-dependent asynchronous circuits using symbolic model checking of Branching Time Regular Temporal Logic(1992)4 cited
- → Design verification of a microprocessor using branching time regular temporal logic(1993)3 cited
- Regular temporal logic expressively equivalent to finite automata and its application to logic design verification(1992)
- → Design verification of sequential machines based on a model checking algorithm of e-free regular temporal logic(2018)3 cited
- → Verification of deadlock free property of high level robot control(2002)3 cited