Difference between revisions of "Wojciech Mostowski"
From CERES
| (32 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 == | ||
| − | * Formal verification of object oriented software, in particular Java, with the emphasis on practice, | + | * Software reliability, |
| + | * 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, | ||
* Embedded systems for automotive applications. | * Embedded systems for automotive applications. | ||
| Line 38: | Line 39: | ||
I currently work on: | I currently work on: | ||
| − | * [ | + | * [https://hh.se/safesmart SafeSmart] |
== 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], |
| + | * [https://www.researchgate.net/profile/Wojciech_Mostowski Research Gate] (not yet up-to-date), | ||
| + | * [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)] | + | * 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>''' |
| − | * PC member [http://www.ieee-iri.org/ IEEE International Workshop on Formal Methods Integration (FMi) 2015] | + | ** [https://hh.se/omhogskolan/aktuellt/nyheter/nyheter/ingenjorsstudentertvaaiinternationelldronartavling.65447156.html Halmstad University article] |
| − | * 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] | + | ** [https://www.youtube.com/watch?v=TixoMWhiHNk YouTube] |
| − | * Local organiser and publicity chair of the [http://www.utwente.nl/avocs2014/ AVoCS 2014] workshop | + | ** [https://cps-vo.org/node/51014 Organiser's Summary] |
| − | * 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] | + | * Organiser of the [http://www.pm.inf.ethz.ch/verifythis.html VerifyThis2017 verification competition] at [http://www.etaps.org/index.php/2017 ETAPS 2017] |
| − | * [http://www.resourceanalysis.cs.ru.nl/jmlworkshop/ CHARTER JML Workshop] | + | * 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>''' |
| − | * 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 | + | ** [https://www.youtube.com/watch?v=MK-tA_C9kdk YouTube], and [https://www.youtube.com/watch?v=rKvb6Dmy7sY our promotion clip]! |
| − | * Organizer of the [http://www.key-project.org/keysymposium11/ 10th KeY Symposium] | + | ** [http://www.hh.se/english/news/news/goldfortheuniversityininternationalcompetitionwithselfdrivingcars.65445577.html Halmstad University] |
| − | * PC member [http://foveoos2011.cost-ic0701.org/ Formal Verification of Object-Oriented Software (FoVeOOS) 2011] | + | ** [http://gcdc.net/en/ GCDC Website] |
| − | * [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.svt.se/nyheter/lokalt/halland/studenternas-robotbil-vann-tavling SVT] |
| − | * PC member [http://www.cs.williams.edu/FTfJP2011/index.html Formal Techniques for Java-like Programs (FTfJP) 2011] | + | ** [http://www.motormagasinet.se/alla/guld-for-hogskolan-i-halmstad-i-tavling-med-sjalvkorande-bilar-2/ Motormagasinet] |
| − | * 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 | + | ** [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] |
| − | * '''Best Paper Award''' at [http://sbmf2010.dimap.ufrn.br/ 13th Brazilian Symposium on Formal Methods (SBMF 2010)] | + | ** [http://nyhetsbrev.viktoria.se/nyhetsbrev-363-julfunderingar/ RI.SE Viktoria newsletter] |
| − | * PC member [http://foveoos2010.cost-ic0701.org/ Formal Verification of Object-Oriented Software (FoVeOOS) 2010] | + | * PC member [http://acsd2016.mat.umk.pl/ 16th International Conference on Application of Concurrency to System Design (ACSD 2016)], |
| − | * PC member [http://cardis2010.xlim.fr/index.html Smart Card Research and Advanced Applications (CARDIS) 2010] | + | * Workshop co-chair [http://en.ru.is/ifm/ 12th International Conference on integrated Formal Methods (iFM 2016)], |
| − | * [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 | + | * PC member [http://www.cyphy.org/ Fifth Workshop on Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy'15)], |
| − | * [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 | + | * PC member [http://www.ieee-iri.org/ IEEE International Workshop on Formal Methods Integration (FMi) 2015], |
| − | * [http://www.cost-ic0701.org/ COST action IC0701]: Formal Verification of Object-Oriented Software. | + | * 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], |
| − | * PC member [http://cs.nju.edu.cn/boyland/ftjp/index.html Formal Techniques for Java-like Programs (FTfJP) 2007] | + | * Local organiser and publicity chair of the [http://www.utwente.nl/avocs2014/ AVoCS 2014] workshop, |
| − | * Mobius – Enabling proof-carrying code for Java on mobile devices | + | * 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.esf.org/ European Science Foundation] Workshop on ''Challenges in Java Program Verification'' | + | * [http://www.resourceanalysis.cs.ru.nl/jmlworkshop/ CHARTER JML Workshop], |
| − | * [http://www.win.tue.nl/pinpasjc/ PinPas Java Card] – Side-Channel Analysis of Java Card | + | * 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, |
| − | * [http://www.key-project.org/ KeY Project] - Integrating Object-Oriented Design with Deductive Verification | + | * 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], | ||
| + | * [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], | ||
| + | * 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)], | ||
| + | * 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], | ||
| + | * [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://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], | ||
| + | * 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.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. | ||
| − | == Teaching == | + | == Software and Other Code== |
| + | |||
| + | * 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://jmrtd.org Java Machine Readable Travel Documents (JMRTD)] – 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://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 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, | ||
| + | * Files accompanying the [[Wojciech Mostowski's Publications#apipaper | ''Fully Verified Java Card API Reference Implementation'']] paper: [[media:javacardapi-20070821.zip | Java sources and KeY specifications]], [[media:proofs-20070821.zip | KeY proofs]], [[media:key-0.2610-source.zip | Old KeY version used for the proofs]], and [[media:javacardapi-20070821-allinv.zip | 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, | ||
| + | * [[media:DemonstratorCaseStudyJML.zip |The Mobius Demonstrator Case Study]] verified with [http://kindsoftware.com/products/opensource/ESCJava2/ ESC/Java2] described in [[Wojciech Mostowski's Publications#midlets-paper|''Midlet Navigation Graphs in JML'']] ([[Wojciech Mostowski's Publications#midlets-tr|Technical Report]]), | ||
| + | * [[media:javacardapi_esc-0.9e.zip|Java Card API JML Specifications]] that can be used with [http://kindsoftware.com/products/opensource/ESCJava2/ ESC/Java2] (not really thoroughly tested and not reviewed for a very long time). | ||
| + | |||
| + | == Current Teaching == | ||
== Convenience Links == | == Convenience Links == | ||
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).
