Nir Piterman (Ed.) 4 3 Hardware and Software: 4 9 S C Verification and Testing N L 11th International Haifa Verification Conference, HVC 2015 Haifa, Israel, November 17–19, 2015 Proceedings 123 Lecture Notes in Computer Science 9434 Commenced Publication in 1973 Founding and Former Series Editors: Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen Editorial Board David Hutchison Lancaster University, Lancaster, UK Takeo Kanade Carnegie Mellon University, Pittsburgh, PA, USA Josef Kittler University of Surrey, Guildford, UK Jon M. Kleinberg Cornell University, Ithaca, NY, USA Friedemann Mattern ETH Zurich, Zürich, Switzerland John C. Mitchell Stanford University, Stanford, CA, USA Moni Naor Weizmann Institute of Science, Rehovot, Israel C. Pandu Rangan Indian Institute of Technology, Madras, India Bernhard Steffen TU Dortmund University, Dortmund, Germany Demetri Terzopoulos University of California, Los Angeles, CA, USA Doug Tygar University of California, Berkeley, CA, USA Gerhard Weikum Max Planck Institute for Informatics, Saarbrücken, Germany More information about this series at http://www.springer.com/series/7408 Nir Piterman (Ed.) Hardware and Software: fi Veri cation and Testing 11th International fi Haifa Veri cation Conference, HVC 2015 – Haifa, Israel, November 17 19, 2015 Proceedings 123 Editor NirPiterman University of Leicester Leicester UK ISSN 0302-9743 ISSN 1611-3349 (electronic) Lecture Notesin Computer Science ISBN 978-3-319-26286-4 ISBN978-3-319-26287-1 (eBook) DOI 10.1007/978-3-319-26287-1 LibraryofCongressControlNumber:2015953248 LNCSSublibrary:SL2–ProgrammingandSoftwareEngineering SpringerChamHeidelbergNewYorkDordrechtLondon ©SpringerInternationalPublishingSwitzerland2015 Thisworkissubjecttocopyright.AllrightsarereservedbythePublisher,whetherthewholeorpartofthe material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storageandretrieval,electronicadaptation,computersoftware,orbysimilarordissimilarmethodologynow knownorhereafterdeveloped. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Thepublisher,theauthorsandtheeditorsaresafetoassumethattheadviceandinformationinthisbookare believedtobetrueandaccurateatthedateofpublication.Neitherthepublishernortheauthorsortheeditors give a warranty, express or implied, with respect to the material contained herein or for any errors or omissionsthatmayhavebeenmade. Printedonacid-freepaper SpringerInternationalPublishingAGSwitzerlandispartofSpringerScience+BusinessMedia (www.springer.com) Preface Thisvolumecontainstheproceedingsofthe11thHaifaVerificationConference(HVC 2015). The conference was hosted by IBM Research Haifa Laboratory and took place during November 17–19, 2015. It was the 11th event in this series of annual confer- encesdedicatedtoadvancingthestateoftheartandstateofthepracticeinverification and testing. The conference provided a forum for researchers and practitioners from academia and industry to share their work, exchange ideas, and discuss the future directions of testing and verification for hardware, software, and complex hybrid systems.Overall,HVC2015attracted32submissionsinresponsetothecallforpapers. EachsubmissionwasassignedtoatleastthreemembersoftheProgramCommitteeand in some cases additional reviews were solicited from external experts. The Program Committeeselected17papersforpresentation.Inadditiontothe17contributedpapers, the program included five invited talks by Patrice Godefroid (Microsoft Research), Stephen Bailey (Mentor Graphics), Mooly Sagiv (Tel Aviv University), Bodo Hoppe (IBM), and Yoav Hollander (Foretellix LTD). On the last day of the conference, the HVC award was presented to Armin Biere (Yohannes Kepler University Linz) for his contributions to SAT solving and its usage in verification. On November 16, one day before the conference, we held a tutorial day. Iwouldliketoextendourappreciationandsincerethankstolocalorganizationteam fromIBMResearchHaifaLaboratory. Inparticular,Michael Vinov,thegeneralchair, Tali Rabetti, the publicity chair,Tamer Salman, thetutorials chair,Revivit Yankovich the local coordinator, Yair Harry, the webmaster, and the Organizing Committee, whichincludedMosheLevinger,RonnyMorad,AviZiv,KarenYorav,SharonKeidar Barner, and Laurent Fournier. HVC 2015 received sponsorships from IBM, Qual- comm, Cadence Design Systems, Sandisk, Mentor Graphics, and Mellanox Tech- nologies. Submission and evaluation of papers, as well as the preparation of this proceedings volume, were handled by the EasyChair conference management system. September 2015 Nir Piterman Organization Program Committee Roderick Bloem Graz University of Technology, Austria Debapriya Chatterjee IBM Corporation, USA Hana Chockler King’s College, UK Flavio M. de Paula IBM Corporation, USA Rayna Dimitrova MPI-SWS, Germany M.J. Escalona University of Seville, Spain Adrian Evans iRoC Technologies, France Harry Foster Mentor Graphics, USA Franco Fummi University of Verona, Italy Alex Goryachev IBM Research - Haifa, Israel Alberto Griggio Bruno Kessler Foundation, Italy Aarti Gupta Princeton University, USA Laura Kovacs Chalmers University of Technology, Sweden Akash Lal Microsoft Research, India Martin Leucker University of Lübeck, Germany João Lourenço NOVA LINCS - Universidade Nova de Lisboa, Portugal Annalisa Massini Sapienza University of Rome, Italy Mayur Naik Georgia Institute of Technology, USA Jorge A. Navas NASA Ames Research Center, USA Hiren Patel University of Waterloo, Canada Pavithra Prabhakar IMDEA Software Institute, Spain Itai Segall Bell Labs, Israel Martina Seidl Johannes Kepler University Linz, Austria Ohad Shacham Yahoo! Labs, Israel Sharon Shoham The Academic College of Tel Aviv Yaffo, Israel Eli Singerman Intel Corporation, Israel Eran Yahav Technion, Israel Karen Yorav IBM Research - Haifa, Israel Local Organization (IBM Research – Haifa) Michael Vinov General Chair Tali Rabetti Publicity Chair Tamer Salman Tutorial Chair Revivit Yankovich Local Coordinator Yair Harry Web Master VIII Organization Moshe Levinger Organizing Committee Ronny Morad Organizing Committee Avi Ziv Organizing Committee Karen Yorav Organizing Committee Sharon Keidar Barner Organizing Committee Laurent Fournier Organizing Committee Additional Reviewers Bingham, Brad D. Khsidashvili, Zurab Salvo, Ivano Chimento, Jesus Mauricio Lavin, Mark Scheffel, Torben Goldstein, Maayan Mari, Federico Tronci, Enrico Harder, Jannis Meshman, Yuri Zwirchmayr, Jakob Ivrii, Alexander Mover, Sergio Karbyshev, Aleksandr Roveri, Marco Invited Talks Between Testing and Verification: SoftwareModelCheckingviaSystematicTesting Patrice Godefroid Microsoft Research [email protected] Abstract. Dynamic software model checking consists of adapting model checking into a form of systematic testing that is applicable to industrial-size software. Over the last two decades, dozens of tools following this paradigm have been developed for checking concurrent and data-driven software. Com- paredtotraditionalsoftwaretesting,dynamicsoftwaremodelcheckingprovides better coverage, but is more computationally expensive. Compared to more general forms of program verification like interactive theorem proving, this approachprovidesmorelimitedverificationguarantees,butischeaperduetoits higher level of automation. Dynamic software model checking thus offers an attractive practical trade-offbetween testing andformal verification. This talk will review 20 years of research on dynamic software model checking.Itwillhighlightsomekeymilestones,applications,andsuccesses.It will also discusslimitations, disappointments, andfuture work.