IEICE Trans

Keyword : formal verification

Symbolic Representation of Time Petri Nets for Efficient Bounded Model Checking Nao IGAWA Tomoyuki YOKOGAWA Sousuke AMASAKI Masafumi KONDO Yoichiro SATO Kazutami ARIMOTO
Publication: Publication Date: 2020/03/01 Vol. E103-D No. 3 ; pp. 702-705 Type of Manuscript: LETTER Category: Software System Keyword: formal verification, Time Petri Net, SMT Solver, difference logic,
	Summary \| Full Text:PDF(99.9KB)

Formal Verification of a Decision-Tree Ensemble Model and Detection of Its Violation Ranges Naoto SATO Hironobu KURUMA Yuichiroh NAKAGAWA Hideto OGAWA
Publication: Publication Date: 2020/02/01 Vol. E103-D No. 2 ; pp. 363-378 Type of Manuscript: PAPER Category: Dependable Computing Keyword: machine learning, formal verification, decision-tree ensemble model,
	Summary \| Full Text:PDF(1.4MB)

Verifying Scenarios of Proximity-Based Federations among Smart Objects through Model Checking and Its Advantages Reona MINODA Shin-ichi MINATO
Publication: Publication Date: 2017/06/01 Vol. E100-D No. 6 ; pp. 1172-1181 Type of Manuscript: Special Section PAPER (Special Section on Formal Approach) Category: Formal techniques Keyword: ubiquitous computing, catalytic reaction network, formal verification, model checking, smart object,
	Summary \| Full Text:PDF(1.5MB)

A Verification Method of SDN Firewall Applications Miyoung KANG Jin-Young CHOI Inhye KANG Hee Hwan KWAK So Jin AHN Myung-Ki SHIN
Publication: IEICE TRANSACTIONS on Communications Publication Date: 2016/07/01 Vol. E99-B No. 7 ; pp. 1408-1415 Type of Manuscript: PAPER Category: Fundamental Theories for Communications Keyword: software-defined networking, pACSR, formal modeling, formal verification,
	Summary \| Full Text:PDF(1.6MB)

A Verification Method for Single-Flux-Quantum Circuits Using Delay-Based Time Frame Model Takahiro KAWAGUCHI Kazuyoshi TAKAGI Naofumi TAKAGI
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 2015/12/01 Vol. E98-A No. 12 ; pp. 2556-2564 Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms) Category: Logic Synthesis, Test and Verification Keyword: single-flux-quantum circuit, static timing analysis, formal verification,
	Summary \| Full Text:PDF(1.1MB)

A Framework for Verifying the Conformance of Design to Its Formal Specifications Dieu-Huong VU Yuki CHIBA Kenro YATAKE Toshiaki AOKI
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2015/06/01 Vol. E98-D No. 6 ; pp. 1137-1149 Type of Manuscript: Special Section PAPER (Special Section on Formal Approach) Category: Formal Verification Keyword: formal specification, design model, formal verification, model checking, simulation relation,
	Summary \| Full Text:PDF(1.6MB)

Formal Design of Arithmetic Circuits over Galois Fields Based on Normal Basis Representations Kotaro OKAMOTO Naofumi HOMMA Takafumi AOKI
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2014/09/01 Vol. E97-D No. 9 ; pp. 2270-2277 Type of Manuscript: Special Section PAPER (Special Section on Multiple-Valued Logic and VLSI Computing) Category: VLSI Architecture Keyword: arithmetic circuits, formal verification, normal basis, computer algebra,
	Summary \| Full Text:PDF(1.2MB)

Automatic Rectification of Processor Design Bugs Using a Scalable and General Correction Model Amir Masoud GHAREHBAGHI Masahiro FUJITA
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2014/04/01 Vol. E97-D No. 4 ; pp. 852-863 Type of Manuscript: PAPER Category: Dependable Computing Keyword: design error diagnosis, design error correction, micro architecture debugging, formal verification, processors,
	Summary \| Full Text:PDF(615.3KB)

A New Preprocessing Method for Efficient Construction of Decision Diagrams S. R. MALATHI P. SAKTHIVEL
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 2014/02/01 Vol. E97-A No. 2 ; pp. 624-631 Type of Manuscript: PAPER Category: Algorithms and Data Structures Keyword: cubes, decision diagram, PLA format, formal verification, BDD pre-processing,
	Summary \| Full Text:PDF(1.4MB)

