Keyword : formal verification


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 computingcatalytic reaction networkformal verificationmodel checkingsmart 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 networkingpACSRformal modelingformal 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 circuitstatic timing analysisformal 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 specificationdesign modelformal verificationmodel checkingsimulation 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 circuitsformal verificationnormal basiscomputer 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 diagnosisdesign error correctionmicro architecture debuggingformal verificationprocessors
 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: 
cubesdecision diagramPLA formatformal verificationBDD 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 verificationbounded model checkingfinite state machine with datapathsymbolic 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 synthesisbehavioral synthesisformal verificationequivalence 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: 
datapatharithmetic circuitsformal verificationcomputer 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 circuitsspeed-independent circuitssafety-failure checkinghazard checkingformal verificationover-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 computingalgebraic specificationformal verificationobservational transition systemsCafeOBJMobileOBJ
 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 verificationSpecC languageevent synchronizationBoolean programsautomatic abstraction refinementassertion-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 theorytimed circuitsformal verificationsafety/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 synthesissequential circuittiming optimizationlevel-sensitive latchformal 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 verificationhigh-level design verificationuninterpreted functionco-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 modeltimed asynchronous circuitsformal verificationtime 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 theorytrace structurestime Petri netsformal verificationasynchronous 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 verificationhigh-level design verificationuninterpreted functionco-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 verificationsimulationstate transition graphdata pathabstraction
 Summary | Full Text:PDF(616.1KB)

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 verificationlanguage containmentsymbolic model checkingbinary decision diagram (BDD)ω finite automaton
 Summary | Full Text:PDF(748.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 expressionlanguage emptiness checksymbolic model checkingformal verification
 Summary | Full Text:PDF(515.4KB)

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 verificationasynchronous circuitSDI modelbounded 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 verificationprocessorpipelinesuperscalar
 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 verificationprocessorpipelineBDDtheorem 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: 
CTLmodel checkingtime Petri netsgeometric regionformal 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 verificationtotally self-checkingfault tolerancebinary 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 diagramdata structureformal verificationgraph representationBDD 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 verificationpipelineprocessorcorrectnessmathematical 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 verificationreal-time systemtemporal 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 verificationtime-space modal logicsymbolic model checkinglogic design verificationverification 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 verificationhardware verificationspecificationsdesign correctnessproofpipeline 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 verificationautomatalanguageand theory of computinghardware 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-safefault toleranceformal verificationtemporal logic
 Summary | Full Text:PDF(717.1KB)