| 2004 | A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata. Tadaaki Tanimoto, Suguru Sasaki, Akio Nakata, Teruo Higashino |
| 2004 | A Temporal Assertion Extension to Verilog. Kai-Hui Chang, Wei-Ting Tu, Yi-Jong Yeh, Sy-Yen Kuo |
| 2004 | Abstraction Refinement. Pei-Hsin Ho |
| 2004 | Abstraction-Based Model Checking Using Heuristical Refinement. Kairong Qian, Albert Nymeyer |
| 2004 | An Automated Rigorous Review Method for Verifying and Validating Formal Specifications. Shaoying Liu |
| 2004 | Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004. Proceedings Farn Wang |
| 2004 | Büchi Complementation Made Tighter. Ehud Friedgut, Orna Kupferman, Moshe Y. Vardi |
| 2004 | CLP Based Static Property Checking. Tun Li, Yang Guo, Sikun Li |
| 2004 | Component-Wise Instruction-Cache Behavior Prediction. Abdur Rakib, Oleg Parshin, Stephan Thesing, Reinhard Wilhelm |
| 2004 | Composition of Accelerations to Verify Infinite Heterogeneous Systems. Sébastien Bardin, Alain Finkel |
| 2004 | Design and Evaluation of a Symbolic and Abstraction-Based Model Checker. Serge Haddad, Jean-Michel Ilié, Kais Klai |
| 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 | Disjunctive Invariants for Numerical Systems. Jérôme Leroux |
| 2004 | Efficient Representation of Algebraic Expressions. Tsung Lee, Pen-Ho Yu |
| 2004 | Evolution of Model Checking into the EDA Industry. Robert P. Kurshan |
| 2004 | Exploiting Symmetries for Testing Equivalence in the Spi Calculus. Ivan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano |
| 2004 | Fair Testing Revisited: A Process-Algebraic Characterisation of Conflicts. Robi Malik, David Streader, Steve Reeves |
| 2004 | First-Order LTL Model Checking Using MDGs. Fang Wang, Sofiène Tahar, Otmane Aït Mohamed |
| 2004 | Games for Formal Design and Verification of Reactive Systems. Rajeev Alur |
| 2004 | Hybrid System Verification Is Not a Sinecure: The Electronic Throttle Control Case Study. Ansgar Fehnker, Bruce H. Krogh |
| 2004 | Integrity-Enhanced Verification Scheme for Software-Intensive Organizations. Wen-Kui Chang, Chun-Yuan Chen |
| 2004 | Introducing Structural Dynamic Changes in Petri Nets: Marked-Controlled Reconfigurable Nets. Marisa Llorens, Javier Oliver |
| 2004 | Localizing Errors in Counterexample with Iteratively Witness Searching. Shengyu Shen, Ying Qin, Sikun Li |
| 2004 | Modular Model Checking of Software Specifications with Simultaneous Environment Generation. Claudio de la Riva, Javier Tuya |
| 2004 | Mutation Coverage Estimation for Model Checking. Te-Chang Lee, Pao-Ann Hsiung |
| 2004 | Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits. Denduang Pradubsuwun, Tomohiro Yoneda, Chris J. Myers |
| 2004 | Providing Automated Verification in HOL Using MDGs. Tarek Mhamdi, Sofiène Tahar |
| 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 | Rabin Tree and Its Application to Group Key Distribution. Hiroaki Kikuchi |
| 2004 | Reducing Parametric Automata: A Multimedia Protocol Service Case Study. Lin Liu, Jonathan Billington |
| 2004 | SAT-Based Verification of Safe Petri Nets. Shougo Ogata, Tatsuhiro Tsuchiya, Tohru Kikuno |
| 2004 | Search Space Partition and Case Basis Exploration for Reducing Model Checking Complexity. Bai Su, Wenhui Zhang |
| 2004 | Solving Box-Pushing Games via Model Checking with Optimizations. Gihwon Kwon, Taehoon Lee |
| 2004 | Specification, Abduction, and Proof. Konstantine Arkoudas |
| 2004 | Synthesis of State Feedback Controllers for Parameterized Discrete Event Systems. Hans Bherer, Jules Desharnais, Marc Frappier, Richard St-Denis |
| 2004 | Synthesising Attacks on Cryptographic Protocols. David Sinclair, David Gray, Geoff W. Hamilton |
| 2004 | Theorem Proving Languages for Verification. Jean-Pierre Jouannaud |
| 2004 | Tools for Automated Verification of Web Services. Tevfik Bultan, Xiang Fu, Jianwen Su |
| 2004 | Toward Unbounded Model Checking for Region Automata. Fang Yu, Bow-Yaw Wang |
| 2004 | Typeness for omega-Regular Automata. Orna Kupferman, Gila Morgenstern, Aniello Murano |
| 2004 | Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors. Cyrille Artho, Klaus Havelund, Armin Biere |
| 2004 | Using Overlay Networks to Improve VoIP Reliability. Mark J. Karol, Parameshwaran Krishnan, J. Jenny Li |
| 2004 | Validating the Translation of an Industrial Optimizing Compiler. I. Gordin, Raya Leviathan, Amir Pnueli |
| 2004 | Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas. Atsushi Moritomo, Kiyoharu Hamaguchi, Toshinobu Kashiwabara |
| 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 | Verification of WCDMA Protocols and Implementation. Anyi Chen, Jian-Ming Wang, Chiu-Han Hsiao |