Multi-Level Bounded Model Checking with Symbolic Counterexamples Tasuku NISHIHARA Takeshi MATSUMOTO Masahiro FUJITA
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 2011/02/01 Vol. E94-A No. 2 ; pp. 696-705 Type of Manuscript: PAPER Category: VLSI Design Technology and CAD Keyword: formal verification, bounded model checking, finite state machine with datapath, symbolic simulation,
	Summary \| Full Text:PDF(1.4MB)

Word-Level Equivalence Checking in Bit-Level Accuracy by Synthesizing Designs onto Identical Datapath Tasuku NISHIHARA Takeshi MATSUMOTO Masahiro FUJITA
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2009/05/01 Vol. E92-D No. 5 ; pp. 972-984 Type of Manuscript: Special Section PAPER (Special Section on Formal Approach) Category: Hardware Verification Keyword: high-level synthesis, behavioral synthesis, formal verification, equivalence checking,
	Summary \| Full Text:PDF(1022KB)

Arithmetic Circuit Verification Based on Symbolic Computer Algebra Yuki WATANABE Naofumi HOMMA Takafumi AOKI Tatsuo HIGUCHI
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 2008/10/01 Vol. E91-A No. 10 ; pp. 3038-3046 Type of Manuscript: PAPER Category: VLSI Design Technology and CAD Keyword: datapath, arithmetic circuits, formal verification, computer algebra,
	Summary \| Full Text:PDF(754.8KB)

A Conservative Framework for Safety-Failure Checking Frederic BEAL Tomohiro YONEDA Chris J. MYERS
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2008/03/01 Vol. E91-D No. 3 ; pp. 642-654 Type of Manuscript: Special Section PAPER (Special Section on Test and Verification of VLSIs) Category: Verification and Timing Analysis Keyword: asynchronous circuits, speed-independent circuits, safety-failure checking, hazard checking, formal verification, over-approximations,
	Summary \| Full Text:PDF(348.1KB)

An Algebraic Framework for Modeling of Mobile Systems Iakovos OURANOS Petros STEFANEAS Panayiotis FRANGOS
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 2007/09/01 Vol. E90-A No. 9 ; pp. 1986-1999 Type of Manuscript: PAPER Category: Concurrent Systems Keyword: mobile computing, algebraic specification, formal verification, observational transition systems, CafeOBJ, MobileOBJ,
	Summary \| Full Text:PDF(312KB)

Synchronization Verification in System-Level Design with ILP Solvers Thanyapat SAKUNKONCHAK Satoshi KOMATSU Masahiro FUJITA
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 2006/12/01 Vol. E89-A No. 12 ; pp. 3387-3396 Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms) Category: System Level Design Keyword: formal verification, SpecC language, event synchronization, Boolean programs, automatic abstraction refinement, assertion-based verification,
	Summary \| Full Text:PDF(380KB)

Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits Denduang PRADUBSUWUN Tomohiro YONEDA Chris MYERS
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2005/07/01 Vol. E88-D No. 7 ; pp. 1646-1661 Type of Manuscript: PAPER Category: Dependable Computing Keyword: timed trace theory, timed circuits, formal verification, safety/timing failures,
	Summary \| Full Text:PDF(1MB)

Timing Optimization Methodology Based on Replacing Flip-Flops by Latches Ko YOSHIKAWA Keisuke KANAMARU Yasuhiko HAGIHARA Shigeto INUI Yuichi NAKAMURA Takeshi YOSHIMURA
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 2004/12/01 Vol. E87-A No. 12 ; pp. 3151-3158 Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms) Category: Logic Synthesis Keyword: logic synthesis, sequential circuit, timing optimization, level-sensitive latch, formal verification,
	Summary \| Full Text:PDF(402.1KB)

Symbolic Simulation Heuristics for High-Level Hardware Descriptions Including Uninterpreted Functions Kiyoharu HAMAGUCHI
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2004/03/01 Vol. E87-D No. 3 ; pp. 637-641 Type of Manuscript: Special Section LETTER (Special Section on Test and Verification of VLSI) Category: Keyword: formal verification, high-level design verification, uninterpreted function, co-design verification,
	Summary \| Full Text:PDF(139.1KB)

