| 1999 | A Theory of Restrictions for Logics and Automata. | Nils Klarlund |
| 1999 | Test Generation Derived from Model-Checking. | Thierry Jron, Pierre Morel |
| 1999 | TIPPtool: Compositional Specification and Analysis of Markovian Performance Models. | Holger Hermanns, Vassilis Mertsiotakis, Markus Siegle |
| 1999 | Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems. | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani |
| 1999 | Assume-Guarantee Refinement Between Different Time Scales. | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani |
| 1999 | Mechanizing Proofs of Computation Equivalence. | Marcelo Glusman, Shmuel Katz |
| 1999 | Stutter-Invariant Languages, omega-Automata, and Temporal Logic. | Kousha Etessami |
| 1999 | Alternative Approaches to Hardware Verification (abstract). | David L. Dill |
| 1999 | Experience with Predicate Abstraction. | Satyaki Das, David L. Dill, Seungjoon Park |
| 1999 | Improved Automata Generation for Linear Temporal Logic. | Marco Daniele, Fausto Giunchiglia, Moshe Y. Vardi |
| 1999 | NUSMV: A New Symbolic Model Verifier. | Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri |
| 1999 | The Mathematical Foundation fo Symbolic Trajectory Evaluation. | Ching-Tsun Chou |
| 1999 | Latency Insensitive Protocols. | Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli |
| 1999 | A Toolbox for the Analysis of Discrete Event Dynamic Systems. | Peter Buchholz, Peter Kemper |
| 1999 | Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. | Randal E. Bryant, Steven M. German, Miroslav N. Velev |
| 1999 | Model Checking Partial State Spaces with 3-Valued Temporal Logics. | Glenn Bruns, Patrice Godefroid |
| 1999 | Formal Methods for Conformance Testing: Theory Can Be Practical. | Ed Brinksma |
| 1999 | On the Representation of Probabilities over Structured Domains. | Marius Bozga, Oded Maler |
| 1999 | Model Checking Based on Sequential ATPG. | Vamsi Boppana, Sreeranga P. Rajan, Koichiro Takayama, Masahiro Fujita |
| 1999 | Efficient Decision Procedures for Model Checking of Linear Time Logic Properties. | Roderick Bloem, Kavita Ravi, Fabio Somenzi |
| 1999 | Automatic Verification of Combinatorial and Pipelined FFT. | Per Bjesse |
| 1999 | Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. | Armin Biere, Edmund M. Clarke, Richard Raimi, Yunshan Zhu |
| 1999 | Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol. | Batrice Brard, Laurent Fribourg |
| 1999 | Efficient Timed Reachability Analysis Using Clock Difference Diagrams. | Gerd Behrmann, Kim Guldstrand Larsen, Justin Pearson, Carsten Weise, Wang Yi |
| 1999 | Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists. | Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz |