Abstract is missing.
- Practical Challenges for Industrial Formal Verification ToolsF. Erich Marschner. 1-2
- Formal Verification of Digital Systems, from ASICs to HW/SW Codesign - a Pragmatic ApproachRoger B. Hughes. 3-6
- The Industrial Success of Verification Tools Based on Stålmarck s MethodArne Borälv. 7-10
- Formal Verification - Applications & Case StudiesMartin Rowe. 11
- Automatic Abstraction Techniques for Propositional µ-calculus Model CheckingAbelardo Pardo, Gary D. Hachtel. 12-23
- A Compositional Rule for Hardware Design RefinementKenneth L. McMillan. 24-35
- Model Checking RevisitedOrna Kupferman, Moshe Y. Vardi. 36-47
- Using Compositional Preorders in the Verification of Sliding Window ProtocalRoope Kaivola. 48-59
- An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-VectorsDavid Cyrluk, M. Oliver Möller, Harald Rueß. 60-71
- Construction of Abstract State Graphs with PVSSusanne Graf, Hassen Saïdi. 72-83
- Verification of a Chemical Process Leak Test ProcedureAdam L. Turk, Scott T. Probst, Gary J. Powers. 84-94
- Automatic Datapath Extraction for Efficient Usage of HDDGila Kamhi, Osnat Weissberg, Limor Fix. 95-106
- An ::::n:::: log ::::n:::: Algorithm for Online BDD RefinementNils Klarlund. 107-118
- Weak Bisimulation for Fully Probabilistic ProcessesChristel Baier, Holger Hermanns. 119-130
- Towards a Mechanization of Cryptographic Protocal VerificationDominique Bolignano. 131-142
- Efficient Model Checking Using Tabled ResolutionY. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Terrance Swift, David Scott Warren. 143-154
- Containing of Regular Languages in Non-Regular Timing Diagram Languages is DecidableKathi Fisler. 155-166
- An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems (Extended Abstract)Bernard Boigelot, Louis Bronne, Stéphane Rassart. 167-178
- Some Progress in the Symbolic Verification of Timed AutomataMarius Bozga, Oded Maler, Amir Pnueli, Sergio Yovine. 179-190
- STARI: A Case Study in Compositional and Hierarchical Timing VerificationSerdar Tasiran, Robert K. Brayton. 191-201
- A Provably Correct Embedded Verifier for the Certification of Safety Critical SoftwareAlessandro Cimatti, Fausto Giunchiglia, Paolo Pecchiari, Bruno Pietra, Joe Profeta, Dario Romano, Paolo Traverso, Bing Yu. 202-213
- Model Checking in a Microprocessor Design ProjectGeoff Barrett, Anthony McIsaac. 214-225
- Some Thoughts on Statecharts, 13 Years LaterDavid Harel. 226-231
- On-the-Fly Model Checking Under Fairness That Exploits SymmetryViktor Gyuris, A. Prasad Sistla. 232-243
- Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory EvaluationManish Pandey, Randal E. Bryant. 244-255
- Parallelizing the Mur::::phi:::: VerifierUlrich Stern, David L. Dill. 256-278
- Efficient Detection of Vacuity in ACTL FormulaasIlan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh. 279-290
- Model Checking and Transitive-Closure LogicNeil Immerman, Moshe Y. Vardi. 291-302
- Boolean and 2-adic Numbers Based Techniques for Verifying Synchronous DesignGérard Berry. 303
- Programs with Quasi-Stable Channels are Effectively Recognizable (Extended Abstract)Gérard Cécé, Alain Finkel. 304-315
- Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear ConstraintsWilliam Chan, Richard J. Anderson, Paul Beame, David Notkin. 316-327
- Relaxed Visibility Enhances Partial Order ReductionIlkka Kokkarinen, Doron Peled, Antti Valmari. 328-339
- Partial-Order Reduction in Symbolic State Space ExplorationRajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani. 340-351
- Deadlock Checking Using Net UnfoldingsStephan Melzer, Stefan Römer. 352-363
- Trace Table Based Approach for Pipeline Microprocessor VerificationJun Sawada, Warren A. Hunt Jr.. 364-375
- On Combining Formal and Informal VerificationJun Yuan, Jian Shen, Jacob A. Abraham, Adnan Aziz. 376-387
- Efficient Modeling of Memory Arrays in Symbolic SimulationMiroslav N. Velev, Randal E. Bryant, Alok Jain. 388-399
- Symbolic Model Checking of Infinite State Systems Using Presburger ArithmeticTevfik Bultan, Richard Gerber, William Pugh. 400-411
- Parametrized Verification of Linear Networks Using Automata as InvariantsA. Prasad Sistla. 412-423
- Symbolic Model Checking with Rich ssertional LanguagesYonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar. 424-435
- The Invariant Checker: Automated Deductive Verification of Reactive SystemsHassen Saïdi. 436-439
- The PEP ToolBernd Grahlmann. 440-443
- TermiLog: A System for Checking Termination of Queries to Logic ProgramsNaomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik. 444-447
- MOSEL: A Sound and Efficient Tool for M2L(Str)Peter Kelb, Tiziana Margaria, Michael Mendler, Claudia Gsottberger. 448-451
- The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time SystemsSérgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea. 452-455
- UPPAAL: Status & DevelopmentsKim Guldstrand Larsen, Paul Pettersson, Wang Yi. 456-459
- HYTECH: A Model Checker for Hybrid SystemsThomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi. 460-463
- SMC: A Symmetry Based Model Checker for Verification of Liveness PropertiesA. Prasad Sistla, L. Miliades, Viktor Gyuris. 464-467
- µcke - Efficient µ-Calculus Model CheckingArmin Biere. 468-471
- prod 3.2: An Advanced Tool for Efficient Reachability AnalysisKimmo Varpaaniemi, Keijo Heljanko, Johan Lilius. 472-475
- VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive SoftwarePatrice Godefroid. 476-479
- RuleBase: Model Checking at IBMIlan Beer, Shoham Ben-David, Cindy Eisner, Daniel Geist, Leonid Gluhovsky, Tamir Heyman, Avner Landver, P. Paanah, Yoav Rodeh, G. Ronin, Yaron Wolfsthal. 480-483