Partial Order Reduction for Timed Circuit Verification Based on Level Oriented Model Tomoya KITAI Yusuke OGURO Tomohiro YONEDA Eric MERCER Chris MYERS
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2003/12/01 Vol. E86-D No. 12 ; pp. 2601-2611 Type of Manuscript: Special Section PAPER (Special Issue on Dependable Computing) Category: Verification and Dependability Analysis Keyword: Level-oriented model, timed asynchronous circuits, formal verification, time Petri nets,
	Summary \| Full Text:PDF(1006.1KB)

Framework of Timed Trace Theoretic Verification Revisited Bin ZHOU Tomohiro YONEDA Chris MYERS
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2002/10/01 Vol. E85-D No. 10 ; pp. 1595-1604 Type of Manuscript: Special Section PAPER (Special Issue on Test and Verification of VLSI) Category: Verification Keyword: timed trace theory, trace structures, time Petri nets, formal verification, asynchronous circuits,
	Summary \| Full Text:PDF(376.6KB)

Verifying Signal-Transition Consistency of High-Level Designs Based on Symbolic Simulation Kiyoharu HAMAGUCHI Hidekazu URUSHIHARA Toshinobu KASHIWABARA
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2002/10/01 Vol. E85-D No. 10 ; pp. 1587-1594 Type of Manuscript: Special Section PAPER (Special Issue on Test and Verification of VLSI) Category: Verification Keyword: formal verification, high-level design verification, uninterpreted function, co-design verification,
	Summary \| Full Text:PDF(213.4KB)

Formal Verification of Data-Path Circuits Based on Symbolic Simulation Yoshifumi MORIHIRO Tomohiro YONEDA
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2002/06/01 Vol. E85-D No. 6 ; pp. 965-974 Type of Manuscript: PAPER Category: Fault Tolerance Keyword: formal verification, simulation, state transition graph, data path, abstraction,
	Summary \| Full Text:PDF(616.1KB)

Efficient Forward Model Checking Algorithm for ω-Regular Properties Hiroaki IWASHITA Tsuneo NAKATA
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 1999/11/25 Vol. E82-A No. 11 ; pp. 2448-2454 Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms) Category: Keyword: forward model checking, ω-regular expression, language emptiness check, symbolic model checking, formal verification,
	Summary \| Full Text:PDF(515.4KB)

A Partially Explicit Method for Efficient Symbolic Checking of Language Containment Kiyoharu HAMAGUCHI Michiyo ICHIHARA Toshinobu KASHIWABARA
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 1999/11/25 Vol. E82-A No. 11 ; pp. 2455-2464 Type of Manuscript: Special Section PAPER (Special Section on VLSI Design and CAD Algorithms) Category: Keyword: formal verification, language containment, symbolic model checking, binary decision diagram (BDD), ω finite automaton,
	Summary \| Full Text:PDF(748.1KB)

Verification of Scalable-Delay-Insensitive Asynchronous Circuits Atsushi YAMAZAKI Hiroshi RYU Tomohiro YONEDA
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 1999/03/25 Vol. E82-D No. 3 ; pp. 701-703 Type of Manuscript: LETTER Category: Fault Tolerant Computing Keyword: formal verification, asynchronous circuit, SDI model, bounded delay model,
	Summary \| Full Text:PDF(99.3KB)

Invariant-Free Formal Verification of Pipelined and Superscalar Controls by Behavior-Covering and Partial Unfolding Toru SHONAI Tsuguo SHIMIZU
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 1999/02/25 Vol. E82-D No. 2 ; pp. 376-388 Type of Manuscript: PAPER Category: Computer Hardware and Design Keyword: formal verification, processor, pipeline, superscalar,
	Summary \| Full Text:PDF(2MB)

Proposal for Incremental Formal Verification Toru SHONAI Kazuhiko MATSUMOTO
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 1998/11/25 Vol. E81-D No. 11 ; pp. 1172-1185 Type of Manuscript: PAPER Category: Computer Hardware and Design Keyword: formal verification, processor, pipeline, BDD, theorem prover,
	Summary \| Full Text:PDF(1.1MB)

