| 2004 | Component-Wise Instruction-Cache Behavior Prediction. | Abdur Rakib, Oleg Parshin, Stephan Thesing, Reinhard Wilhelm |
| 2004 | Abstraction-Based Model Checking Using Heuristical Refinement. | Kairong Qian, Albert Nymeyer |
| 2004 | Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits. | Denduang Pradubsuwun, Tomohiro Yoneda, Chris J. Myers |
| 2004 | SAT-Based Verification of Safe Petri Nets. | Shougo Ogata, Tatsuhiro Tsuchiya, Tohru Kikuno |
| 2004 | Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas. | Atsushi Moritomo, Kiyoharu Hamaguchi, Toshinobu Kashiwabara |
| 2004 | Providing Automated Verification in HOL Using MDGs. | Tarek Mhamdi, Sofine Tahar |
| 2004 | Fair Testing Revisited: A Process-Algebraic Characterisation of Conflicts. | Robi Malik, David Streader, Steve Reeves |
| 2004 | Introducing Structural Dynamic Changes in Petri Nets: Marked-Controlled Reconfigurable Nets. | Marisa Llorens, Javier Oliver |
| 2004 | Reducing Parametric Automata: A Multimedia Protocol Service Case Study. | Lin Liu, Jonathan Billington |
| 2004 | An Automated Rigorous Review Method for Verifying and Validating Formal Specifications. | Shaoying Liu |
| 2004 | Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets. | Scott Little, David Walter, Nicholas Seegmiller, Chris J. Myers, Tomohiro Yoneda |
| 2004 | CLP Based Static Property Checking. | Tun Li, Yang Guo, Sikun Li |
| 2004 | Disjunctive Invariants for Numerical Systems. | Jrme Leroux |
| 2004 | Efficient Representation of Algebraic Expressions. | Tsung Lee, Pen-Ho Yu |
| 2004 | Mutation Coverage Estimation for Model Checking. | Te-Chang Lee, Pao-Ann Hsiung |
| 2004 | RCGES: Retargetable Code Generation for Embedded Systems. | Trong-Yen Lee, Yang-Hsin Fan, Tsung-Hsun Yang, Chia-Chun Tsai, Wen-Ta Lee, Yuh-Shyan Hwang |
| 2004 | Solving Box-Pushing Games via Model Checking with Optimizations. | Gihwon Kwon, Taehoon Lee |
| 2004 | Evolution of Model Checking into the EDA Industry. | Robert P. Kurshan |
| 2004 | Typeness for omega-Regular Automata. | Orna Kupferman, Gila Morgenstern, Aniello Murano |
| 2004 | Development of RTOS for PLC Using Formal Methods. | Jin Hyun Kim, Su-Young Lee, Young Ah Ahn, Jae-Hwan Sim, Jin Seok Yang, Na-Young Lee, Jin-Young Choi |
| 2004 | Rabin Tree and Its Application to Group Key Distribution. | Hiroaki Kikuchi |
| 2004 | Using Overlay Networks to Improve VoIP Reliability. | Mark J. Karol, Parameshwaran Krishnan, J. Jenny Li |
| 2004 | Theorem Proving Languages for Verification. | Jean-Pierre Jouannaud |
| 2004 | Abstraction Refinement. | Pei-Hsin Ho |
| 2004 | Design and Evaluation of a Symbolic and Abstraction-Based Model Checker. | Serge Haddad, Jean-Michel Ili, Kais Klai |