Difference between revisions of "Wojciech Mostowski's BibTeX Entries"

From CERES
Jump to: navigation, search
 
(23 intermediate revisions by one user not shown)
Line 1: Line 1:
 +
<div id="Mostowski2022b"><pre>
 +
@Inbook{Mostowski2022b,
 +
  title =        {Implications of Deductive Verification on Research Quality},
 +
  author =      {Wojciech Mostowski},
 +
  editor =      {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Einar Broch Johnsen},
 +
  booktitle =    {The Logic of Software. A Tasting Menu of Formal Methods},
 +
  year =        2022,
 +
  publisher =    {Springer International Publishing},
 +
  pages =        {370--381},
 +
  series =      {LNCS},
 +
  volume =      {13360},
 +
  doi =          {10.1007/978-3-031-08166-8_17}
 +
}
 +
</pre></div>
 +
 +
<div id="Mostowski2022"><pre>
 +
@Inbook{Mostowski2022,
 +
  title =        {Locality-Based Test Selection for Autonomous Agents},
 +
  author =      {Sina Entekhabi and Wojciech Mostowski and Mohammad Reza Mousavi},
 +
  editor =      {David Clark and Hector Menendez and Ana Rosa Cavalli},
 +
  booktitle =    {ICTSS 2021: Testing Software and Systems},
 +
  year =        2022,
 +
  publisher =    {Springer International Publishing},
 +
  pages =        {73--89},
 +
  series =      {LNCS},
 +
  volume =      {13045},
 +
  doi =          {10.1007/978-3-031-04673-5_6}
 +
}
 +
</pre></div>
 +
 +
<div id="Mostowski2021"><pre>
 +
@InProceedings{Mostowski2021,
 +
  title =        {The CAR Approach: Creative Applied Research Experiences for Master’s Students in Autonomous Platooning},
 +
  author =      {Galina Sidorenko and Wojciech Mostowski and Alexey Vinel and Jeanette Sj\"{o}berg and Martin Cooney},
 +
  booktitle =    {2021 30th IEEE International Conference on Robot \& Human Interactive Communication (RO-MAN)},
 +
  year =        2021,
 +
  month =        {August},
 +
  pages =        {214--221},
 +
  doi =          {10.1109/RO-MAN50785.2021.9515560},
 +
  publisher =    {IEEE}
 +
}
 +
</pre></div>
 +
 +
<div id="Mostowski2020"><pre>
 +
@Inbook{Mostowski2020,
 +
  title =        {From Explicit to Implicit Dynamic Frames in Concurrent Reasoning for Java},
 +
  author =      {Mostowski, Wojciech},
 +
  editor =      {Ahrendt, Wolfgang and Beckert, Bernhard and Bubel, Richard and H{\"a}hnle, Reiner and Ulbrich, Mattias},
 +
  booktitle =    {Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY},
 +
  year =        2020,
 +
  publisher =    {Springer International Publishing},
 +
  pages =        {177--203},
 +
  series =      {LNCS},
 +
  volume =      {12345},
 +
  doi =          {10.1007/978-3-030-64354-6_7}
 +
}
 +
</pre></div>
 +
 +
<div id="Mostowski2018"><pre>
 +
@Article{Mostowski2018,
 +
  title =        {Model-Based Fault Injection for Testing Gray-Box Systems},
 +
  author =      {Wojciech Mostowski},
 +
  journal =      {Journal of Logical and Algebraic Methods in Programming},
 +
  publisher =    {Elsevier},
 +
  doi =          {10.1016/j.jlamp.2018.10.003},
 +
  year =        2019,
 +
  volume =      103,
 +
  pages =        {31--45}
 +
}
 +
</pre></div>
 +
 +
<div id="HalmstadGCDC2016"><pre>
 +
@Article{HalmstadGCDC2016,
 +
  title =        {Team {Halmstad} Approach to Cooperative Driving in the {Grand Cooperative Driving Challenge} 2016},
 +
  author =      {Maytheewat Aramrattana and J{\'e}r{\^o}me Detournay and Cristofer Englund and Viktor Frimodig and
 +
                  Oscar Uddman Jansson and Tony Larsson and Wojciech Mostowski and V{\'\i}ctor D{\'\i}ez Rodr{\'\i}guez and
 +
                  Thomas Rosenstatter and Golam Shahanoor},
 +
  journal =      {Transactions on Intelligent Transportation Systems, Special Issue on GCDC},
 +
  publisher =    {IEEE},
 +
  volume =      19,
 +
  issue =        4,
 +
  doi =          {10.1109/TITS.2017.2752359},
 +
  year =        2017
 +
}
 +
</pre></div>
 +
 +
<div id="MostowskiUlbrich2016"><pre>
 +
@InBook{MostowskiUlbrich2016,
 +
  author =      {Wojciech Mostowski and Mattias Ulbrich},
 +
  title =        {Dynamic Dispatch for Method Contracts through Abstract Predicates},
 +
  booktitle =    {Transactions on Modularity and Composition I},
 +
  editor =      {Shigeru Chiba and Mario S{\"u}dholt and Patrick Eugster and Lukasz Ziarek and Gary T. Leavens},
 +
  year =        2016,
 +
  pages =        {238--267},
 +
  doi =          {10.1007/978-3-319-46969-0_7},
 +
  publisher =    {Springer International Publishing}
 +
}
 +
</pre></div>
 +
 
<div id="Mostowski-VerifyThis2012"><pre>
 
<div id="Mostowski-VerifyThis2012"><pre>
 
@Article{Mostowski-VerifyThis2012,
 
@Article{Mostowski-VerifyThis2012,
Line 9: Line 108:
 
   issue =        {6},
 
   issue =        {6},
 
   pages =        {729--744},
 
   pages =        {729--744},
 +
  doi =          {10.1007/s10009-013-0293-y},
 
   publisher =    {Springer}
 
   publisher =    {Springer}
 
}
 
}
Line 24: Line 124:
 
   year =        2005,
 
   year =        2005,
 
   month =        {February},
 
   month =        {February},
 +
  doi =          {10.1007/s10270-004-0058-x},
 
   publisher =    {Springer}
 
   publisher =    {Springer}
 +
}
 +
</pre></div>
 +
 +
<div id="Mostowski2019VerifyThis"><pre>
 +
@InProceedings{Mostowski2019VerifyThis,
 +
  title =        {{VerifyThis} -- {Verification} Competition with a Human Factor},
 +
  author =      {Gidon Ernst and Marieke Huisman and Wojciech Mostowski and Mattias Ulbrich},
 +
  editor =      {Dirk Beyer and Marieke Huisman and Fabrice Kordon and Bernhard Steffen},
 +
  booktitle =    {Tools and Algorithms for the Construction and Analysis of Systems, Part III, 25 Years of TACAS: TOOLympics},
 +
  year =        2019,
 +
  publisher =    {Springer, Cham},
 +
  series =      {LNCS},
 +
  volume =      {11429},
 +
  pages =        {176--195},
 +
  doi =          {10.1007/978-3-030-17502-3_12}
 +
}
 +
</pre></div>
 +
 +
<div id="AichernigMostowskiMousaviTapplerTaromirad2018"><pre>
 +
@InProceedings{AichernigMostowskiMousaviTapplerTaromirad2018,
 +
  title =        {Model Learning and Model-Based Testing},
 +
  author =      {Bernhard K. Aichernig and Wojciech Mostowski and Mohammad Reza Mousavi and Martin Tappler and Masoumeh Taromirad},
 +
  editor =      {Amel Bennaceur and Reiner H{\"a}hnle and Karl Meinke},
 +
  booktitle =    {Machine Learning for Dynamic Software Analysis: Potentials and Limits: International Dagstuhl Seminar 16172, Dagstuhl Castle, Germany, April 24--27, 2016, Revised Papers},
 +
  year =        2018,
 +
  publisher =    {Springer International Publishing},
 +
  series =      {LNCS},
 +
  volume =      {11026},
 +
  pages =        {74--100},
 +
  doi =          {10.1007/978-3-319-96562-8_3}
 +
}
 +
</pre></div>
 +
 +
<div id="MostowskiArtsHughes2017"><pre>
 +
@InProceedings{MostowskiArtsHughes2017,
 +
  title =        {Modelling of {Autosar} Libraries for Large Scale Testing},
 +
  author =      {Wojciech Mostowski and Thomas Arts and John Hughes},
 +
  booktitle =    {2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017)},
 +
  editor=        {Holger Hermanns and Peter H\"ofner},
 +
  year =        2017,
 +
  month =        {April},
 +
  pages =        {184--199},
 +
  series =      {Electronic Proceedings in Theoretical Computer Science},
 +
  volume =      {244},
 +
  doi =          {10.4204/EPTCS.244.7},
 +
  publisher =    {Open Publishing Association}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 33: Line 180:
 
   author =      {Sebastian Kunze and Wojciech Mostowski and Mohammad Reza Mousavi and Mahsa Varshosaz},  
 
   author =      {Sebastian Kunze and Wojciech Mostowski and Mohammad Reza Mousavi and Mahsa Varshosaz},  
 
   booktitle =    {Workshop on Automotive Systems/Software Architectures (WASA'16)},  
 
   booktitle =    {Workshop on Automotive Systems/Software Architectures (WASA'16)},  
   year =        {2016},  
+
   year =        2016,  
 
   month =        {April},
 
   month =        {April},
 
   pages =        {22--25},  
 
   pages =        {22--25},  
Line 51: Line 198:
 
   publisher =    {Springer},
 
   publisher =    {Springer},
 
   volume =      {9593},
 
   volume =      {9593},
 +
  doi =          {10.1007/978-3-319-29613-5_8},
 
   pages =        {124--141}
 
   pages =        {124--141}
 
}
 
}
Line 91: Line 239:
 
   volume =      {8471},
 
   volume =      {8471},
 
   year =        2014,
 
   year =        2014,
 +
  doi =          {10.1007/978-3-319-12154-3_4},
 
   publisher =    {Springer}
 
   publisher =    {Springer}
 
}
 
}
Line 105: Line 254:
 
   series =      {LNCS},
 
   series =      {LNCS},
 
   volume =      {8483},
 
   volume =      {8483},
 +
  doi =          {10.1007/978-3-319-07317-0_5},
 
   publisher =    {Springer},
 
   publisher =    {Springer},
 
}
 
}
Line 132: Line 282:
 
   publisher =    {Springer},
 
   publisher =    {Springer},
 
   series =      {LNCS},
 
   series =      {LNCS},
 +
  doi =          {10.1007/978-3-642-38592-6_3},
 
   volume =      {7892}
 
   volume =      {7892}
 
}
 
}
Line 143: Line 294:
 
   year =        2012,
 
   year =        2012,
 
   publisher =    {ACM},
 
   publisher =    {ACM},
   doi =          {10.1145/2388936.2388960}
+
   doi =          {10.1145/2388936.2388960},
 
   pages =        {145--154}
 
   pages =        {145--154}
 
}
 
}
Line 161: Line 312:
 
   pages =        {3--21},
 
   pages =        {3--21},
 
   publisher =    {Springer},
 
   publisher =    {Springer},
 +
  doi =          {10.1007/978-3-642-31762-0_2},
 
   year =        2012
 
   year =        2012
 
}
 
}
Line 175: Line 327:
 
   publisher =    {Springer},
 
   publisher =    {Springer},
 
   series =      {LNICST},
 
   series =      {LNICST},
 +
  doi =          {10.1007/978-3-642-31909-9_14},
 
   volume =      {96},
 
   volume =      {96},
 
   year =        2012
 
   year =        2012
Line 190: Line 343:
 
   pages =        {17--32},
 
   pages =        {17--32},
 
   series =      {LNCS},
 
   series =      {LNCS},
 +
  doi =          {10.1007/978-3-642-19829-8_2},
 
   volume =      {6527},
 
   volume =      {6527},
 
   publisher =    {Springer}
 
   publisher =    {Springer}
Line 200: Line 354:
 
   title =        {Developing Efficient Blinded Attribute Certificates on Smart Cards via Pairings},
 
   title =        {Developing Efficient Blinded Attribute Certificates on Smart Cards via Pairings},
 
   booktitle =    {Smart Card Research and Advanced Application Conference CARDIS 2010, Proceedings, Passau, Germany},
 
   booktitle =    {Smart Card Research and Advanced Application Conference CARDIS 2010, Proceedings, Passau, Germany},
 +
  editor =      {Dieter Gollmann and Jean-Louis Lanet and Julien Iguchi-Cartigny},
 
   year =        2010,
 
   year =        2010,
 
   series =      {LNCS},
 
   series =      {LNCS},
 +
  doi =          {10.1007/978-3-642-12510-2_15},
 
   volume =      {6035},
 
   volume =      {6035},
 
   month =        {April},
 
   month =        {April},
Line 217: Line 373:
 
   address =      {Louvain-la-Neuve, Belgium},
 
   address =      {Louvain-la-Neuve, Belgium},
 
   month =        {November},
 
   month =        {November},
 +
  url =          {http://ceres.hh.se/mediawiki/images/5/5d/Mostowski_wissec2009.pdf},
 
   note =        {Available on-line}
 
   note =        {Available on-line}
 
}
 
}
Line 230: Line 387:
 
   editor =      {Mar\'{i}a Alpuente and Byron Cook and Christophe Joubert},
 
   editor =      {Mar\'{i}a Alpuente and Byron Cook and Christophe Joubert},
 
   series =      {LNCS},
 
   series =      {LNCS},
 +
  doi =          {10.1007/978-3-642-04570-7_19},
 
   pages =        {207--209},
 
   pages =        {207--209},
 
   volume =      {5825},
 
   volume =      {5825},
Line 242: Line 400:
 
   booktitle =    {eSmart 2008, Proceedings},
 
   booktitle =    {eSmart 2008, Proceedings},
 
   year =        {2008},
 
   year =        {2008},
 +
  url =          {http://ceres.hh.se/mediawiki/images/3/36/Mostowski_esmart2008.pdf},
 
   month =        {September}
 
   month =        {September}
 
}
 
}
Line 254: Line 413:
 
   year =        {2008},
 
   year =        {2008},
 
   series =      {LNCS},
 
   series =      {LNCS},
 +
  doi =          {10.1007/978-3-540-85893-5_1},
 
   volume =      5189,
 
   volume =      5189,
 
   month =        {September},
 
   month =        {September},
Line 266: Line 426:
 
   title =        {Fingerprinting Passports},
 
   title =        {Fingerprinting Passports},
 
   booktitle =    {NLUUG 2008 Spring Conference on Security, Proceedings},
 
   booktitle =    {NLUUG 2008 Spring Conference on Security, Proceedings},
 +
  url =          {http://ceres.hh.se/mediawiki/images/3/37/Mostowski_nluug2008.pdf},
 
   month =        {May},
 
   month =        {May},
 
   year =        2008
 
   year =        2008
Line 280: Line 441:
 
   month =        {July},
 
   month =        {July},
 
   volume =      {259},
 
   volume =      {259},
 +
  url =          {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-259/paper12.pdf},
 
   series =      {CEUR WS}
 
   series =      {CEUR WS}
 
}
 
}
Line 290: Line 452:
 
   booktitle =    {Proceedings, e-Smart 2006, Sophia-Antipolis, France, September 20--22},
 
   booktitle =    {Proceedings, e-Smart 2006, Sophia-Antipolis, France, September 20--22},
 
   note =        {Available on-line},
 
   note =        {Available on-line},
 +
  url =          {http://ceres.hh.se/mediawiki/images/8/83/Mostowski_esmart2006.pdf},
 
   year =        2006
 
   year =        2006
 
}
 
}
Line 303: Line 466:
 
   editor =      {Jayadev Misra and Tobias Nipkow and Emil Sekerinski},
 
   editor =      {Jayadev Misra and Tobias Nipkow and Emil Sekerinski},
 
   series =      {LNCS},
 
   series =      {LNCS},
 +
  doi =          {10.1007/11813040_30},
 
   pages =        {444--459},
 
   pages =        {444--459},
 
   volume =      {4085},
 
   volume =      {4085},
