Difference between revisions of "Wojciech Mostowski"
From CERES
| (12 intermediate revisions by one user not shown) | |||
| Line 4: | Line 4: | ||
|Title=Ph.D. | |Title=Ph.D. | ||
|Phone=+46-35-16-7137 | |Phone=+46-35-16-7137 | ||
| − | |Position= | + | |Position=Associate Professor |
|Email=Wojciech.Mostowski@hh.se | |Email=Wojciech.Mostowski@hh.se | ||
|Image=Wojciech Mostowski photo.jpg | |Image=Wojciech Mostowski photo.jpg | ||
|Office=F 309 | |Office=F 309 | ||
| − | |Affiliation= | + | |Affiliation=Computing and Electronics for Real-time Embedded Systems |
|url=http://ceres.hh.se/mediawiki/Wojciech_Mostowski | |url=http://ceres.hh.se/mediawiki/Wojciech_Mostowski | ||
}} | }} | ||
| Line 30: | Line 30: | ||
== Research Interests == | == Research Interests == | ||
| + | * Software reliability, | ||
* Formal verification of object oriented software, in particular [https://java.com/ Java], with the emphasis on practice, | * Formal verification of object oriented software, in particular [https://java.com/ Java], with the emphasis on practice, | ||
* Security and implementation of smart card applications and products, | * Security and implementation of smart card applications and products, | ||
| Line 38: | Line 39: | ||
I currently work on: | I currently work on: | ||
| − | * [ | + | * [https://hh.se/safesmart SafeSmart] |
== Publications == | == Publications == | ||
| Line 49: | Line 50: | ||
== (Past) Projects, Events, Program Committees == | == (Past) Projects, Events, Program Committees == | ||
| + | * Sub-group supervisor and mentor of the Halmstad Team taking part in [https://cps-vo.org/group/CPSchallenge CPS Challenge] on autonomous drones. '''<span style="color:red">Halmstad Team took the second position in the on-site competition:</span>''' | ||
| + | ** [https://hh.se/omhogskolan/aktuellt/nyheter/nyheter/ingenjorsstudentertvaaiinternationelldronartavling.65447156.html Halmstad University article] | ||
| + | ** [https://www.youtube.com/watch?v=TixoMWhiHNk YouTube] | ||
| + | ** [https://cps-vo.org/node/51014 Organiser's Summary] | ||
| + | * Organiser of the [http://www.pm.inf.ethz.ch/verifythis.html VerifyThis2017 verification competition] at [http://www.etaps.org/index.php/2017 ETAPS 2017] | ||
| + | * Leader for the Halmstad University team taking part in [http://gcdc.net/en/ Grand Cooperative Driving Challenge (GCDC) 2016]. '''<span style="color:red">Halmstad Team has won the competition! See the following news and media coverage:</span>''' | ||
| + | ** [https://www.youtube.com/watch?v=MK-tA_C9kdk YouTube], and [https://www.youtube.com/watch?v=rKvb6Dmy7sY our promotion clip]! | ||
| + | ** [http://www.hh.se/english/news/news/goldfortheuniversityininternationalcompetitionwithselfdrivingcars.65445577.html Halmstad University] | ||
| + | ** [http://gcdc.net/en/ GCDC Website] | ||
| + | ** [http://www.svt.se/nyheter/lokalt/halland/studenternas-robotbil-vann-tavling SVT] | ||
| + | ** [http://www.motormagasinet.se/alla/guld-for-hogskolan-i-halmstad-i-tavling-med-sjalvkorande-bilar-2/ Motormagasinet] | ||
| + | ** [https://www.tassinternational.com/news/prescan-software-driven-team-halmstad-university-wins-grand-cooperative-driving-challenge-2016 TASS International 1], [https://www.tassinternational.com/news/gcdc-winning-team-halmstad-university-acclaims-its-use-prescan-software-testing-automated TASS International 2] | ||
| + | ** [http://nyhetsbrev.viktoria.se/nyhetsbrev-363-julfunderingar/ RI.SE Viktoria newsletter] | ||
| + | * PC member [http://acsd2016.mat.umk.pl/ 16th International Conference on Application of Concurrency to System Design (ACSD 2016)], | ||
| + | * Workshop co-chair [http://en.ru.is/ifm/ 12th International Conference on integrated Formal Methods (iFM 2016)], | ||
* 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], | ||
| Line 75: | Line 91: | ||
== Software and Other Code== | == Software and Other Code== | ||
| − | * PVS files accompanying the [[Wojciech Mostowski's Publications#permpaper | ''A Symbolic Approach to Permission Accounting for Concurrent Reasoning | + | * PVS files accompanying the [[Wojciech Mostowski's Publications#permpaper | ''A Symbolic Approach to Permission Accounting for Concurrent Reasoning'']] paper: [[media:Permissions_PVS.zip | Permissions_PVS.zip]]. All other examples mentioned in the paper are now part of the development version of the [http://www.key-project.org/download/ The KeY System], |
* [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, | ||
Latest revision as of 14:38, 7 May 2020
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
- Software reliability,
- 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:
Publications
- Publication List,
- Google Scholar,
- Research Gate (not yet up-to-date),
- KeY Book.
(Past) Projects, Events, Program Committees
- Sub-group supervisor and mentor of the Halmstad Team taking part in CPS Challenge on autonomous drones. Halmstad Team took the second position in the on-site competition:
- Organiser of the VerifyThis2017 verification competition at ETAPS 2017
- Leader for the Halmstad University team taking part in Grand Cooperative Driving Challenge (GCDC) 2016. Halmstad Team has won the competition! See the following news and media coverage:
- PC member 16th International Conference on Application of Concurrency to System Design (ACSD 2016),
- Workshop co-chair 12th International Conference on integrated Formal Methods (iFM 2016),
- 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).