CTL Model Checking of Time Petri Nets Using Geometric Regions Tomohiro YONEDA Hikaru RYUBA
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 1998/03/25 Vol. E81-D No. 3 ; pp. 297-306 Type of Manuscript: PAPER Category: Fault Tolerant Computing Keyword: CTL, model checking, time Petri nets, geometric region, formal verification,
	Summary \| Full Text:PDF(880.7KB)

Formal Verification of Totally Self-Checking Properties of Combinational Circuits Kazuo KAWAKUBO Koji TANAKA Hiromi HIRAISHI
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 1997/01/25 Vol. E80-D No. 1 ; pp. 57-62 Type of Manuscript: Special Section PAPER (Special Issue on Fault-Tolerant Computing) Category: Verification Keyword: formal verification, totally self-checking, fault tolerance, binary decision diagram,
	Summary \| Full Text:PDF(508.2KB)

Implicit Representations of Graphs by OBDDs and Patricia BDDs Mizuho IWAIHARA Masanori HIROFUJI
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 1996/07/25 Vol. E79-A No. 7 ; pp. 1068-1078 Type of Manuscript: PAPER Category: VLSI Design Technology and CAD Keyword: binary decision diagram, data structure, formal verification, graph representation, BDD size,
	Summary \| Full Text:PDF(947.8KB)

Formal Verification System for Pipelined Processors Toru SHONAI Tsuguo SHIMIZU
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 1996/06/25 Vol. E79-A No. 6 ; pp. 883-891 Type of Manuscript: PAPER Category: VLSI Design Technology and CAD Keyword: formal verification, pipeline, processor, correctness, mathematical induction,
	Summary \| Full Text:PDF(753KB)

Temporal Verification of Real-Time Systems Sérgio V. CAMPOS Edmund M. CLARKE Wilfredo MARRERO Marius MINEA Hiromi HIRAISHI
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 1995/07/25 Vol. E78-D No. 7 ; pp. 796-801 Type of Manuscript: Special Section PAPER (Special Issue on Verification, Test and Diagnosis of VLSI Systems) Category: Keyword: formal verification, real-time system, temporal logic,
	Summary \| Full Text:PDF(633KB)

Towards Verification of Bit-Slice Circuits--Time-Space Modal Model Checking Approach-- Hiromi HIRAISHI
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 1995/07/25 Vol. E78-D No. 7 ; pp. 791-795 Type of Manuscript: Special Section PAPER (Special Issue on Verification, Test and Diagnosis of VLSI Systems) Category: Keyword: formal verification, time-space modal logic, symbolic model checking, logic design verification, verification of bit-slice circuits,
	Summary \| Full Text:PDF(390.5KB)

A Formal Verification Algorithm for Pipelined Processors Toru SHONAI Tsuguo SHIMIZU
Publication: IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences Publication Date: 1995/05/25 Vol. E78-A No. 5 ; pp. 618-631 Type of Manuscript: PAPER Category: VLSI Design Technology and CAD Keyword: formal verification, hardware verification, specifications, design correctness, proof, pipeline invariant,
	Summary \| Full Text:PDF(1.1MB)

Automatic Generation and Verification of Sufficient Correctness Properties of Synchornous Array Processors Stan Y. LIAO Srinivas DEVADAS
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 1993/09/25 Vol. E76-D No. 9 ; pp. 1030-1038 Type of Manuscript: INVITED PAPER (Special Issue on Synthesis and Verification of Hardware Design) Category: Design Verification Keyword: formal verification, automata, language, and theory of computing, hardware and disign,
	Summary \| Full Text:PDF(836.6KB)

An Application of Regular Temporal Logic to Verification of Fail-Safeness of a Comparator for Redundant System Kazuo KAWAKUBO Hiromi HIRAISHI
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 1993/07/25 Vol. E76-D No. 7 ; pp. 763-770 Type of Manuscript: Special Section PAPER (Special Issue on VLSI Testing and Testable Design) Category: Keyword: fail-safe, fault tolerance, formal verification, temporal logic,
	Summary \| Full Text:PDF(717.1KB)