CAV 1997

52 papers

1. A Compositional Rule for Hardware Design Refinement · Kenneth L. McMillan
2. A Provably Correct Embedded Verifier for the Certification of Safety Critical Software · Alessandro Cimatti, Fausto Giunchiglia, Paolo Pecchiari, Bruno Pietra, Joe Profeta, Dario Romano + 2 more
3. An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors · David Cyrluk, M. Oliver Möller, Harald Rueß
4. An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems (Extended Abstract) · Bernard Boigelot, Louis Bronne, Stéphane Rassart
5. An n log n Algorithm for Online BDD Refinement · Nils Klarlund
6. Automatic Abstraction Techniques for Propositional µ-calculus Model Checking · Abelardo Pardo, Gary D. Hachtel
7. Automatic Datapath Extraction for Efficient Usage of HDD · Gila Kamhi, Osnat Weissberg, Limor Fix
8. Boolean and 2-adic Numbers Based Techniques for Verifying Synchronous Design · Gérard Berry
9. 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
10. Construction of Abstract State Graphs with PVS · Susanne Graf, Hassen Saïdi
11. Containing of Regular Languages in Non-Regular Timing Diagram Languages is Decidable · Kathi Fisler
12. Deadlock Checking Using Net Unfoldings · Stephan Melzer, Stefan Römer
13. Efficient Detection of Vacuity in ACTL Formulaas · Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh
14. Efficient Model Checking Using Tabled Resolution · Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Terrance Swift, David Scott Warren
15. Efficient Modeling of Memory Arrays in Symbolic Simulation · Miroslav N. Velev, Randal E. Bryant, Alok Jain
16. Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation · Manish Pandey, Randal E. Bryant
17. Formal Verification - Applications & Case Studies · Martin Rowe
18. Formal Verification of Digital Systems, from ASICs to HW/SW Codesign - a Pragmatic Approach · Roger B. Hughes
19. HYTECH: A Model Checker for Hybrid Systems · Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi
20. MOSEL: A Sound and Efficient Tool for M2L(Str) · Peter Kelb, Tiziana Margaria, Michael Mendler, Claudia Gsottberger
21. Model Checking and Transitive-Closure Logic · Neil Immerman, Moshe Y. Vardi
22. Model Checking in a Microprocessor Design Project · Geoff Barrett, Anthony McIsaac
23. Module Checking Revisited · Orna Kupferman, Moshe Y. Vardi
24. On Combining Formal and Informal Verification · Jun Yuan, Jian Shen, Jacob A. Abraham, Adnan Aziz
25. On-the-Fly Model Checking Under Fairness That Exploits Symmetry · Viktor Gyuris, A. Prasad Sistla
26. Parallelizing the Murphi Verifier · Ulrich Stern, David L. Dill
27. Parametrized Verification of Linear Networks Using Automata as Invariants · A. Prasad Sistla
28. Partial-Order Reduction in Symbolic State Space Exploration · Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani
29. Practical Challenges for Industrial Formal Verification Tools · F. Erich Marschner
30. Programs with Quasi-Stable Channels are Effectively Recognizable (Extended Abstract) · Gérard Cécé, Alain Finkel
31. Relaxed Visibility Enhances Partial Order Reduction · Ilkka Kokkarinen, Doron A. Peled, Antti Valmari
32. RuleBase: Model Checking at IBM · Ilan Beer, Shoham Ben-David, Cindy Eisner, Daniel Geist, Leonid Gluhovsky, Tamir Heyman + 5 more
33. SMC: A Symmetry Based Model Checker for Verification of Liveness Properties · A. Prasad Sistla, L. Miliades, Viktor Gyuris
34. STARI: A Case Study in Compositional and Hierarchical Timing Verification · Serdar Tasiran, Robert K. Brayton
35. Some Progress in the Symbolic Verification of Timed Automata · Marius Bozga, Oded Maler, Amir Pnueli, Sergio Yovine
36. Some Thoughts on Statecharts, 13 Years Later · David Harel
37. Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic · Tevfik Bultan, Richard Gerber, William W. Pugh
38. Symbolic Model Checking with Rich ssertional Languages · Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar
39. TermiLog: A System for Checking Termination of Queries to Logic Programs · Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik
40. The Industrial Success of Verification Tools Based on Stålmarck's Method · Arne Borälv
41. The Invariant Checker: Automated Deductive Verification of Reactive Systems · Hassen Saïdi
42. The PEP Tool · Bernd Grahlmann
43. The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems · Sérgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea
44. Towards a Mechanization of Cryptographic Protocal Verification · Dominique Bolignano
45. Trace Table Based Approach for Pipeline Microprocessor Verification · Jun Sawada, Warren A. Hunt Jr.
46. UPPAAL: Status & Developments · Kim Guldstrand Larsen, Paul Pettersson, Wang Yi
47. Using Compositional Preorders in the Verification of Sliding Window Protocal · Roope Kaivola
48. VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software · Patrice Godefroid
49. Verification of a Chemical Process Leak Test Procedure · Adam L. Turk, Scott T. Probst, Gary J. Powers
50. Weak Bisimulation for Fully Probabilistic Processes · Christel Baier, Holger Hermanns
51. prod 3.2: An Advanced Tool for Efficient Reachability Analysis · Kimmo Varpaaniemi, Keijo Heljanko, Johan Lilius
52. µcke - Efficient µ-Calculus Model Checking · Armin Biere