Thomas Jensen - Böcker

This book constitutes the proceedings of the 27th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2026, which took place in Rennes, France, during January 12-13, 2026.The 18 full papers presented in the proceedings were carefully reviewed and selected from 54 submissions. They deal with formal verification model checking, abstract interpretation, fostering interaction, cross-fertilization, and advancement of hybrid methods that combine these and related approaches.

Smart cards are playing an increasingly important role in areas such as ban- 1 king,electroniccommerce,andtelecommunications. TheJavaCard language hasbeenproposedasahigh-levellanguageforprogrammingmulti-application smartcards. Theuseofahigh-levellanguagecanfacilitatethedevelopmentand veri?cation of software for smart cards. The modest code size and the imp- tanceoftheapplicationareasimpliesthatitisbothpossibleanddesirableto developandapplyformalmethodsintheconstructionofsafeandsecureJava Cardsoftware. ThepresentvolumeconstitutestheproceedingsoftheJavaCardworkshop heldinCannes,14September2000. TheworkshopgrewoutoftheINRIAAction deRechercheCoop'erative"JavaCard"andwasorganizedincollaborationwith the Java Card Forum. A call for papers resulted in 14 submissions of which theprogramcommitteeselected11papersforpresentationattheworkshop. In addition,theworkshopfeaturedaninvitedtalkbyDanielLeM'etayer,Trusted Logic,onformalmethodsandsmartcardsecurity. WewishtothankCatherine Godest and Maryse Renaud for their help with preparing the proceedings for thisworkshop. February2001IsabelleAttali ThomasJensen 1 ItshouldbenotedthatJavaCardisatrademarkofSunMicrosystems.Organization ProgramCommittee ProgramChair: IsabelleAttali(INRIA,France) ThomasJensen(IRISA/CNRS,France) Committeemembers: ChristianGoire(BullCP8,France) SebastianHans(SunMicrosystems,USA) PieterHartel(UniversityofSouthampton,UK) PeterHoneyman(UniversityofMichigan,USA) PierreParadinas(Gemplus,France) JoachimPosegga(SAPCorporateResearch,Germany) TableofContents InvitedTalk FormalMethodsinContext:SecurityandJavaCard ...1 D. Bolignano,D. LeM'etayer,C. Loiseaux ContributedPapers ADynamicLogicfortheFormalVeri?cationofJavaCardPrograms ...6 BernhardBeckert ThePACAPPrototype:AToolforDetectingJavaCardIllegalFlow ...25 P. Bieber,J. Cazin,A. ElMarouani,P. Girard,J. -L. Lanet,V. Wiels, G. Zanon CardKt:AutomatedMulti-modalDeductiononJavaCardsfor Multi-applicationSecurity...38 RajeevGor'e,LanDuyNguyen A Programming and a Modelling Perspective on the Evaluation of Java CardImplementations...52 PieterH. Hartel,EduarddeJong SecureInternetSmartcards...73 NaomaruItoi,TomokoFukuzawa,PeterHoneyman IssuesinSmartcardMiddleware...90 RogerKehr,MichaelRohs,HaraldVogt OpenPlatfomSecurity ...98 MarcKekiche?,ForoughKashef,DavidBrewer ASimple(r)InterfaceDistributionMechanismforJavaCard ...114 KsheerabdhiKrishna,MichaelMontgomery AutomaticTestGenerationforJavaCardApplets ...121 HuguesMartin,LydieduBousquet FormalSpeci?cationandVeri?cationofJavaCard'sApplicationIdenti?er Class...137 JoachimvandenBerg,BartJacobs,ErikPoll X TableofContents Security on Your Hand: Secure Filesystems with a "Non-cryptographic" JAVA-Ring...151 R..udigerWeis,BastiaanBakker,StefanLucks AuthorIndex ...163 Formal Methods in Context: Security and Java Card D. Bolignano, D. Le Metayer, and C. Loiseaux Trusted Logic www. trusted-logic. fr 1. Security and Java Card: An Ideal Application Area for Formal Methods The benefits of formal methods for software engineering have been described at length in many research papers. They include among others: Better understanding and improved communication through unambiguous descriptions. Early bug detection thanks to the formalisation of specifications.

The E-smart 2001 international conference on research in smart cards was held in Cannes, France on 19-21 September. The conference was jointlyorganized bythe Java Card Forum, Eurosmart and INRIA, and received helpful ?nancial support from the Conseil R'egional Provence-Alpes-Cote d'Azur. The intention with E-smart is to provide a forum for discussion and exchange of results on smart card development, security, and applications. This year's p- gram was established byan international program committee that examined 38 papers submitted and selected 20 of these for presentation. The list of topics of this year's presentations includes biometrics, cryptography and electronic sig- tures on smart cards, hardware and software solution for smart card security, formal methods for smart card evaluation and certi?cation, architectures for multi-applications and secure open platforms, middleware for smart cards and novel applications of smart cards. The conference also featured an invited talk bySimon Moore from the Universityof Cambridge. Isabelle Attali Thomas Jensen E-smart 2001 program committee co-chairs.Organization Program Committee Isabelle Attali, INRIA Dominique Bolignano, Trusted Logic Bertrand du Castel, Schlumberger Wolfgang E?ng, Giesecke & Devrient Christian Goire, Bull CP8 Pieter Hartel, Universityof Twente Peter Honeyman, University of Michigan Thomas Jensen, IRISA / CNRS Pierre Paradinas, Gemplus Joachim Posegga, SAP AG Peter Ryan, CERT Jean-Paul Thomasson, ST Microelectronics Yasuyoshi Uemura, ECSEC Thanks are due to the following people for their help with the refereeing of papers: Thomas Genet, Valerie Viet Triem Tong, Stefan Friedich, Harald Vogt, Jaap-Henk Hoepman, Neil Henderson, Adam Field, and Jordan Chong.

This book constitutes the refereed proceedings of the 22nd International Static Analysis Symposium, SAS 2015, held in Saint-Malo, France, in September 2015. The 18 papers presented in this volume were carefully reviewed and selected from 44 submissions.