Difference between revisions of "Wojciech Mostowski"
From CERES
Line 42: | Line 42: | ||
== Publications == | == Publications == | ||
− | * [[Wojciech Mostowski's Publications | Publication List]] | + | * [[Wojciech Mostowski's Publications | Publication List]], |
− | * [https://scholar.google.com/citations?user=dmYvWaAAAAAJ Google Scholar] | + | * [https://scholar.google.com/citations?user=dmYvWaAAAAAJ Google Scholar], |
− | * [http://www.key-project.org/thebook/ KeY Book] | + | * [http://www.key-project.org/thebook/ KeY Book]. |
== (Past) Projects, Events, Program Committees == | == (Past) Projects, Events, Program Committees == | ||
− | * PC member [http://www.cyphy.org/ Fifth Workshop on Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy'15)] | + | * PC member [http://www.cyphy.org/ Fifth Workshop on Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy'15)], |
− | * PC member [http://www.ieee-iri.org/ IEEE International Workshop on Formal Methods Integration (FMi) 2015] | + | * PC member [http://www.ieee-iri.org/ IEEE International Workshop on Formal Methods Integration (FMi) 2015], |
− | * Scientific organiser of the [http://www.lorentzcenter.nl/ Lorentz Center] workshop on [http://www.lorentzcenter.nl/lc/web/2015/677/info.php3?wsid=677&venue=Snellius JML: Advancing Specification Language Methodologies] | + | * Scientific organiser of the [http://www.lorentzcenter.nl/ Lorentz Center] workshop on [http://www.lorentzcenter.nl/lc/web/2015/677/info.php3?wsid=677&venue=Snellius JML: Advancing Specification Language Methodologies], |
− | * Local organiser and publicity chair of the [http://www.utwente.nl/avocs2014/ AVoCS 2014] workshop | + | * Local organiser and publicity chair of the [http://www.utwente.nl/avocs2014/ AVoCS 2014] workshop, |
− | * Participation in the [http://fm2012.verifythis.org/ VerifyThis 2012 Verification Competition] at [http://fm2012.cnam.fr/ FM 2012], team [http://www.key-project.org/ KeY] formed with [http://formal.iti.kit.edu/~bruns/ Daniel Bruns] | + | * Participation in the [http://fm2012.verifythis.org/ VerifyThis 2012 Verification Competition] at [http://fm2012.cnam.fr/ FM 2012], team [http://www.key-project.org/ KeY] formed with [http://formal.iti.kit.edu/~bruns/ Daniel Bruns], |
− | * [http://www.resourceanalysis.cs.ru.nl/jmlworkshop/ CHARTER JML Workshop] | + | * [http://www.resourceanalysis.cs.ru.nl/jmlworkshop/ CHARTER JML Workshop], |
− | * Participation in the [http://foveoos2011.cost-ic0701.org/verification-competition FoVeOOS 2011 Verification Competition], team [http://www.key-project.org/ KeY] formed with Christoph Scheben | + | * Participation in the [http://foveoos2011.cost-ic0701.org/verification-competition FoVeOOS 2011 Verification Competition], team [http://www.key-project.org/ KeY] formed with Christoph Scheben, |
− | * Organizer of the [http://www.key-project.org/keysymposium11/ 10th KeY Symposium] | + | * Organizer of the [http://www.key-project.org/keysymposium11/ 10th KeY Symposium], |
− | * PC member [http://foveoos2011.cost-ic0701.org/ Formal Verification of Object-Oriented Software (FoVeOOS) 2011] | + | * PC member [http://foveoos2011.cost-ic0701.org/ Formal Verification of Object-Oriented Software (FoVeOOS) 2011], |
− | * [http://www.cost-ic0701.org/meetings/7th-mc-and-wg-meeting-limerick-ireland-june-20-22-2011 COST Action Training School 2011] tutorial on [http://limerick.cost-ic0701.org/home/verifying-java-card-programs-with-key Formal Verification of Java Card programs] | + | * [http://www.cost-ic0701.org/meetings/7th-mc-and-wg-meeting-limerick-ireland-june-20-22-2011 COST Action Training School 2011] tutorial on [http://limerick.cost-ic0701.org/home/verifying-java-card-programs-with-key Formal Verification of Java Card programs], |
− | * PC member [http://www.cs.williams.edu/FTfJP2011/index.html Formal Techniques for Java-like Programs (FTfJP) 2011] | + | * PC member [http://www.cs.williams.edu/FTfJP2011/index.html Formal Techniques for Java-like Programs (FTfJP) 2011], |
− | * For [http://frontex.europa.eu/ Frontex], in cooperation with [http://www.pwc.nl/nl PwC] and [https://www.collistesttools.com/home Collis] we performed an EU-wide study of electronic (biometric) passports | + | * For [http://frontex.europa.eu/ Frontex], in cooperation with [http://www.pwc.nl/nl PwC] and [https://www.collistesttools.com/home Collis] we performed an EU-wide study of electronic (biometric) passports, |
− | * '''Best Paper Award''' at [http://sbmf2010.dimap.ufrn.br/ 13th Brazilian Symposium on Formal Methods (SBMF 2010)] | + | * '''Best Paper Award''' at [http://sbmf2010.dimap.ufrn.br/ 13th Brazilian Symposium on Formal Methods (SBMF 2010)], |
− | * PC member [http://foveoos2010.cost-ic0701.org/ Formal Verification of Object-Oriented Software (FoVeOOS) 2010] | + | * PC member [http://foveoos2010.cost-ic0701.org/ Formal Verification of Object-Oriented Software (FoVeOOS) 2010], |
− | * PC member [http://cardis2010.xlim.fr/index.html Smart Card Research and Advanced Applications (CARDIS) 2010] | + | * PC member [http://cardis2010.xlim.fr/index.html Smart Card Research and Advanced Applications (CARDIS) 2010], |
− | * [https://ovchip.cs.ru.nl/Main_Page OV Chip 2.0] is concerned with developing state-of-the-art privacy-friendly protocols for e-Transport/e-Ticketing and e-Identity | + | * [https://ovchip.cs.ru.nl/Main_Page OV Chip 2.0] is concerned with developing state-of-the-art privacy-friendly protocols for e-Transport/e-Ticketing and e-Identity, |
− | * [http://charterproject.ning.com/ 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. [http://www.rtsj.org/ Real-time Java] plays a major role in this effort | + | * [http://charterproject.ning.com/ 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. [http://www.rtsj.org/ Real-time Java] plays a major role in this effort, |
− | * [http://www.cost-ic0701.org/ COST action IC0701]: Formal Verification of Object-Oriented Software. | + | * [http://www.cost-ic0701.org/ COST action IC0701]: Formal Verification of Object-Oriented Software., |
− | * PC member [http://cs.nju.edu.cn/boyland/ftjp/index.html Formal Techniques for Java-like Programs (FTfJP) 2007] | + | * PC member [http://cs.nju.edu.cn/boyland/ftjp/index.html Formal Techniques for Java-like Programs (FTfJP) 2007], |
− | * Mobius – Enabling proof-carrying code for Java on mobile devices | + | * Mobius – Enabling proof-carrying code for Java on mobile devices, |
− | * [http://www.esf.org/ European Science Foundation] Workshop on ''Challenges in Java Program Verification'' | + | * [http://www.esf.org/ European Science Foundation] Workshop on ''Challenges in Java Program Verification'', |
− | * [http://www.win.tue.nl/pinpasjc/ PinPas Java Card] – Side-Channel Analysis of Java Card | + | * [http://www.win.tue.nl/pinpasjc/ PinPas Java Card] – Side-Channel Analysis of Java Card, |
− | * [http://www.key-project.org/ KeY Project] - Integrating Object-Oriented Design with Deductive Verification | + | * [http://www.key-project.org/ KeY Project] - Integrating Object-Oriented Design with Deductive Verification. |
== Software == | == Software == | ||
− | * [http://www.key-project.org/download/ The KeY System] – long time developer, contributor, and maintainer | + | * [http://www.key-project.org/download/ The KeY System] – long time developer, contributor, and maintainer, |
− | * [http://jmrtd.org Java Machine Readable Travel Documents (JMRTD)] – contributor | + | * [http://jmrtd.org Java Machine Readable Travel Documents (JMRTD)] – contributor, |
− | * [http://scuba.sourceforge.net/ Smart Card Utilities for Better Access] – contributor | + | * [http://scuba.sourceforge.net/ Smart Card Utilities for Better Access] – contributor, |
− | * [http://isodl.sourceforge.net/ Electronic Driving License (ISO18013)] – lead developer and maintainer, based on [http://jmrtd.org Java JMRTD] | + | * [http://isodl.sourceforge.net/ Electronic Driving License (ISO18013)] – lead developer and maintainer, based on [http://jmrtd.org Java JMRTD], |
− | * [http://javacardsign.sourceforge.net/ ISO7816 PKI Java Card signing applet] – lead developer and maintainer | + | * [http://javacardsign.sourceforge.net/ ISO7816 PKI Java Card signing applet] – lead developer and maintainer, |
− | * [http://gpj.sourceforge.net/ Global Platform for Java SmartCardIO] – lead developer and maintainer, this is now subsumed by | + | * [http://gpj.sourceforge.net/ Global Platform for Java SmartCardIO] – lead developer and maintainer, this is now subsumed by Martin Paljak's [https://github.com/martinpaljak/GlobalPlatformPro Global Platform Pro], |
− | Martin Paljak's [https://github.com/martinpaljak/GlobalPlatformPro Global Platform Pro] | + | * [http://www.sos.cs.ru.nl/applications/smartcards/firewalltester/ Java Card Firewall Tester] – developed in the context of the [http://www.win.tue.nl/pinpasjc/ PinPas Java Card] project, |
− | * [http://www.sos.cs.ru.nl/applications/smartcards/firewalltester/ Java Card Firewall Tester] – developed in the context of the [http://www.win.tue.nl/pinpasjc/ PinPas Java Card] project | + | * [[Wojciech Mostowski's Old Software | Older and/or obsolete projects]]. |
− | * [[Wojciech Mostowski's Old Software | Older and/or obsolete projects]] | + | |
== Current Teaching == | == Current Teaching == |
Revision as of 14:06, 4 June 2015
Contents
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
(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
- 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,
- Older and/or obsolete projects.