Line 319: Line 483:
 
   pages =        {357--371},
 
   pages =        {357--371},
 
   series =      {LNCS},
 
   series =      {LNCS},
 +
  doi =          {10.1007/978-3-540-31984-9_27},
 
   month =        {April},
 
   month =        {April},
 
   publisher =    {Springer}
 
   publisher =    {Springer}
Line 334: Line 499:
 
   year =        2005,
 
   year =        2005,
 
   volume =      {3362},
 
   volume =      {3362},
   series =      {LNCS}
+
   series =      {LNCS},
 +
  doi =          {10.1007/978-3-540-30569-9_8}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 348: Line 514:
 
   volume =      {102C},
 
   volume =      {102C},
 
   series =      {ENTCS},
 
   series =      {ENTCS},
 +
  doi =          {10.1016/j.entcs.2003.09.001},
 
   month =        {November},
 
   month =        {November},
 
   publisher =    {Elsevier}
 
   publisher =    {Elsevier}
Line 363: Line 530:
 
   volume =      {2621},
 
   volume =      {2621},
 
   series =      {LNCS},
 
   series =      {LNCS},
 +
  doi =          {10.1007/3-540-36578-8_18},
 
   month =        {April},
 
   month =        {April},
 
   publisher =    {Springer}
 
   publisher =    {Springer}
Line 379: Line 547:
 
   publisher =    {Springer},
 
   publisher =    {Springer},
 
   series =      {LNCS},
 
   series =      {LNCS},
 +
  doi =          {10.1007/3-540-45923-5_23},
 
   volume =      {2306},
 
   volume =      {2306},
 
   year =        2002
 
   year =        2002
Line 392: Line 561:
 
   month =        {March},
 
   month =        {March},
 
   editor =      {T. Clarke and A. Evans and K. Lano},
 
   editor =      {T. Clarke and A. Evans and K. Lano},
   note =        {Available on-line}
+
   note =        {Available on-line},
 +
  url =          {http://ceres.hh.se/mediawiki/images/f/fb/Mostowski_room2002.ps}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 416: Line 586:
 
   year =        2010,
 
   year =        2010,
 
   note =        {Available on-line}
 
   note =        {Available on-line}
 +
}
 +
</pre></div>
 +
 +
<div id="KeYBook2-Chapter9"><pre>
 +
@InBook{KeYBook2-Chapter9,
 +
  author =      {Daniel Grahl and Richard Bubel and Wojciech Mostowski and Peter H. Schmitt and Mattias Ulbrich and Benjamin Wei{\ss}},
 +
  title =        {Deductive Software Verification -- {The} {\KeY{}} Book},
 +
  subtitle =    {From Theory to Practice},
 +
  editor =      {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"a}hnle and Peter H. Schmitt and Mattias Ulbrich},
 +
  volume =      {10001},
 +
  series =      {LNCS},
 +
  publisher =    {Springer International Publishing},
 +
  year =        {2017},
 +
  chapter =      {Chapter~9. Modular Specification and Verification},
 +
  pages =        {289--351},
 +
  doi =          {10.1007/978-3-319-49812-6_9},
 +
  isbn =        {978-3-319-49811-9}
 +
}
 +
</pre></div>
 +
 +
<div id="KeYBook2-Chapter10"><pre>
 +
@InBook{KeYBook2-Chapter10,
 +
  author =      {Wojciech Mostowski},
 +
  title =        {Deductive Software Verification -- {The} {\KeY{}} Book},
 +
  subtitle =    {From Theory to Practice},
 +
  editor =      {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"a}hnle and Peter H. Schmitt and Mattias Ulbrich},
 +
  volume =      {10001},
 +
  series =      {LNCS},
 +
  publisher =    {Springer International Publishing},
 +
  year =        {2017},
 +
  chapter =      {Chapter~10. Verifying {Java Card} Programs},
 +
  pages =        {353--380},
 +
  doi =          {10.1007/978-3-319-49812-6_10},
 +
  isbn =        {978-3-319-49811-9}
 +
}
 +
</pre></div>
 +
 +
<div id="KeYBook2-AppendixB"><pre>
 +
@InBook{KeYBook2-AppendixB,
 +
  author =      {Wojciech Mostowski and Richard Bubel},
 +
  title =        {Deductive Software Verification -- {The} {\KeY{}} Book},
 +
  subtitle =    {From Theory to Practice},
 +
  editor =      {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"a}hnle and Peter H. Schmitt and Mattias Ulbrich},
 +
  volume =      {10001},
 +
  series =      {LNCS},
 +
  publisher =    {Springer International Publishing},
 +
  year =        {2017},
 +
  chapter =      {Appendix~B. {KeY} File Reference},
 +
  pages =        {631--665},
 +
  isbn =        {978-3-319-49811-9}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 429: Line 649:
 
   volume =      4334,
 
   volume =      4334,
 
   year =        2007,
 
   year =        2007,
 +
  doi =          {10.1007/978-3-540-69061-0_9},
 
   pages =        {375--405}
 
   pages =        {375--405}
 
}
 
}
Line 443: Line 664:
 
   volume =      4334,
 
   volume =      4334,
 
   year =        2007,
 
   year =        2007,
 +
  doi =          {10.1007/978-3-540-69061-0_14},
 
   pages =        {533--568}
 
   pages =        {533--568}
 
}
 
}
Line 493: Line 715:
 
   number =      {16L},
 
   number =      {16L},
 
   month =        {December}
 
   month =        {December}
 +
}
 +
