Lecture Notes in Computer Science 3114 CommencedPublicationin1973 FoundingandFormerSeriesEditors: GerhardGoos,JurisHartmanis,andJanvanLeeuwen EditorialBoard TakeoKanade CarnegieMellonUniversity,Pittsburgh,PA,USA JosefKittler UniversityofSurrey,Guildford,UK JonM.Kleinberg CornellUniversity,Ithaca,NY,USA FriedemannMattern ETHZurich,Switzerland JohnC.Mitchell StanfordUniversity,CA,USA MoniNaor WeizmannInstituteofScience,Rehovot,Israel OscarNierstrasz UniversityofBern,Switzerland C.PanduRangan IndianInstituteofTechnology,Madras,India BernhardSteffen UniversityofDortmund,Germany MadhuSudan MassachusettsInstituteofTechnology,MA,USA DemetriTerzopoulos NewYorkUniversity,NY,USA DougTygar UniversityofCalifornia,Berkeley,CA,USA MosheY.Vardi RiceUniversity,Houston,TX,USA GerhardWeikum Max-PlanckInstituteofComputerScience,Saarbruecken,Germany Rajeev Alur Doron A. Peled (Eds.) Computer Aided Verification 16th International Conference, CAV 2004 Boston, MA, USA, July 13-17, 2004 Proceedings 1 3 VolumeEditors RajeevAlur UniversityofPensylvania,DepartmentofComputerundInformationScience 3330WalnutStreet,Philadelphia,PA19104,USA E-mail:[email protected] DoronA.Peled UniversityofWarwick,DepartmentofComputerScience Coventry,CV47AL,UK E-mail:[email protected] LibraryofCongressControlNumber:2004108215 CRSubjectClassification(1998):F.3,D.2.4,D.2.2,F.4.1,I.2.3,B.7.2,C.3 ISSN0302-9743 ISBN3-540-22342-8Springer-VerlagBerlinHeidelbergNewYork Thisworkissubjecttocopyright.Allrightsarereserved,whetherthewholeorpartofthematerialis concerned,specificallytherightsoftranslation,reprinting,re-useofillustrations,recitation,broadcasting, reproductiononmicrofilmsorinanyotherway,andstorageindatabanks.Duplicationofthispublication orpartsthereofispermittedonlyundertheprovisionsoftheGermanCopyrightLawofSeptember9,1965, initscurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer-Verlag.Violationsare liabletoprosecutionundertheGermanCopyrightLaw. Springer-VerlagisapartofSpringerScience+BusinessMedia springeronline.com ©Springer-VerlagBerlinHeidelberg2004 PrintedinGermany Typesetting:Camera-readybyauthor,dataconversionbyOlgunComputergrafik Printedonacid-freepaper SPIN:11015802 06/3142 543210 Preface ThisvolumecontainstheproceedingsoftheconferenceonComputerAidedVeri- fication,CAV2004,heldinBoston,Massachusetts,USA,July13–17,2004.CAV 2004wasthe 16thinaseriesofconferencesdedicatedtotheadvancementofthe theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical re- sults to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. The conferencehastraditionallydrawnparticipationfromresearchersaswellas practitioners in both academia and industry. CAV 2004 was colocated with the ACM International Symposium on Soft- ware Testing and Analysis (ISSTA 2004), and was partially sponsored by the ACMSIGSOFT.Thecolocationreflectstheincreasingsynergybetweenresearch on verification and testing, and emerging applications of formal verification to softwareanalysis.JointCAV-ISSTAeventsincludedadistinguishedplenarylec- ture by David Harel and a special session exploring various approaches to the specification and verification of concurrent software organized by Shaz Qadeer. The program of the conference consisted of 32 regular papers and 16 tool pa- pers, selected from a total of 144 submissions. The conference was preceded by a tutorialon processorverification,onJuly 12,2004,with three invited lectures by Randal E. Bryant, David L. Dill and Warren A. Hunt, Jr. The conference also included invited talks by Mary Jean Harrold and Thomas W. Reps. Two workshops were associated with CAV 2004: – BMC 2004: Second International Workshop on Bounded Model Checking – GDV 2004: Games in Design and Verification We would like to thank all the program committee members and the sub- referees for their excellent work in evaluating the submissions and the selection of the program.Our thanks also go to the steering committee members and the organizers of CAV 2003 for their helpful advice. Special thanks go to George Avrunin,the ISSTAGeneralChair,andErinDolanofACM,fortheir helpwith the local organization. We would like to acknowledge the generous sponsorship of Cadence Design Systems, IBM Research, Intel Research, Microsoft Research andtheJohnVonNeumannMinervaCenterforVerificationofReactiveSystems. Their support helped us reduce the registrationfee for the graduate students. TheCAVcommunityisdeeplysaddenedbythesuddendemiseofDr.RobT. Gerth. Rob was a highly regarded researcher with many notable contributions to the theory and practice of formal verification. For CAV 2004,we had invited Rob to join the program committee as well as to give a tutorial on processor verification. This LNCS volume containing the CAV 2004 proceedings is dedi- cated to Rob, and includes a special presentation, commemorating his scientific accomplishments and collaborations. May 2004 Rajeev Alur and Doron A. Peled Program Committee Rajeev Alur (University of Pennsylvania, USA, co-chair) David Basin (ETH Zurich, Switzerland) Armin Biere (ETH Zurich, Switzerland) Dennis Dams (Bell Labs, Lucent Technologies, USA) David L. Dill (Stanford University, USA) E. Allen Emerson (University of Texas at Austin, USA) Kousha Etessami (University of Edinburgh, UK) Steven German (IBM Research, USA) Mike Gordon (University of Cambridge, UK) Aarti Gupta (NEC Labs America, USA) Klaus Havelund (NASA Ames, USA) Holger Hermanns (Saarland University, Germany) Alan Hu (University of British Columbia, Canada) Bengt Jonsson (Uppsala University, Sweden) Andreas Kuehlman (Cadence Berkeley Labs, USA) Salvatore La Torre (University of Salerno, Italy) Oded Maler (Verimag, France) Pete Manolios (Georgia Institute of Technology, USA) Ken McMillan (Cadence Berkeley Labs, USA) Anca Muscholl (University of Paris 7, France) Chris Myers (University of Utah, USA) Doron Peled (University of Warwick, UK, co-chair) Fabio Somenzi (University of Colorado at Boulder, USA) Amir Pnueli (New York University, USA) Shaz Qadeer (Microsoft Research, USA) Jun Sawada (IBM Research, USA) Frits Vaandrager (University of Nijmegen, The Netherlands) Pierre Wolper (University of Liege, Belgium) Sergio Yovine (Verimag, France) Steering Committee Edmund M. Clarke (Carnegie Mellon University, USA) Robert P. Kurshan (Cadence, USA) Amir Pnueli (New York University, USA) Mike Gordon (University of Cambridge, UK) Referees ParoshAbdulla Tamarah Arons Christel Baier Nina Amla Cyrille Artho Ittai Balaban Suzana Andova Eugene Asarin Howard Barringer VIII Organization Jason Baumgartner Marc Herbstritt Marcus Nilsson Bernd Becker Gerard Holzmann Iulian Ober Michael Benedikt Jozef Hooman Alfredo Olivero Saddek Bensalem Michael Huth Joel Ouaknine Sergey Berezin Franjo Ivancic Domenico Parente Mikhail Bernadsky Paul Jackson Gennaro Parlato Jesse Bingham Sadegh Jahanpour Viresh Paruthi Roderick Bloem Petr Jancar Corina Pasareanu Johan Blom Geert Janssen Mark Pichora Bernard Boigelot Bertrand Jeannet Nir Piterman Dragan Bosnacki Sven Johr Andreas Podelski Ahmed Bouajjani Rajeev Joshi Ramanujam Marius Bozga Vineet Kahlon Kavita Ravi Tevfik Bultan Huthasana Kalyanam Theo Ruys Donald Chai Joost-Pieter Katoen Gerardo Schneider Jacob Chang Nathan Kitchen Viktor Schuppan Marsha Chechik Felix Klaedtke Sanjit Seshia Ling Cheung Nils Klarlund Ilya Shlyakhter Alessandro Cimatti Christos Kloukinas Eric Smith Scott Cotton Matthias Kuntz Oleg Sokolsky Thao Dang Orna Kupferman Sudarshan Srinivasan Conrado Daws Shuvendu Lahiri Ian Stark Johann Deneux Yassine Lakhnech Martin Steffen Jyotirmoy Deshmukh Frederic Lang Colin Stirling Peter Dillinger Ruggiero Lanotte Marielle Stoelinga Xiaoqun Du Joyce Lauer Val Tannen Elena Dubrova Ranko Lazic P.S. Thiagarajan Avijit Dutta Axel Legay Tayssir Touili Marco Faella Martin Leucker Richard Trefler Manuel Fahndrich Bing Li Stavros Tripakis Ansgar Fehnker Scott Little Yaroslav Usenko Xiushan Feng Rupak Majumdar Antti Valmari David Fink Shawn Manley Helmut Veith Bernd Finkbeiner Heiko Mantel Miroslav Velev Carsten Fritz Marco Maratea Willem Visser Marc Geilen Eric Mercer Daron Vroon Blaise Genest Markus Mueller-Olm Thomas Wahl Philippe Gerner Aniello Murano David Walter Alain Girault Madan Musuvathi Thomas Wilke Amit Goel David N. Jansen Aleksander Zaks Gregor Goessler Kedar Namjoshi Yunshan Zhu Peter Habermehl Margherita Napoli Lenore Zuck Malek Haroud Kelvin Ng Rob van Glabbeek John Hatcliff Dejan Nickovic Table of Contents Rob Tristan Gerth: 1956–2003...................................... 1 Static ProgramAnalysis via 3-Valued Logic .......................... 15 Thomas W. Reps, Mooly Sagiv, and Reinhard Wilhelm Deductive Verification of Pipelined Machines Using First-Order Quantification.................................... 31 Sandip Ray and Warren A. Hunt, Jr. A Formal Reduction for Lock-Free ParallelAlgorithms................. 44 Hui Gao and Wim H. Hesselink An Efficiently Checkable, Proof-BasedFormulation of Vacuity in Model Checking ................................................ 57 Kedar S. Namjoshi Termination of Linear Programs .................................... 70 Ashish Tiwari Symbolic Model Checking of Non-regular Properties................... 83 Martin Lange Proving More Properties with Bounded Model Checking ............... 96 Mohammad Awedh and Fabio Somenzi Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings............................................... 109 Claus Schro¨ter and Victor Khomenko Using Interface Refinement to Integrate Formal Verification into the Design Cycle.............................................. 122 Jacob Chang, Sergey Berezin, and David L. Dill Indexed Predicate Discovery for Unbounded System Verification ........ 135 Shuvendu K. Lahiri and Randal E. Bryant Range Allocation for Separation Logic............................... 148 Muralidhar Talupur, Nishant Sinha, Ofer Strichman, and Amir Pnueli An Experimental Evaluation of Ground Decision Procedures ........... 162 Leonardo de Moura and Harald Rueß X Table of Contents DPLL(T): Fast Decision Procedures................................. 175 HaraldGanzinger,GeorgeHagen,RobertNieuwenhuis,AlbertOliveras, and Cesare Tinelli Verifying ω-Regular Properties of Markov Chains ..................... 189 Doron Bustan, Sasha Rubin, and Moshe Y. Vardi Statistical Model Checking of Black-Box Probabilistic Systems.......... 202 Koushik Sen, Mahesh Viswanathan, and Gul Agha Compositional Specification and Model Checking in GSTE ............. 216 Jin Yang and Carl-Johan H. Seger GSTE Is Partitioned Model Checking................................ 229 Roberto Sebastiani, Eli Singerman, Stefano Tonetta, and Moshe Y. Vardi Stuck-Free Conformance ........................................... 242 C´edric Fournet, Tony Hoare, Sriram K. Rajamani, and Jakob Rehof Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors................................. 255 Amit Goel and Randal E. Bryant Functional Dependency for Verification Reduction..................... 268 Jie-Hong R. Jiang and Robert K. Brayton Verification via Structure Simulation ................................ 281 Niel Immerman, Alexander Rabinovich, Thomas W. Reps, Mooly Sagiv, and Great Yorsh Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures .................................... 295 Farn Wang Abstraction-Based Satisfiability Solving of Presburger Arithmetic ....... 308 DanielKroening,Jo¨elOuaknine,SanjitA.Seshia,andOferStrichman Widening Arithmetic Automata .................................... 321 Constantinos Bartzis and Tevfik Bultan Why Model Checking Can Improve WCET Analysis................... 334 Alexander Metzner Regular Model Checking for LTL(MSO) ............................. 348 Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d’Orso, and Mayank Saksena Image Computation in Infinite State Model Checking.................. 361 Alain Finkel and J´eroˆme Leroux Table of Contents XI Abstract Regular Model Checking................................... 372 Ahmed Bouajjani, Peter Habermehl, and Toma´ˇs Vojnar Global Model-Checking of Infinite-State Systems...................... 387 Nir Piterman and Moshe Y. Vardi QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings ............................................. 401 Ganesh Gopalakrishnan, Yue Yang, and Hemanthkumar Sivaraj Verification of an Advanced mips-Type Out-of-Order Execution Algorithm .............................................. 414 Tamarah Arons Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values......................................... 427 Jesse Bingham, Anne Condon, Alan J. Hu, Shaz Qadeer, and Zhichuan Zhang Efficient Modeling of Embedded Memories in Bounded Model Checking.. 440 Malay K. Ganai, Aarti Gupta, and Pranav Ashar Understanding Counterexamples with explain ....................... 453 Alex Groce, Daniel Kroening, and Flavio Lerda Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement................................ 457 Thomas Ball, Byron Cook, Shuvendu K. Lahiri, and Lintao Zhang JNuke: Efficient Dynamic Analysis for Java .......................... 462 Cyrille Artho, Viktor Schuppan, Armin Biere, Pascal Eugster, Marcel Baur, and Boris Zweimu¨ller The HiVy Tool Set................................................ 466 Paula J. Pingree and Erich Mikk ObsSlice: A Timed Automata Slicer Based on Observers.............. 470 V´ıctor Braberman, Diego Garbervetsky, and Alfredo Olivero The UCLID Decision Procedure ................................... 475 Shuvendu K. Lahiri and Sanjit A. Seshia MCK: Model Checking the Logic of Knowledge ...................... 479 Peter Gammie and Ron van der Meyden Zing: A Model Checker for Concurrent Software ...................... 484 Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof, and Yichen Xie