| 1997 | A Compositional Rule for Hardware Design Refinement. Kenneth L. McMillan |
| 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 | An Nils Klarlund |
| 1997 | An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors. David Cyrluk, M. Oliver Möller, Harald Rueß |
| 1997 | An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems (Extended Abstract). Bernard Boigelot, Louis Bronne, Stéphane Rassart |
| 1997 | Automatic Abstraction Techniques for Propositional µ-calculus Model Checking. Abelardo Pardo, Gary D. Hachtel |
| 1997 | Automatic Datapath Extraction for Efficient Usage of HDD. Gila Kamhi, Osnat Weissberg, Limor Fix |
| 1997 | Boolean and 2-adic Numbers Based Techniques for Verifying Synchronous Design. Gérard Berry |
| 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 | Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings Orna Grumberg |
| 1997 | Construction of Abstract State Graphs with PVS. Susanne Graf, Hassen Saïdi |
| 1997 | Containing of Regular Languages in Non-Regular Timing Diagram Languages is Decidable. Kathi Fisler |
| 1997 | Deadlock Checking Using Net Unfoldings. Stephan Melzer, Stefan Römer |
| 1997 | Efficient Detection of Vacuity in ACTL Formulaas. Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh |
| 1997 | Efficient Model Checking Using Tabled Resolution. Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Terrance Swift, David Scott Warren |
| 1997 | Efficient Modeling of Memory Arrays in Symbolic Simulation. Miroslav N. Velev, Randal E. Bryant, Alok Jain |
| 1997 | Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation. Manish Pandey, Randal E. Bryant |
| 1997 | Formal Verification - Applications & Case Studies. Martin Rowe |
| 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 | MOSEL: A Sound and Efficient Tool for M2L(Str). Peter Kelb, Tiziana Margaria, Michael Mendler, Claudia Gsottberger |
| 1997 | Model Checking and Transitive-Closure Logic. Neil Immerman, Moshe Y. Vardi |
| 1997 | Model Checking in a Microprocessor Design Project. Geoff Barrett, Anthony McIsaac |
| 1997 | Module Checking Revisited. Orna Kupferman, Moshe Y. Vardi |
| 1997 | On Combining Formal and Informal Verification. Jun Yuan, Jian Shen, Jacob A. Abraham, Adnan Aziz |
| 1997 | On-the-Fly Model Checking Under Fairness That Exploits Symmetry. Viktor Gyuris, A. Prasad Sistla |
| 1997 | Parallelizing the Mur Ulrich Stern, David L. Dill |
| 1997 | Parametrized Verification of Linear Networks Using Automata as Invariants. A. Prasad Sistla |
| 1997 | Partial-Order Reduction in Symbolic State Space Exploration. Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani |
| 1997 | Practical Challenges for Industrial Formal Verification Tools. F. Erich Marschner |
| 1997 | Programs with Quasi-Stable Channels are Effectively Recognizable (Extended Abstract). Gérard Cécé, Alain Finkel |
| 1997 | Relaxed Visibility Enhances Partial Order Reduction. Ilkka Kokkarinen, Doron A. Peled, Antti Valmari |
| 1997 | RuleBase: Model Checking at IBM. Ilan Beer, Shoham Ben-David, Cindy Eisner, Daniel Geist, Leonid Gluhovsky, Tamir Heyman, Avner Landver, P. Paanah, Yoav Rodeh, G. Ronin, Yaron Wolfsthal |
| 1997 | SMC: A Symmetry Based Model Checker for Verification of Liveness Properties. A. Prasad Sistla, L. Miliades, Viktor Gyuris |
| 1997 | STARI: A Case Study in Compositional and Hierarchical Timing Verification. Serdar Tasiran, Robert K. Brayton |
| 1997 | Some Progress in the Symbolic Verification of Timed Automata. Marius Bozga, Oded Maler, Amir Pnueli, Sergio Yovine |
| 1997 | Some Thoughts on Statecharts, 13 Years Later. David Harel |
| 1997 | Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic. Tevfik Bultan, Richard Gerber, William W. Pugh |
| 1997 | Symbolic Model Checking with Rich ssertional Languages. Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar |
| 1997 | TermiLog: A System for Checking Termination of Queries to Logic Programs. Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik |
| 1997 | The Industrial Success of Verification Tools Based on Stålmarck's Method. Arne Borälv |
| 1997 | The Invariant Checker: Automated Deductive Verification of Reactive Systems. Hassen Saïdi |
| 1997 | The PEP Tool. Bernd Grahlmann |
| 1997 | The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems. Sérgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea |
| 1997 | Towards a Mechanization of Cryptographic Protocal Verification. Dominique Bolignano |
| 1997 | Trace Table Based Approach for Pipeline Microprocessor Verification. Jun Sawada, Warren A. Hunt Jr. |
| 1997 | UPPAAL: Status & Developments. Kim Guldstrand Larsen, Paul Pettersson, Wang Yi |
| 1997 | Using Compositional Preorders in the Verification of Sliding Window Protocal. Roope Kaivola |
| 1997 | VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software. Patrice Godefroid |
| 1997 | Verification of a Chemical Process Leak Test Procedure. Adam L. Turk, Scott T. Probst, Gary J. Powers |
| 1997 | Weak Bisimulation for Fully Probabilistic Processes. Christel Baier, Holger Hermanns |
| 1997 | prod 3.2: An Advanced Tool for Efficient Reachability Analysis. Kimmo Varpaaniemi, Keijo Heljanko, Johan Lilius |
| 1997 | µcke - Efficient µ-Calculus Model Checking. Armin Biere |