Wojciech Mostowski - Publications

BibTeX

Journal Papers

Daniel Bruns, Wojciech Mostowski, and Mattias Ulbrich. Implementation-level Verification of Algorithms with KeY. Software Tools for Technology Transfer, © Springer, 2013, on-line first, to appear. Springer
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager and Peter H. Schmitt. The KeY Tool. Software and Systems Modeling Journal, Volume 4, Number 1, pages 32-54. © Springer, February 2005. Springer

Conference and Workshop Papers (peer reviewed)

Marieke Huisman and Wojciech Mostowski. A Symbolic Approach to Permission Accounting for Concurrent Reasoning. Proceedings, 14th International Symposium on Parallel and Distributed Computing (ISPDC 2015), Limassol, Cyprus, June 2015, © IEEE Computer Society, to appear. PDF IEEE
Wojciech Mostowski and Mattias Ulbrich. Dynamic Dispatch for Method Contracts through Abstract Predicates. Proceedings, 15th International Conference on MODULARITY (MODULARITY'15). © ACM 2015, 978-1-4503-3249-1/15/03, pages 109-116. ACM
Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich. The KeY Platform for Verification and Analysis of Java Programs. 6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), Vienna, Austria, July 2014. LNCS 8471, pages 1-17, © Springer. PDF Springer
Afshin Amighi, Stefan Blom, Saeed Darabi, Marieke Huisman, Wojciech Mostowski, and Marina Zaharieva-Stojanovski. Verification of Concurrent Systems with VerCors. 14th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Executable Software Models, Bertinoro, Italy, June 2014. LNCS 8483, pages 172-216, © Springer. PDF Springer
Afshin Amighi, Stefan Blom, Marieke Huisman, Wojciech Mostowski, and Marina Zaharieva-Stojanovski. Formal Specifications for Java's Synchronisation Classes. Proceedings, 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, Torino, Italy, February 2014, pages 725-733, © IEEE Computer Society. PDF IEEE
Wojciech Mostowski. A Case Study in Formal Verification using Multiple Explicit Heaps. Proceedings, 2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems (FORTE/FMOODS), Florence, Italy, June 2013. LNCS 7892, pages 20-34, © IFIP. PDF Springer
Wolfgang Ahrendt, Wojciech Mostowski, and Gabriele Paganelli. Real-time Java API Specifications for High Coverage Test Generation. Proceedings, The 10th International Workshop on Java Technologies for Real-time and Embedded Systems - JTRES '12. © ACM 2012, 978-1-4503-1688-0/12/10. ACM
Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst, Jean-Christophe Filliâtre, Radu Grigore, Marieke Huisman, Vladimir Klebanov, Claude Marché, Rosemary Monahan, Wojciech Mostowski, Nadia Polikarpova, Christoph Scheben, Gerhard Schellhorn, Bogdan Tofan, Julian Tschannen, and Mattias Ulbrich. The COST IC0701 Verification Competition 2011. Proceedings, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011), Torino, Italy, October 2011. LNCS 7421, pages 3-21, © Springer. PDF Springer
Wojciech Mostowski and Pim Vullers. Efficient U-Prove Implementation for Anonymous Credentials on Smart Cards. Proceedings, 7th International ICST Conference on Security and Privacy in Communication Networks (SecureComm 2011), London, U.K., September 2011. LNICST 96, pages 243-260, © Springer. PDF Springer
Wojciech Mostowski and Erik Poll. Midlet Navigation Graphs in JML. Post Proceedings, 13th Brazilian Symposium on Formal Methods (SBMF 2010), Natal, Rio Grande do Norte, Brazil, November 2010. LNCS 6527, pages 17-32, © Springer. Best Paper Award! PDF Springer
Lejla Batina, Jaap-Henk Hoepman, Bart Jacobs, Wojciech Mostowski, and Pim Vullers. Developing Efficient Blinded Attribute Certificates on Smart Cards via Pairings. Proceedings, Smart Card Research and Advanced Application Conference CARDIS 2010, Passau, Germany, April 2010. LNCS 6035, pages 207-222, © Springer. PDF Springer
Jip Hogenboom and Wojciech Mostowski. Full Memory Read Attack on a Java Card. Proceedings of 4th Benelux Workshop on Information and System Security, Louvain-la-Neuve, Belgium, November 2009. PDF
Wojciech Mostowski, Erik Poll, Julien Schmaltz, Jan Tretmans, and Ronny Wichers Schreur. Model-Based Testing of Electronic Passports. Proceedings, FMICS 2009, Eindhoven, The Netherlands, November 2009. Poster presentation, LNCS 5825, pages 207-209, © Springer. PDF Poster Springer
Wojciech Mostowski and Erik Poll. Java Card Applet Firewall Exploration and Exploitation. Proceedings, e-Smart 2008, Sophia-Antipolis, France, September 2008. PDF Slides
Wojciech Mostowski and Erik Poll. Malicious Code on Java Card Smartcards: Attacks and Countermeasures. Proceedings, Smart Card Research and Advanced Application Conference CARDIS 2008, Egham, U.K., September 2008. LNCS 5189, pages 1-16, © Springer. PDF Springer
Henning Richter, Wojciech Mostowski, and Erik Poll. Fingerprinting Passports. NLUUG 2008 Spring Conference on Security, Ede, the Netherlands, May 2008. PDF
Wojciech Mostowski. Fully Verified Java Card API Reference Implementation. Proceedings of the Verify 2007 Workshop (associated with CADE 2007), Bremen, Germany, July 2007, CEUR Workshop Proceedings. PDF
Engelbert Hubbers, Wojciech Mostowski, and Erik Poll. Tearing Java Cards. Proceedings, e-Smart 2006, Sophia-Antipolis, France, September 2006. PDF
Wojciech Mostowski. Formal Reasoning about Non-Atomic Java Card Methods in Dynamic Logic. Proceedings, Formal Methods (FM) 2006, Hamilton, Ontario, Canada, August 2006. LNCS 4085, pages 444-459, © Springer. PDF Springer
Wojciech Mostowski. Formalisation and Verification of Java Card Security Properties in Dynamic Logic. Proceedings, Fundamental Approaches to Software Engineering (FASE) Conference, Edinburgh, Scotland, April 2005. LNCS 3442, pages 357-371, © Springer. PDF Springer
Reiner Hähnle and Wojciech Mostowski. Verification of Safety Properties in the Presence of Transactions. Proceedings, Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS'04) Workshop, LNCS 3362, pages 151-171, 2005. © Springer. PDF Springer
Daniel Larsson and Wojciech Mostowski. Specifying Java Card API in OCL. OCL 2.0 Workshop at UML 2003 Conference, San Francisco, U.S.A., October 21, 2003. ENTCS 102C, pages 3-19. © Elsevier, November 2004. PDF Elsevier
Bernhard Beckert and Wojciech Mostowski. A Program Logic for Handling Java Card's Transaction Mechanism. Proceedings, Fundamental Approaches to Software Engineering (FASE) Conference, LNCS 2621, pages 246-260, Warsaw, Poland, April 2003. © Springer. PDF Springer
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski and Peter H. Schmitt. The KeY System: Integrating Object-Oriented Design and Formal Methods. Proceedings, Fundamental Approaches to Software Engineering (FASE) Conference, LNCS 2306, pages 327-330, Grenoble, France, April 2002. © Springer. PDF PDF Springer
Wojciech Mostowski. Rigorous development of Java Card applications. Rigorous Object Oriented Methods Workshop, London, U.K., March 21, 2002. PostScript PDF
Tomasz Janowski and Wojciech Mostowski. Fail-Stop Components by Pattern Matching. Formal Methods for Open Object-Based Distributed Systems Conference, Stanford, California, U.S.A., September 6-8, 2000. PostScript

