| 1997 | TermiLog: A System for Checking Termination of Queries to Logic Programs. | Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik |
| 1997 | UPPAAL: Status & Developments. | Kim Guldstrand Larsen, Paul Pettersson, Wang Yi |
| 1997 | Module Checking Revisited. | Orna Kupferman, Moshe Y. Vardi |
| 1997 | Relaxed Visibility Enhances Partial Order Reduction. | Ilkka Kokkarinen, Doron A. Peled, Antti Valmari |
| 1997 | An | Nils Klarlund |
| 1997 | Symbolic Model Checking with Rich ssertional Languages. | Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar |
| 1997 | MOSEL: A Sound and Efficient Tool for M2L(Str). | Peter Kelb, Tiziana Margaria, Michael Mendler, Claudia Gsottberger |
| 1997 | Automatic Datapath Extraction for Efficient Usage of HDD. | Gila Kamhi, Osnat Weissberg, Limor Fix |
| 1997 | Using Compositional Preorders in the Verification of Sliding Window Protocal. | Roope Kaivola |
| 1997 | Model Checking and Transitive-Closure Logic. | Neil Immerman, Moshe Y. Vardi |
| 1997 | Formal Verification of Digital Systems, from ASICs to HW/SW Codesign - a Pragmatic Approach. | Roger B. Hughes |
| 1997 | HYTECH: A Model Checker for Hybrid Systems. | Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi |
| 1997 | Some Thoughts on Statecharts, 13 Years Later. | David Harel |
| 1997 | On-the-Fly Model Checking Under Fairness That Exploits Symmetry. | Viktor Gyuris, A. Prasad Sistla |
| 1997 | The PEP Tool. | Bernd Grahlmann |
| 1997 | Construction of Abstract State Graphs with PVS. | Susanne Graf, Hassen Sadi |
| 1997 | VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software. | Patrice Godefroid |
| 1997 | Containing of Regular Languages in Non-Regular Timing Diagram Languages is Decidable. | Kathi Fisler |
| 1997 | An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors. | David Cyrluk, M. Oliver Mller, Harald Rue |
| 1997 | A Provably Correct Embedded Verifier for the Certification of Safety Critical Software. | Alessandro Cimatti, Fausto Giunchiglia, Paolo Pecchiari, Bruno Pietra, Joe Profeta, Dario Romano, Paolo Traverso, Bing Yu |
| 1997 | Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints. | William Chan, Richard J. Anderson, Paul Beame, David Notkin |
| 1997 | Programs with Quasi-Stable Channels are Effectively Recognizable (Extended Abstract). | Grard Cc, Alain Finkel |
| 1997 | The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems. | Srgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea |
| 1997 | Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic. | Tevfik Bultan, Richard Gerber, William W. Pugh |
| 1997 | Some Progress in the Symbolic Verification of Timed Automata. | Marius Bozga, Oded Maler, Amir Pnueli, Sergio Yovine |