9. CAV 1997: Haifa, Israel
- Orna Grumberg:
Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings. Lecture Notes in Computer Science 1254, Springer 1997, ISBN 3-540-63166-6 - Roger B. Hughes:
Formal Verification of Digital Systems, from ASICs to HW/SW Codesign - a Pragmatic Approach. 3-6 - Abelardo Pardo, Gary D. Hachtel:
Automatic Abstraction Techniques for Propositional µ-calculus Model Checking. 12-23 - David Cyrluk, M. Oliver Möller, Harald Rueß:
An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors. 60-71 - Adam L. Turk, Scott T. Probst, Gary J. Powers:
Verification of a Chemical Process Leak Test Procedure. 84-94 - Gila Kamhi, Osnat Weissberg, Limor Fix:
Automatic Datapath Extraction for Efficient Usage of HDD. 95-106 - Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Terrance Swift, David Scott Warren:
Efficient Model Checking Using Tabled Resolution. 143-154 - Kathi Fisler:
Containing of Regular Languages in Non-Regular Timing Diagram Languages is Decidable. 155-166 - Bernard Boigelot, Louis Bronne, Stéphane Rassart:
An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems (Extended Abstract). 167-178 - Marius Bozga, Oded Maler, Amir Pnueli, Sergio Yovine:
Some Progress in the Symbolic Verification of Timed Automata. 179-190 - Serdar Tasiran, Robert K. Brayton:
STARI: A Case Study in Compositional and Hierarchical Timing Verification. 191-201 - Alessandro Cimatti, Fausto Giunchiglia, Paolo Pecchiari, Bruno Pietra, Joe Profeta, Dario Romano, Paolo Traverso, Bing Yu:
A Provably Correct Embedded Verifier for the Certification of Safety Critical Software. 202-213 - Viktor Gyuris, A. Prasad Sistla:
On-the-Fly Model Checking Under Fairness That Exploits Symmetry. 232-243 - Manish Pandey, Randal E. Bryant:
Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation. 244-255 - Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh:
Efficient Detection of Vacuity in ACTL Formulaas. 279-290 - Gérard Cécé, Alain Finkel:
Programs with Quasi-Stable Channels are Effectively Recognizable (Extended Abstract). 304-315 - William Chan, Richard J. Anderson, Paul Beame, David Notkin:
Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints. 316-327 - Ilkka Kokkarinen, Doron A. Peled, Antti Valmari:
Relaxed Visibility Enhances Partial Order Reduction. 328-339 - Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani:
Partial-Order Reduction in Symbolic State Space Exploration. 340-351 - Jun Sawada, Warren A. Hunt Jr.:
Trace Table Based Approach for Pipeline Microprocessor Verification. 364-375 - Jun Yuan, Jian Shen, Jacob A. Abraham, Adnan Aziz:
On Combining Formal and Informal Verification. 376-387 - Miroslav N. Velev, Randal E. Bryant, Alok Jain:
Efficient Modeling of Memory Arrays in Symbolic Simulation. 388-399 - Tevfik Bultan, Richard Gerber, William Pugh:
Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic. 400-411 - A. Prasad Sistla:
Parametrized Verification of Linear Networks Using Automata as Invariants. 412-423 - Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar:
Symbolic Model Checking with Rich ssertional Languages. 424-435
Tool Papers
- Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik:
TermiLog: A System for Checking Termination of Queries to Logic Programs. 444-447 - Peter Kelb, Tiziana Margaria, Michael Mendler, Claudia Gsottberger:
MOSEL: A Sound and Efficient Tool for M2L(Str). 448-451 - Sérgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea:
The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems. 452-455 - Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi:
HYTECH: A Model Checker for Hybrid Systems. 460-463 - A. Prasad Sistla, L. Miliades, Viktor Gyuris:
SMC: A Symmetry Based Model Checker for Verification of Liveness Properties. 464-467 - Kimmo Varpaaniemi, Keijo Heljanko, Johan Lilius:
prod 3.2: An Advanced Tool for Efficient Reachability Analysis. 472-475 - Patrice Godefroid:
VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software. 476-479 - Ilan Beer, Shoham Ben-David, Cindy Eisner, Daniel Geist, Leonid Gluhovsky, Tamir Heyman, Avner Landver, P. Paanah, Yoav Rodeh, G. Ronin, Yaron Wolfsthal:
RuleBase: Model Checking at IBM. 480-483