</pre></div>
 +
 +
<div id="VerifyThis2017-TR"><pre>
 +
@TechReport{VerifyThis2017-TR,
 +
  author =      {Marieke Huisman and Rosemary Monahan and Wojciech Mostowski and Peter M{\"u}ller and Mattias Ulbrich},
 +
  title =        {{VerifyThis 2017}: A Program Verification Competition},
 +
  institution =  {Karlsruhe Institute of Technology},
 +
  series =      {Karlsruhe Reports in Informatics},
 +
  doi =          {10.5445/ir/1000077160},
 +
  url =          {https://publikationen.bibliothek.kit.edu/1000077160},
 +
  year =        2017,
 +
  number =      {2017-10}
 
}
 
}
 
</pre></div>
 
</pre></div>

Latest revision as of 10:56, 11 August 2022

@Inbook{Mostowski2022b,
  title =        {Implications of Deductive Verification on Research Quality},
  author =       {Wojciech Mostowski},
  editor =       {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Einar Broch Johnsen},
  booktitle =    {The Logic of Software. A Tasting Menu of Formal Methods},
  year =         2022,
  publisher =    {Springer International Publishing},
  pages =        {370--381},
  series =       {LNCS},
  volume =       {13360},
  doi =          {10.1007/978-3-031-08166-8_17}
}
@Inbook{Mostowski2022,
  title =        {Locality-Based Test Selection for Autonomous Agents},
  author =       {Sina Entekhabi and Wojciech Mostowski and Mohammad Reza Mousavi},
  editor =       {David Clark and Hector Menendez and Ana Rosa Cavalli},
  booktitle =    {ICTSS 2021: Testing Software and Systems},
  year =         2022,
  publisher =    {Springer International Publishing},
  pages =        {73--89},
  series =       {LNCS},
  volume =       {13045},
  doi =          {10.1007/978-3-031-04673-5_6}
}
@InProceedings{Mostowski2021, 
  title =        {The CAR Approach: Creative Applied Research Experiences for Master’s Students in Autonomous Platooning}, 
  author =       {Galina Sidorenko and Wojciech Mostowski and Alexey Vinel and Jeanette Sj\"{o}berg and Martin Cooney}, 
  booktitle =    {2021 30th IEEE International Conference on Robot \& Human Interactive Communication (RO-MAN)}, 
  year =         2021, 
  month =        {August},
  pages =        {214--221}, 
  doi =          {10.1109/RO-MAN50785.2021.9515560},
  publisher =    {IEEE}
}
@Inbook{Mostowski2020,
  title =        {From Explicit to Implicit Dynamic Frames in Concurrent Reasoning for Java},
  author =       {Mostowski, Wojciech},
  editor =       {Ahrendt, Wolfgang and Beckert, Bernhard and Bubel, Richard and H{\"a}hnle, Reiner and Ulbrich, Mattias},
  booktitle =    {Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY},
  year =         2020,
  publisher =    {Springer International Publishing},
  pages =        {177--203},
  series =       {LNCS},
  volume =       {12345},
  doi =          {10.1007/978-3-030-64354-6_7}
}
@Article{Mostowski2018,
  title =        {Model-Based Fault Injection for Testing Gray-Box Systems},
  author =       {Wojciech Mostowski},
  journal =      {Journal of Logical and Algebraic Methods in Programming},
  publisher =    {Elsevier},
  doi =          {10.1016/j.jlamp.2018.10.003},
  year =         2019,
  volume =       103,
  pages =        {31--45}
}
@Article{HalmstadGCDC2016,
  title =        {Team {Halmstad} Approach to Cooperative Driving in the {Grand Cooperative Driving Challenge} 2016},
  author =       {Maytheewat Aramrattana and J{\'e}r{\^o}me Detournay and Cristofer Englund and Viktor Frimodig and
                  Oscar Uddman Jansson and Tony Larsson and Wojciech Mostowski and V{\'\i}ctor D{\'\i}ez Rodr{\'\i}guez and
                  Thomas Rosenstatter and Golam Shahanoor},
  journal =      {Transactions on Intelligent Transportation Systems, Special Issue on GCDC},
  publisher =    {IEEE},
  volume =       19,
  issue =        4,
  doi =          {10.1109/TITS.2017.2752359},
  year =         2017
}
@InBook{MostowskiUlbrich2016,
  author =       {Wojciech Mostowski and Mattias Ulbrich},
  title =        {Dynamic Dispatch for Method Contracts through Abstract Predicates},
  booktitle =    {Transactions on Modularity and Composition I},
  editor =       {Shigeru Chiba and Mario S{\"u}dholt and Patrick Eugster and Lukasz Ziarek and Gary T. Leavens},
  year =         2016,
  pages =        {238--267},
  doi =          {10.1007/978-3-319-46969-0_7},
  publisher =    {Springer International Publishing}
}
@Article{Mostowski-VerifyThis2012,
  author =       {Daniel Bruns and Wojciech Mostowski and Mattias Ulbrich},
  title =        {Implementation-level Verification of Algorithms with {KeY}},
  journal =      {International Journal on Software Tools for Technology Transfer},
  year =         2015,
  month =        {November},
  volume =       {17},
  issue =        {6},
  pages =        {729--744},
  doi =          {10.1007/s10009-013-0293-y},
  publisher =    {Springer}
}
@Article{KeYSoSyM2004,
  author =       {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert and Richard Bubel and Martin Giese and Reiner H\"{a}hnle
                  and Wolfram Menzel and Wojciech Mostowski and Andreas Roth and Steffen Schlager and Peter H. Schmitt},
  title =        {The {KeY} Tool},
  journal =      {Software and Systems Modeling},
  volume =       {4},
  number =       {1},
  pages =        {32--54},
  year =         2005,
  month =        {February},
  doi =          {10.1007/s10270-004-0058-x},
  publisher =    {Springer}
}
@InProceedings{Mostowski2019VerifyThis,
  title =        {{VerifyThis} -- {Verification} Competition with a Human Factor},
  author =       {Gidon Ernst and Marieke Huisman and Wojciech Mostowski and Mattias Ulbrich},
  editor =       {Dirk Beyer and Marieke Huisman and Fabrice Kordon and Bernhard Steffen},
  booktitle =    {Tools and Algorithms for the Construction and Analysis of Systems, Part III, 25 Years of TACAS: TOOLympics},
  year =         2019,
  publisher =    {Springer, Cham},
  series =       {LNCS},
  volume =       {11429},
  pages =        {176--195},
  doi =          {10.1007/978-3-030-17502-3_12}
}
@InProceedings{AichernigMostowskiMousaviTapplerTaromirad2018,
  title =        {Model Learning and Model-Based Testing},
  author =       {Bernhard K. Aichernig and Wojciech Mostowski and Mohammad Reza Mousavi and Martin Tappler and Masoumeh Taromirad},
  editor =       {Amel Bennaceur and Reiner H{\"a}hnle and Karl Meinke},
  booktitle =    {Machine Learning for Dynamic Software Analysis: Potentials and Limits: International Dagstuhl Seminar 16172, Dagstuhl Castle, Germany, April 24--27, 2016, Revised Papers},
  year =         2018,
  publisher =    {Springer International Publishing},
  series =       {LNCS},
  volume =       {11026},
  pages =        {74--100},
  doi =          {10.1007/978-3-319-96562-8_3}
}
@InProceedings{MostowskiArtsHughes2017, 
  title =        {Modelling of {Autosar} Libraries for Large Scale Testing}, 
  author =       {Wojciech Mostowski and Thomas Arts and John Hughes}, 
  booktitle =    {2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017)}, 
  editor=        {Holger Hermanns and Peter H\"ofner},
  year =         2017, 
  month =        {April},
  pages =        {184--199}, 
  series =       {Electronic Proceedings in Theoretical Computer Science},
  volume =       {244},
  doi =          {10.4204/EPTCS.244.7},
  publisher =    {Open Publishing Association}
}
@InProceedings{KunzeMostowskiMousaviVarshosaz2016, 
  title =        {Generation of Failure Models through Automata Learning}, 
  author =       {Sebastian Kunze and Wojciech Mostowski and Mohammad Reza Mousavi and Mahsa Varshosaz}, 
  booktitle =    {Workshop on Automotive Systems/Software Architectures (WASA'16)}, 
  year =         2016, 
  month =        {April},
  pages =        {22--25}, 
  doi =          {10.1109/WASA.2016.7},
  publisher =    {IEEE Computer Society}
}
@InProceedings{Mostowski2015,
  title =        {Dynamic Frames Based Verification Method for Concurrent {Java} Programs},
  author =       {Wojciech Mostowski},
  booktitle =    {Verified Software: Theories, Tools, and Experiments (VSTTE'15)},
  editor =       {Arie Gurfinkel and Sanjit A. Seshia},
  year =         2016,
  series =       {LNCS},
  publisher =    {Springer},
  volume =       {9593},
  doi =          {10.1007/978-3-319-29613-5_8},
  pages =        {124--141}
}
@InProceedings{HuismanMostowski2015,
  title =        {A Symbolic Approach to Permission Accounting for Concurrent Reasoning},
  author =       {Marieke Huisman and Wojciech Mostowski},
  year =         2015,
  publisher =    {IEEE Computer Society},
  booktitle =    {14th International Symposium on Parallel and Distributed Computing (ISPDC 2015)},
  doi =          {10.1109/ISPDC.2015.26},
  pages =        {165--174}
}
@InProceedings{MostowskiUlbrich2015,
  author =       {Wojciech Mostowski and Mattias Ulbrich},
  title =        {Dynamic Dispatch for Method Contracts through Abstract Predicates},
  booktitle =    {15th International Conference on MODULARITY (MODULARITY'15)},
  publisher =    {ACM},
  year =         {2015},
  doi =          {10.1145/2724525.2724574},
  pages =        {109--116}
}
@InProceedings{KeY2014,
  title =        {The {KeY} Platform for Verification and Analysis of {Java} Programs},
  author =       {Wolfgang Ahrendt and Bernhard Beckert and Daniel Bruns and Richard Bubel and Christoph Gladisch and
                  Sarah Grebing and Reiner H\"ahnle and Martin Hentschel and Mihai Herda and Vladimir Klebanov and
                  Wojciech Mostowski and Christoph Scheben and Peter H. Schmitt and Mattias Ulbrich},
  booktitle =    {Verified Software: Theories, Tools, and Experiments (VSTTE'14)},
  editor =       {Dimitra Giannakopoulou and Daniel Kroening},
  pages =        {1--17},
  series =       {LNCS},
  volume =       {8471},
  year =         2014,
  doi =          {10.1007/978-3-319-12154-3_4},
  publisher =    {Springer}
}
@InProceedings{ABDHMZ2014,
  author =       {Afshin Amighi and Stefan Blom and Saeed Darabi and Marieke Huisman and Wojciech Mostowski and Marina Zaharieva-Stojanovski},
  title =        {Verification of Concurrent Systems with {VerCors}},
  booktitle =    {14th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Executable Software Models},
  pages =        {172--216},
  editor=        {Marco Bernardo and Ferruccio Damiani and Reiner H\"ahnle and Einar Broch Johnsen and Ina Schaefer},
  year =         2014,
  series =       {LNCS},
  volume =       {8483},
  doi =          {10.1007/978-3-319-07317-0_5},
  publisher =    {Springer},
}
@InProceedings{ABHMZ2014,
  author =       {Afshin Amighi and Stefan Blom and Marieke Huisman and Wojciech Mostowski and Marina Zaharieva-Stojanovski},
  title =        {Formal Specifications for {Java}'s Synchronisation Classes},
  booktitle =    {22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing},
  editor =       {Alberto Lluch Lafuente and Emilio Tuosto},
  year =         2014,
  doi =          {10.1109/PDP.2014.31},
  publisher =    {IEEE Computer Society},
  pages =        {725--733}
}
@InProceedings{Mostowski2013,
  author =       {Wojciech Mostowski},
  title =        {A Case Study in Formal Verification using Multiple Explicit Heaps},
  booktitle =    {2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems (FORTE/FMOODS)},
  editor =       {Dirk Beyer and Michele Boreale},
  pages =        {20--34},
  year =         2013,
  publisher =    {Springer},
  series =       {LNCS},
  doi =          {10.1007/978-3-642-38592-6_3},
  volume =       {7892}
}
@InProceedings{AhrendtMostowskiPaganelli2012,
  author =       {Wolfgang Ahrendt and Wojciech Mostowski and Gabriele Paganelli},
  title =        {Real-time {Java API} Specifications for High Coverage Test Generation},
  booktitle =    {The 10th International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES'12)},
  year =         2012,
  publisher =    {ACM},
  doi =          {10.1145/2388936.2388960},
  pages =        {145--154}
}
@InProceedings{VerificationCompetition2011Short,
  author =       {Thorsten Bormer and Marc Brockschmidt and Dino Distefano and Gidon Ernst and Jean-Christophe Filli\^{a}tre
                  and Radu Grigore and Marieke Huisman and Vladimir Klebanov and Claude March\'{e} and Rosemary Monahan and
                  Wojciech Mostowski and Nadia Polikarpova and Christoph Scheben and Gerhard Schellhorn and  Bogdan Tofan and
                  Julian Tschannen and Mattias Ulbrich},
  title =        {The {COST IC0701} Verification Competition 2011},
  booktitle =    {Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011)},
  editor =       {Bernhard Beckert and Ferruccio Damiani and Dilian Gurov},
  volume =       {7421},
  series =       {LNCS},
  pages =        {3--21},
  publisher =    {Springer},
  doi =          {10.1007/978-3-642-31762-0_2},
  year =         2012
}
@InProceedings{MostowskiVullers2011,
  author =       {Wojciech Mostowski and Pim Vullers},
  title =        {Efficient {U-Prove} Implementation for Anonymous Credentials on Smart Cards},
  booktitle =    {7th International ICST Conference on Security and Privacy in Communication Networks,
                  SecureComm 2011, London, UK, September 7--9, 2011. Proceedings},
  pages =        {243--260},
  editor =       {Muttukrishnan Rajarajan and Fred Piper and George Kesidis and Haining Wang},
  publisher =    {Springer},
  series =       {LNICST},
  doi =          {10.1007/978-3-642-31909-9_14},
  volume =       {96},
  year =         2012
}
@InProceedings{MostowskiPoll2010,
  author =       {Wojciech Mostowski and Erik Poll},
  title =        {Midlet Navigation Graphs in {JML}},
  booktitle =    {Formal Methods: Foundations and Applications, Proceedings of the 13th Brazilian Symposium on Formal Methods (SBMF 2010)},
  year =         2011,
  month =        {April},
  editor =       {Jim Davies and Leila Silva and Adenilso Sim{\~a}o},
  pages =        {17--32},
  series =       {LNCS},
  doi =          {10.1007/978-3-642-19829-8_2},
  volume =       {6527},
  publisher =    {Springer}
}
@InProceedings{BatinaHoepmanJacobsMostowskiVullers2010,
  author =       {Lejla Batina and Jaap-Henk Hoepman and Bart Jacobs and Wojciech Mostowski and Pim Vullers},
  title =        {Developing Efficient Blinded Attribute Certificates on Smart Cards via Pairings},
  booktitle =    {Smart Card Research and Advanced Application Conference CARDIS 2010, Proceedings, Passau, Germany},
  editor =       {Dieter Gollmann and Jean-Louis Lanet and Julien Iguchi-Cartigny},
  year =         2010,
  series =       {LNCS},
  doi =          {10.1007/978-3-642-12510-2_15},
  volume =       {6035},
  month =        {April},
  pages =        {209--222},
  publisher =    {Springer}
}
@InCollection{HogenboomMostowski2009,
  author =       {Jip Hogenboom and Wojciech Mostowski},
  title =        {Full Memory Attack on a {Java Card}},
  booktitle =    {4th Benelux Workshop on Information and System Security, Proceedings},
  year =         2009,
  address =      {Louvain-la-Neuve, Belgium},
  month =        {November},
  url =          {http://ceres.hh.se/mediawiki/images/5/5d/Mostowski_wissec2009.pdf},
  note =         {Available on-line}
}
@InProceedings{Mostowskietal2009,
  author =       {Wojciech Mostowski and Erik Poll and Julien Schmaltz and Jan Tretmans and Ronny Wichers Schreur},
  title =        {Model-Based Testing of Electronic Passports},
  booktitle =    {Formal Methods for Industrial Critical Systems 2009, Proceedings},
  year =         2009,
  month =        {November},
  editor =       {Mar\'{i}a Alpuente and Byron Cook and Christophe Joubert},
  series =       {LNCS},
  doi =          {10.1007/978-3-642-04570-7_19},
  pages =        {207--209},
  volume =       {5825},
  publisher =    {Springer}
}
@InProceedings{MostowskiPoll2008b,
  author =       {Wojciech Mostowski and Erik Poll},
  title =        {Java {Card} Applet Firewall Exploration and Exploitation},
  booktitle =    {eSmart 2008, Proceedings},
  year =         {2008},
  url =          {http://ceres.hh.se/mediawiki/images/3/36/Mostowski_esmart2008.pdf},
  month =        {September}
}
@InProceedings{MostowskiPoll2008,
  author =       {Wojciech Mostowski and Erik Poll},
  title =        {Malicious Code on {Java Card} Smartcards: {Attacks} and Countermeasures},
  booktitle =    {Smart Card Research and Advanced Application Conference CARDIS 2008, Proceedings, Egham, U.K.},
  editors =      {Gilles Grimaud and Fran\c{c}ois-Xavier Standaert},
  year =         {2008},
  series =       {LNCS},
  doi =          {10.1007/978-3-540-85893-5_1},
  volume =       5189,
  month =        {September},
  publisher =    {Springer},
  pages =        {1--16}
}
@InProceedings{RichterMostowskiPoll2008,
  author =       {Henning Richter and Wojciech Mostowski and Erik Poll},
  title =        {Fingerprinting Passports},
  booktitle =    {NLUUG 2008 Spring Conference on Security, Proceedings},
  url =          {http://ceres.hh.se/mediawiki/images/3/37/Mostowski_nluug2008.pdf},
  month =        {May},
  year =         2008
}
@InProceedings{Mostowski2007,
  author =       {Wojciech Mostowski},
  title =        {Fully Verified {Java Card API} Reference Implementation},
  booktitle =    {Verify'07 4th International Verification Workshop},
  year =         2007,
  editor =       {Bernhard Beckert},
  month =        {July},
  volume =       {259},
  url =          {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-259/paper12.pdf},
  series =       {CEUR WS}
}
@InProceedings{HubbersMostowskiPoll2006,
  author =       {Engelbert Hubbers and Wojciech Mostowski and Erik Poll},
  title =        {Tearing {Java Cards}},
  booktitle =    {Proceedings, e-Smart 2006, Sophia-Antipolis, France, September 20--22},
  note =         {Available on-line},
  url =          {http://ceres.hh.se/mediawiki/images/8/83/Mostowski_esmart2006.pdf},
  year =         2006
}
@InProceedings{Mostowski2006,
  author =       {Wojciech Mostowski},
  title =        {Formal Reasoning about Non-Atomic {Java Card} Methods in {Dynamic Logic}},
  booktitle =    {Proceedings, Formal Methods (FM) 2006, Hamilton, Ontario, Canada}, 
  year =         2006,
  month =        {August},
  editor =       {Jayadev Misra and Tobias Nipkow and Emil Sekerinski},
  series =       {LNCS},
  doi =          {10.1007/11813040_30},
  pages =        {444--459},
  volume =       {4085},
  publisher =    {Springer}
}
@InProceedings{Mostowski2005,
  author =       {Wojciech Mostowski},
  title =        {Formalisation and Verification of {Java Card} Security Properties in {Dynamic Logic}},
  booktitle =    {Proceedings, Fundamental Approaches to Software Engineering (FASE) Conference 2005, Edinburgh, Scotland}, 
  year =         2005,
  editor =       {Maura Cerioli},
  volume =       {3442},
  pages =        {357--371},
  series =       {LNCS},
  doi =          {10.1007/978-3-540-31984-9_27},
  month =        {April},
  publisher =    {Springer}
}
@InProceedings{HaehnleMostowski2004,
  author =       {Reiner H\"ahnle and Wojciech Mostowski},
  title =        {Verification of Safety Properties in the Presence of Transactions},
  booktitle =    {Proceedings, Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS'04) Workshop},
  editor   =     {Gilles Barthe and Lilian Burdy and Marieke Huisman and Jean-Louis Lanet and Traian Muntean},
  publisher =    {Springer},
  pages =        {151--171},
  year =         2005,
  volume =       {3362},
  series =       {LNCS},
  doi =          {10.1007/978-3-540-30569-9_8}
}
@InProceedings{LarssonMostowski2003,
  author =       {Daniel Larsson and Wojciech Mostowski},
  title =        {Specifying {Java Card API} in {OCL}},
  booktitle =    {OCL 2.0 Workshop at UML 2003},
  pages =        {3--19},
  year =         2004,
  editor =       {Peter H. Schmitt},
  volume =       {102C},
  series =       {ENTCS},
  doi =          {10.1016/j.entcs.2003.09.001},
  month =        {November},
  publisher =    {Elsevier}
}
@InProceedings{BeckertMostowski2003,
  author =       {Bernhard Beckert and Wojciech Mostowski},
  title =        {A Program Logic for Handling {Java Card}'s Transaction Mechanism},
  booktitle =    {Proceedings, Fundamental Approaches to Software Engineering (FASE) Conference 2003, Warsaw, Poland}, 
  pages =        {246--260},
  year =         2003,
  editor =       {Mauro Pezz\`{e}},
  volume =       {2621},
  series =       {LNCS},
  doi =          {10.1007/3-540-36578-8_18},
  month =        {April},
  publisher =    {Springer}
}
@InProceedings{KeYFASE2002,
  author =       {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert and Martin Giese and
                  Reiner H\"{a}hnle and Wolfram Menzel and Wojciech Mostowski and Peter H. Schmitt},
  title =        {The {KeY} System: {I}ntegrating Object-Oriented Design and Formal Methods},
  booktitle =    {Proceedings, Fundamental Approaches to Software Engineering (FASE) Conference, Grenoble, France},
  editor =       {Ralf-Detlef Kutsche and Herbert Weber},
  pages =        {327--330},
  month =        {April},
  publisher =    {Springer},
  series =       {LNCS},
  doi =          {10.1007/3-540-45923-5_23},
  volume =       {2306},
  year =         2002
}
@InProceedings{Mostowski2002,
  author =       {Wojciech Mostowski},
  title =        {Rigorous development of {Java Card} applications},
  booktitle =    {Proceedings, Fourth Workshop on Rigorous Object-Oriented Methods, London, U.K.},
  year =         2002,
  month =        {March},
  editor =       {T. Clarke and A. Evans and K. Lano},
  note =         {Available on-line},
  url =          {http://ceres.hh.se/mediawiki/images/f/fb/Mostowski_room2002.ps}
}
@InProceedings{JanowskiMostowski2000,
  author =       {Tomasz Janowski and Wojciech Mostowski},
  title =        {Fail-Stop Components by Pattern Matching},
  booktitle =    {Formal Methods for Open Object-Based Distributed Systems},
  editor =       {Scott F. Smith and Carolyn L. Talcott},
  year =         2000,
  publisher =    {Kluwer Academic Publishers},
  month =        {September}
}
@Misc{BJMPV-STWICT2010,
  author =       {Lejla Batina and Bart Jacobs and Wojciech Mostowski and Erik Poll and Pim Vullers},
  title =        {{Security and Privacy of Smartcard-based e-Identity}},
  howpublished = {Poster Presentation at STW.ICT 2010 Conference, Veldhoven, the Netherlands},
  month =        {November},
  year =         2010,
  note =         {Available on-line}
}
@InBook{KeYBook2-Chapter9,
  author =       {Daniel Grahl and Richard Bubel and Wojciech Mostowski and Peter H. Schmitt and Mattias Ulbrich and Benjamin Wei{\ss}},
  title =        {Deductive Software Verification -- {The} {\KeY{}} Book},
  subtitle =     {From Theory to Practice},
  editor =       {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"a}hnle and Peter H. Schmitt and Mattias Ulbrich},
  volume =       {10001},
  series =       {LNCS},
  publisher =    {Springer International Publishing},
  year =         {2017},
  chapter =      {Chapter~9. Modular Specification and Verification},
  pages =        {289--351},
  doi =          {10.1007/978-3-319-49812-6_9},
  isbn =         {978-3-319-49811-9}
}
@InBook{KeYBook2-Chapter10,
  author =       {Wojciech Mostowski},
  title =        {Deductive Software Verification -- {The} {\KeY{}} Book},
  subtitle =     {From Theory to Practice},
  editor =       {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"a}hnle and Peter H. Schmitt and Mattias Ulbrich},
  volume =       {10001},
  series =       {LNCS},
  publisher =    {Springer International Publishing},
  year =         {2017},
  chapter =      {Chapter~10. Verifying {Java Card} Programs},
  pages =        {353--380},
  doi =          {10.1007/978-3-319-49812-6_10},
  isbn =         {978-3-319-49811-9}
}
@InBook{KeYBook2-AppendixB,
  author =       {Wojciech Mostowski and Richard Bubel},
  title =        {Deductive Software Verification -- {The} {\KeY{}} Book},
  subtitle =     {From Theory to Practice},
  editor =       {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"a}hnle and Peter H. Schmitt and Mattias Ulbrich},
  volume =       {10001},
  series =       {LNCS},
  publisher =    {Springer International Publishing},
  year =         {2017},
  chapter =      {Appendix~B. {KeY} File Reference},
  pages =        {631--665},
  isbn =         {978-3-319-49811-9}
}
@InBook{KeYBook-Chapter9,
  author =       {Wojciech Mostowski},
  editor =       {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
  title =        {Verification of Object-Oriented Software: {The} {KeY} Approach},
  chapter =      {9. From Sequential {Java} to {Java Card}},
  publisher =    {Springer},
  series =       {LNAI},
  volume =       4334,
  year =         2007,
  doi =          {10.1007/978-3-540-69061-0_9},
  pages =        {375--405}
}
@InBook{KeYBook-Chapter14,
  author =       {Wojciech Mostowski},
  editor =       {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
  title =        {Verification of Object-Oriented Software: {The} {KeY} Approach},
  chapter =      {14. The {Demoney} Case Study},
  publisher =    {Springer},
  series =       {LNAI},
  volume =       4334,
  year =         2007,
  doi =          {10.1007/978-3-540-69061-0_14},
  pages =        {533--568}
}
@InBook{KeYBook-AppendixB,
  author =       {Wojciech Mostowski},
  editor =       {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
  title =        {Verification of Object-Oriented Software: {The} {KeY} Approach},
  chapter =      {Appendix B. The {KeY} Syntax},
  series =       {LNAI},
  volume =       4334,
  publisher =    {Springer},
  year =         2007,
  pages =        {599--626}
}
@InBook{JanowskiMostowski2002,
  author =       {Tomasz Janowski and Wojciech Mostowski},
  editor =       {Hung Dang Van and Chris George and Tomasz Janowski and Richard Moore},
  title =        {Specification Case Studies in {RAISE}},
  chapter =      {13. Fail-Stop Components by Pattern Matching},
  publisher =    {Springer},
  year =         2002,
  pages =        {341--368}
}
@PhdThesis{MostowskiPhD2005,
  author =       {Wojciech Mostowski},
  title =        {Formal Development of Safe and Secure {Java Card} Applets},
  school =       {Chalmers University of Technology, Department of Computer Science and Engineering, G\"oteborg, Sweden},
  year =         2005,
  month =        {February},
  isbn =         {91-7291-575-7}
}
@TechReport{MostowskiLic2002,
  author =       {Wojciech Mostowski},
  title =        {Towards Development of Safe and Secure {Java Card} Applets},
  institution =  {Chalmers University of Technology, Computing Science Department, G\"{o}teborg, Sweden},
  year =         2002,
  type =         {Licentiate Thesis},
  number =       {16L},
  month =        {December}
}
@TechReport{VerifyThis2017-TR,
  author =       {Marieke Huisman and Rosemary Monahan and Wojciech Mostowski and Peter M{\"u}ller and Mattias Ulbrich},
  title =        {{VerifyThis 2017}: A Program Verification Competition},
  institution =  {Karlsruhe Institute of Technology},
  series =       {Karlsruhe Reports in Informatics},
  doi =          {10.5445/ir/1000077160},
  url =          {https://publikationen.bibliothek.kit.edu/1000077160},
  year =         2017,
  number =       {2017-10}
}
@TechReport{Mostowski2013-TR,
  author =       {Afshin Amighi and Stefan Blom and Marieke Huisman and Wojciech Mostowski and Marina Zaharieva-Stojanovski},
  title =        {Formal Specifications for {Java}'s Synchronisation Classes},
  number =       {TR--CTIT--13--18},
  institution =  {University of Twente},
  year =         2013,
}
@TechReport{2010-Mostowski-ElectronicNutshell,
  author =       {{Mostowski}, Wojciech and {Poll}, Erik},
  title =        {{Electronic Passports in a Nutshell}},
  number =       {ICIS--R10004},
  month  =       {June},
  institution =  {Radboud University Nijmegen},
  year =         {2010},
  note =         {Available at \url{https://pms.cs.ru.nl/iris-diglib/src/getContent.php?id=2010-Mostowski-ElectronicNutshell}}
}
@TechReport{2009-Mostowski-MidletGraphs,
  author =       {{Mostowski}, Wojciech and {Poll}, Erik},
  title =        {{Midlet Navigation Graphs in JML}},
  number =       {ICIS--R09004},
  month =        {August},
  institution =  {Radboud University Nijmegen},
  year =         2009,
  note =         {Available at \url{https://pms.cs.ru.nl/iris-diglib/src/getContent.php?id=2009-Mostowski-MidletGraphs}}
}
@techreport{MostowskiPoll2007,
  author =       {{Mostowski}, Wojciech and {Poll}, Erik},
  title =        {{Testing the Java Card Applet Firewall}},
  number =       {ICIS--R07029},
  month =        {December},
  institution =  {Radboud University Nijmegen},
  year =         2007,
  note =         {Available on-line}
}
@TechReport{STReport2007,
  author =       {Wojciech Mostowski and Jing Pan and Srikanth Akkiraju and Erik de Vink and Erik Poll and Jerry den Hartog},
  title =        {A Comparison of {Java Cards}: {State}-of-Affairs 2006},
  institution =  {Technical University Eindhoven},
  year =         2007,
  number =       {CS-Report CSR 07-06},
  note =         {Available on request}
}
@TechReport{Mostowski2004,
  author =       {Wojciech Mostowski},
  title =        {Formalisation and Verification of {Java Card} Security Properties in {Dynamic Logic}},
  institution =  {Department of Computing Science, Chalmers University of Technology, G\"{o}teborg, Sweden},
  year =         2004,
  month =        {October},
  number =       {2004--08}
}
@Unpublished{Mostowski-JCtools,
  author =       {Wojciech Mostowski},
  title =        {{Java Card} Tools for {Together Control Center}},
  note =         {Available on-line}
}
@TechReport{KeYTool2003,
  author =      {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert and Richard Bubel and Martin Giese and Reiner H\"{a}hnle
                 and Wolfram Menzel and Wojciech Mostowski and Andreas Roth and Steffen Schlager and Peter H. Schmitt},
  title =       {The {KeY} Tool},
  institution = {Department of Computing Science, Chalmers University of Technology, G\"{o}teborg, Sweden},
  year =        2003,
  number =      {2003--05}
}