Wojciech Mostowski

Wojciech Mostowski

Wojciech Mostowski, Associate Professor, Ph.D.

Family Name: Mostowski
Given Name: Wojciech
Role: Associate Professor
Title: Ph.D.
Subject: 
Organization: Computing and Electronics for Real-time Embedded Systems
Email: Wojciech.Mostowski@hh.se
url: http://ceres.hh.se/mediawiki/Wojciech_Mostowski
Phone: +46-35-16-7137
Cell Phone: 

Personal Info

My academic history before I took up the position at CERES:

• Post-Doc at the Formal Methods and Tools (FMT) group at the University of Twente in the Netherlands working on the VerCors project with Marieke Huisman,
• Visiting Lecturer at Division of Software Technology at Chalmers University of Technology in Sweden,
• Post-Doc at the Digital Security group at Radboud University Nijmegen in the Netherlands working with Erik Poll on several EU and national projects,
• Ph.D. studies at (what is now) Division of Software Technology at Chalmers University of Technology in Sweden, Ph.D. supervisor Reiner Hähnle.

Research Interests

• Formal verification of object oriented software, in particular Java, with the emphasis on practice,
• Security and implementation of smart card applications and products,
• Embedded systems for automotive applications.

Projects

I currently work on:

• AUTO-CAAS (100%).

Publications

• Publication List,
• Google Scholar,
• Research Gate (not yet up-to-date),
• KeY Book.

(Past) Projects, Events, Program Committees

• PC member Fifth Workshop on Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy'15),
• PC member IEEE International Workshop on Formal Methods Integration (FMi) 2015,
• Scientific organiser of the Lorentz Center workshop on JML: Advancing Specification Language Methodologies,
• Local organiser and publicity chair of the AVoCS 2014 workshop,
• Participation in the VerifyThis 2012 Verification Competition at FM 2012, team KeY formed with Daniel Bruns,
• CHARTER JML Workshop,
• Participation in the FoVeOOS 2011 Verification Competition, team KeY formed with Christoph Scheben,
• Organizer of the 10th KeY Symposium,
• PC member Formal Verification of Object-Oriented Software (FoVeOOS) 2011,
• COST Action Training School 2011 tutorial on Formal Verification of Java Card programs,
• PC member Formal Techniques for Java-like Programs (FTfJP) 2011,
• For Frontex, in cooperation with PwC and Collis we performed an EU-wide study of electronic (biometric) passports,
• Best Paper Award at 13th Brazilian Symposium on Formal Methods (SBMF 2010),
• PC member Formal Verification of Object-Oriented Software (FoVeOOS) 2010,
• PC member Smart Card Research and Advanced Applications (CARDIS) 2010,
• OV Chip 2.0 is concerned with developing state-of-the-art privacy-friendly protocols for e-Transport/e-Ticketing and e-Identity,
• CHARTER is concerned with developing concepts, methods, and tools for embedded system design and deployment that will enable developers to master the complexity and substantially improve the development, verification and certification of critical embedded systems. Real-time Java plays a major role in this effort,
• COST action IC0701: Formal Verification of Object-Oriented Software.,
• PC member Formal Techniques for Java-like Programs (FTfJP) 2007,
• Mobius – Enabling proof-carrying code for Java on mobile devices,
• European Science Foundation Workshop on Challenges in Java Program Verification,
• PinPas Java Card – Side-Channel Analysis of Java Card,
• KeY Project - Integrating Object-Oriented Design with Deductive Verification.

Software and Other Code

• PVS files accompanying the A Symbolic Approach to Permission Accounting for Concurrent Reasoning. paper: Permissions_PVS.zip. All other examples mentioned in the paper are now part of the development version of the The KeY System,
• The KeY System – long time developer, contributor, and maintainer,
• Java Machine Readable Travel Documents (JMRTD) – contributor,
• Smart Card Utilities for Better Access – contributor,
• Electronic Driving License (ISO18013) – lead developer and maintainer, based on Java JMRTD,
• ISO7816 PKI Java Card signing applet – lead developer and maintainer,
• Global Platform for Java SmartCardIO – lead developer and maintainer, this is now subsumed by Martin Paljak's Global Platform Pro,
• Java Card Firewall Tester – developed in the context of the PinPas Java Card project,
• Files accompanying the Fully Verified Java Card API Reference Implementation paper: Java sources and KeY specifications, KeY proofs, Old KeY version used for the proofs, and Java sources and alternative KeY specifications with stronger invariants (not proved). Note: this work has been done with the previous generation of KeY, the files will not even load with the current development version of KeY,
• The Mobius Demonstrator Case Study verified with ESC/Java2 described in Midlet Navigation Graphs in JML (Technical Report),
• Java Card API JML Specifications that can be used with ESC/Java2 (not really thoroughly tested and not reviewed for a very long time).