Posters

Lejla Batina, Bart Jacobs, Wojciech Mostowski, Erik Poll, and Pim Vullers. Security and Privacy of Smartcard-based e-Identity Poster presentation, STW.ICT Conference, Veldhoven, the Netherlands, November 2010. PDF PDF

Chapters in Books

Wojciech Mostowski. Chapter 9. From Sequential Java to Java Card of Verification of Object-Oriented Software: The KeY Approach , pages 375-405, © Springer, 2007. Springer
Wojciech Mostowski. Chapter 14. The Demoney Case Study of Verification of Object-Oriented Software: The KeY Approach , pages 533-568, © Springer, 2007. Springer
Wojciech Mostowski. Appendix B. The KeY Syntax of Verification of Object-Oriented Software: The KeY Approach , pages 599-626, © Springer, 2007. Springer
Tomasz Janowski and Wojciech Mostowski. Chapter 13. Fail-Stop Components by Pattern Matching of Specification Case Studies in RAISE, pages 341-368, © Springer, 2002. Springer

Thesis

Wojciech Mostowski. Formal Development of Safe and Secure Java Card Applets. PhD Thesis, Technical Report 2D, Chalmers University of Technology, Department of Computer Science and Engineering, Göteborg, Sweden, February 2005. PDF
Wojciech Mostowski. Towards Development of Safe and Secure Java Card Applets. Licentiate Thesis, Technical Report 16L, Chalmers University of Technology, Computing Science Department, Göteborg, Sweden, December 2002. PDF

Technical Reports

Afshin Amighi, Stefan Blom, Marieke Huisman, Wojciech Mostowski, and Marina Zaharieva-Stojanovski. Formal Specifications for Java's Synchronisation Classes. Technical Report TR-CTIT-13-18, University of Twente, the Netherlands, September 2013. PDF
Wojciech Mostowski and Erik Poll. Electronic Passports in a Nutshell. Technical Report ICIS-R10004, Radboud University Nijmegen, the Netherlands, June 2010. PDF
Wojciech Mostowski and Erik Poll. Midlet Navigation Graphs in JML. Technical Report ICIS-R09004, Radboud University Nijmegen, the Netherlands, August 2009. PDF
Wojciech Mostowski and Erik Poll. Testing the Java Card Applet Firewall. Technical Report ICIS-R07029, Radboud University Nijmegen, the Netherlands, December 2007. PDF Erratum
Wojciech Mostowski, Jing Pan, Srikanth Akkiraju, Erik de Vink, Erik Poll, and Jerry den Hartog. A Comparison of Java Cards: State-of-Affairs 2006. Technical Report CSR 07-06, Technical University Eindhoven, the Netherlands, 2007. Available on Request
Wojciech Mostowski. Formalisation and Verification of Java Card Security Properties in Dynamic Logic. Technical Report no. 2004-08, Chalmers University of Technology, Computing Science Department, Göteborg, Sweden, October 2004. PDF
Wojciech Mostowski. Java Card Tools for Together Control Center. PDF
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager and Peter H. Schmitt. The KeY Tool. Technical Report no. 2003-05, Chalmers University of Technology, Computing Science Department, Göteborg, Sweden, 2003. PDF