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

From CERES
Jump to: navigation, search
Line 1: Line 1:
 
<div id="Mostowski-VerifyThis2012"><pre>
 
<div id="Mostowski-VerifyThis2012"><pre>
 
@Article{Mostowski-VerifyThis2012,
 
@Article{Mostowski-VerifyThis2012,
   author = {Daniel Bruns and Wojciech Mostowski and Mattias Ulbrich},
+
   author =       {Daniel Bruns and Wojciech Mostowski and Mattias Ulbrich},
   title = {Implementation-level Verification of Algorithms with {KeY}},
+
   title =       {Implementation-level Verification of Algorithms with {KeY}},
 
   journal =      {Software Tools for Technology Transfer},
 
   journal =      {Software Tools for Technology Transfer},
 
   year =        2013,
 
   year =        2013,
Line 12: Line 12:
 
<div id="KeYSoSyM2004"><pre>
 
<div id="KeYSoSyM2004"><pre>
 
@Article{KeYSoSyM2004,
 
@Article{KeYSoSyM2004,
   author = {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert and Richard Bubel and
+
   author =       {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert and Richard Bubel and Martin Giese and Reiner H\"{a}hnle
                  Martin Giese and Reiner H\"{a}hnle and Wolfram Menzel and Wojciech Mostowski
+
                  and Wolfram Menzel and Wojciech Mostowski and Andreas Roth and Steffen Schlager and Peter H. Schmitt},
                  and Andreas Roth and Steffen Schlager and Peter H. Schmitt},
+
   title =       {The {KeY} Tool},
   title = {The {KeY} Tool},
+
   journal =     {Software and Systems Modeling},
   journal = {Software and Systems Modeling},
+
 
   volume =      {4},
 
   volume =      {4},
 
   number =      {1},
 
   number =      {1},
Line 27: Line 26:
  
 
<div id="HuismanMostowski2015"><pre>
 
<div id="HuismanMostowski2015"><pre>
@inproceedings{HuismanMostowski2015,
+
@InProceedings{HuismanMostowski2015,
   title =     {A Symbolic Approach to Permission Accounting for Concurrent Reasoning},
+
   title =       {A Symbolic Approach to Permission Accounting for Concurrent Reasoning},
   author =   {Marieke Huisman and Wojciech Mostowski},
+
   author =       {Marieke Huisman and Wojciech Mostowski},
   year =     2015,
+
   year =         2015,
   publisher = {IEEE Computer Society},
+
   publisher =   {IEEE Computer Society},
   booktitle = {14th International Symposium on Parallel and Distributed Computing (ISPDC 2015)},
+
   booktitle =   {14th International Symposium on Parallel and Distributed Computing (ISPDC 2015)},
   note =     {To appear}
+
   note =         {To appear}
 
}
 
}
 
</pre></div>
 
</pre></div>
  
 
<div id="MostowskiUlbrich2015"><pre>
 
<div id="MostowskiUlbrich2015"><pre>
@inproceedings{MostowskiUlbrich2015,
+
@InProceedings{MostowskiUlbrich2015,
   author =   {Wojciech Mostowski and Mattias Ulbrich},
+
   author =       {Wojciech Mostowski and Mattias Ulbrich},
   title =     {Dynamic Dispatch for Method Contracts through Abstract Predicates},
+
   title =       {Dynamic Dispatch for Method Contracts through Abstract Predicates},
   booktitle = {15th International Conference on MODULARITY (MODULARITY'15)},
+
   booktitle =   {15th International Conference on MODULARITY (MODULARITY'15)},
   publisher = {ACM},
+
   publisher =   {ACM},
   year =     {2015},
+
   year =         {2015},
   doi =       {10.1145/2724525.2724574},
+
   doi =         {10.1145/2724525.2724574},
   pages =     {109--116}
+
   pages =       {109--116}
 
}
 
}
 
</pre></div>
 
</pre></div>
  
 
<div id="KeY2014"><pre>
 
<div id="KeY2014"><pre>
@inproceedings{KeY2014,
+
@InProceedings{KeY2014,
   title = {The {KeY} Platform for Verification and Analysis of {Java} Programs},
+
   title =       {The {KeY} Platform for Verification and Analysis of {Java} Programs},
   author = {Wolfgang Ahrendt and Bernhard Beckert and Daniel Bruns and Richard Bubel
+
   author =       {Wolfgang Ahrendt and Bernhard Beckert and Daniel Bruns and Richard Bubel and Christoph Gladisch and
            and Christoph Gladisch and Sarah Grebing and Reiner H\"ahnle and Martin Hentschel
+
                  Sarah Grebing and Reiner H\"ahnle and Martin Hentschel and Mihai Herda and Vladimir Klebanov and
            and Mihai Herda and Vladimir Klebanov and Wojciech Mostowski and Christoph Scheben
+
                  Wojciech Mostowski and Christoph Scheben and Peter H. Schmitt and Mattias Ulbrich},
            and Peter H. Schmitt and Mattias Ulbrich},
+
   booktitle =   {Verified Software: Theories, Tools, and Experiments (VSTTE)},
   booktitle = {Verified Software: Theories, Tools, and Experiments (VSTTE)},
+
   editor =       {Dimitra Giannakopoulou and Daniel Kroening},
   editor =   {Dimitra Giannakopoulou and Daniel Kroening},
+
   pages =       {1--17},
   pages =     {1--17},
+
   series =       {LNCS},
   series =   {LNCS},
+
   volume =       {8471},
   volume =   {8471},
+
   year =         2014,
   year =     2014,
+
   publisher =   {Springer}
   publisher = {Springer}
+
 
}
 
}
 
</pre></div>
 
</pre></div>
  
 
<div id="ABDHMZ2014"><pre>
 
<div id="ABDHMZ2014"><pre>
@inproceedings{ABDHMZ2014,
+
@InProceedings{ABDHMZ2014,
   author =   {Afshin Amighi and Stefan Blom and Saeed Darabi and Marieke Huisman and
+
   author =       {Afshin Amighi and Stefan Blom and Saeed Darabi and Marieke Huisman and Wojciech Mostowski and Marina Zaharieva-Stojanovski},
              Wojciech Mostowski and Marina Zaharieva-Stojanovski},
+
   title =       {Verification of Concurrent Systems with {VerCors}},
   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},
   booktitle = {14th International School on Formal Methods for the Design of
+
   pages =       {172--216},
              Computer, Communication and Software Systems: Executable Software Models},
+
   editor=       {Marco Bernardo and Ferruccio Damiani and Reiner H\"ahnle and Einar Broch Johnsen and Ina Schaefer},
   pages =     {172--216},
+
   year =         2014,
   editor=     {Marco Bernardo and Ferruccio Damiani and Reiner H\"ahnle and Einar Broch Johnsen and Ina Schaefer},
+
   series =       {LNCS},
   year =     2014,
+
   volume =       {8483},
   series =   {LNCS},
+
   publisher =   {Springer},
   volume =   {8483},
+
   publisher = {Springer},
+
 
}
 
}
 
</pre></div>
 
</pre></div>
  
 
<div id="ABHMZ2014"><pre>
 
<div id="ABHMZ2014"><pre>
@inproceedings{ABHMZ2014,
+
@InProceedings{ABHMZ2014,
   author =   {Afshin Amighi and Stefan Blom and Marieke Huisman and Wojciech Mostowski and Marina Zaharieva-Stojanovski},
+
   author =       {Afshin Amighi and Stefan Blom and Marieke Huisman and Wojciech Mostowski and Marina Zaharieva-Stojanovski},
   title =     {Formal Specifications for {Java}'s Synchronisation Classes},
+
   title =       {Formal Specifications for {Java}'s Synchronisation Classes},
   booktitle = {22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing},
+
   booktitle =   {22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing},
   editor =   {Alberto Lluch Lafuente and Emilio Tuosto},
+
   editor =       {Alberto Lluch Lafuente and Emilio Tuosto},
   year =     {2014},
+
   year =         2014,
   doi =       {10.1109/PDP.2014.31},
+
   doi =         {10.1109/PDP.2014.31},
   publisher = {IEEE Computer Society},
+
   publisher =   {IEEE Computer Society},
   pages =     {725--733}
+
   pages =       {725--733}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 97: Line 93:
 
<div id="Mostowski2013"><pre>
 
<div id="Mostowski2013"><pre>
 
@InProceedings{Mostowski2013,
 
@InProceedings{Mostowski2013,
   author =   {Wojciech Mostowski},
+
   author =       {Wojciech Mostowski},
   title =     {A Case Study in Formal Verification using Multiple Explicit Heaps},
+
   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)},
+
   booktitle =   {2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems (FORTE/FMOODS)},
   editor =   {Dirk Beyer and Michele Boreale},
+
   editor =       {Dirk Beyer and Michele Boreale},
   pages =     {20--34},
+
   pages =       {20--34},
   year =     {2013},
+
   year =         2013,
   publisher = {Springer},
+
   publisher =   {Springer},
   series =   {LNCS},
+
   series =       {LNCS},
   volume =   {7892}
+
   volume =       {7892}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 111: Line 107:
 
<div id="AhrendtMostowskiPaganelli2012"><pre>
 
<div id="AhrendtMostowskiPaganelli2012"><pre>
 
@InProceedings{AhrendtMostowskiPaganelli2012,
 
@InProceedings{AhrendtMostowskiPaganelli2012,
   author =   {Wolfgang Ahrendt and Wojciech Mostowski and Gabriele Paganelli},
+
   author =       {Wolfgang Ahrendt and Wojciech Mostowski and Gabriele Paganelli},
   title =     {Real-time {Java API} Specifications for High Coverage Test Generation},
+
   title =       {Real-time {Java API} Specifications for High Coverage Test Generation},
   booktitle = {The 10th International Workshop on Java
+
   booktitle =   {The 10th International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES'12)},
              Technologies for Real-time and Embedded Systems (JTRES'12)},
+
   year =         2012,
   year =     {2012},
+
   publisher =   {ACM},
   publisher = {ACM},
+
   doi =         {10.1145/2388936.2388960}
   doi =       {10.1145/2388936.2388960}
+
   pages =       {145--154}
   pages =     {145--154}
+
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 124: Line 119:
 
<div id="VerificationCompetition2011Short"><pre>
 
<div id="VerificationCompetition2011Short"><pre>
 
@InProceedings{VerificationCompetition2011Short,
 
@InProceedings{VerificationCompetition2011Short,
   author =   {Thorsten Bormer and Marc Brockschmidt and Dino Distefano and Gidon Ernst and  
+
   author =       {Thorsten Bormer and Marc Brockschmidt and Dino Distefano and Gidon Ernst and Jean-Christophe Filli\^{a}tre
              Jean-Christophe Filli\^{a}tre and Radu Grigore and Marieke Huisman and Vladimir Klebanov and  
+
                  and Radu Grigore and Marieke Huisman and Vladimir Klebanov and Claude March\'{e} and Rosemary Monahan and
              Claude March\'{e} and Rosemary Monahan and Wojciech Mostowski and Nadia Polikarpova and
+
                  Wojciech Mostowski and Nadia Polikarpova and Christoph Scheben and Gerhard Schellhorn and  Bogdan Tofan and
              Christoph Scheben and Gerhard Schellhorn and  Bogdan Tofan and Julian Tschannen and Mattias Ulbrich},
+
                  Julian Tschannen and Mattias Ulbrich},
   title =     {The {COST IC0701} Verification Competition 2011},
+
   title =       {The {COST IC0701} Verification Competition 2011},
   booktitle = {Revised Selected Papers, International Conference on Formal  
+
   booktitle =   {Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011)},
              Verification of Object-Oriented Software (FoVeOOS 2011)},
+
   editor =       {Bernhard Beckert and Ferruccio Damiani and Dilian Gurov},
   editor =   {Bernhard Beckert and Ferruccio Damiani and Dilian Gurov},
+
   volume =       {7421},
   volume =   {7421},
+
   series =       {LNCS},
   series =   {LNCS},
+
   pages =       {3--21},
   pages =     {3--21},
+
   publisher =   {Springer},
   publisher = {Springer},
+
   year =         2012
   year =     {2012}
+
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 142: Line 136:
 
<div id="MostowskiVullers2011"><pre>
 
<div id="MostowskiVullers2011"><pre>
 
@InProceedings{MostowskiVullers2011,
 
@InProceedings{MostowskiVullers2011,
   author   = {Wojciech Mostowski and Pim Vullers},
+
   author =       {Wojciech Mostowski and Pim Vullers},
   title     = {Efficient {U-Prove} Implementation for Anonymous Credentials on Smart Cards},
+
   title =       {Efficient {U-Prove} Implementation for Anonymous Credentials on Smart Cards},
   booktitle = {7th International ICST Conference on Security and Privacy in Communication Networks,
+
   booktitle =   {7th International ICST Conference on Security and Privacy in Communication Networks,
              SecureComm 2011, London, UK, September 7--9, 2011. Proceedings},
+
                  SecureComm 2011, London, UK, September 7--9, 2011. Proceedings},
   pages     = {243--260},
+
   pages =       {243--260},
   editor   = {Muttukrishnan Rajarajan and Fred Piper and George Kesidis and Haining Wang},
+
   editor =       {Muttukrishnan Rajarajan and Fred Piper and George Kesidis and Haining Wang},
   publisher = {Springer},
+
   publisher =   {Springer},
   series   = {LNICST},
+
   series =       {LNICST},
   volume   = {96},
+
   volume =       {96},
   year     = {2012},
+
   year =         2012
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 157: Line 151:
 
<div id="MostowskiPoll2010"><pre>
 
<div id="MostowskiPoll2010"><pre>
 
@InProceedings{MostowskiPoll2010,
 
@InProceedings{MostowskiPoll2010,
   author = {Wojciech Mostowski and Erik Poll},
+
   author =       {Wojciech Mostowski and Erik Poll},
   title = {Midlet Navigation Graphs in {JML}},
+
   title =       {Midlet Navigation Graphs in {JML}},
   booktitle =    {Formal Methods: Foundations and Applications,
+
   booktitle =    {Formal Methods: Foundations and Applications, Proceedings of the 13th Brazilian Symposium on Formal Methods (SBMF 2010)},
                  Proceedings of the 13th Brazilian Symposium on Formal Methods (SBMF 2010)},
+
 
   year =        2011,
 
   year =        2011,
 
   month =        {April},
 
   month =        {April},
   editor = {Jim Davies and Leila Silva and Adenilso Sim{\~a}o},
+
   editor =       {Jim Davies and Leila Silva and Adenilso Sim{\~a}o},
 
   pages =        {17--32},
 
   pages =        {17--32},
   series = {LNCS},
+
   series =       {LNCS},
   volume =      6527,
+
   volume =      {6527},
   publisher = {Springer}
+
   publisher =   {Springer}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 176: Line 169:
 
   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},
   year =        {2010},
+
   year =        2010,
 
   series =      {LNCS},
 
   series =      {LNCS},
 
   volume =      {6035},
 
   volume =      {6035},
Line 187: Line 180:
 
<div id="HogenboomMostowski2009"><pre>
 
<div id="HogenboomMostowski2009"><pre>
 
@InCollection{HogenboomMostowski2009,
 
@InCollection{HogenboomMostowski2009,
   author = {Jip Hogenboom and Wojciech Mostowski},
+
   author =       {Jip Hogenboom and Wojciech Mostowski},
   title = {Full Memory Attack on a {Java Card}},
+
   title =       {Full Memory Attack on a {Java Card}},
   booktitle = {4th Benelux Workshop on Information and System Security,
+
   booktitle =   {4th Benelux Workshop on Information and System Security, Proceedings},
                  Proceedings},
+
   year =         2009,
   year = 2009,
+
   address =     {Louvain-la-Neuve, Belgium},
   address = {Louvain-la-Neuve, Belgium},
+
 
   month =        {November},
 
   month =        {November},
   note =        {Available at \url{http://www.dice.ucl.ac.be/crypto/wissec2009/static/13.pdf}}
+
   note =        {Available on-line}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 200: Line 192:
 
<div id="Mostowskietal2009"><pre>
 
<div id="Mostowskietal2009"><pre>
 
@InProceedings{Mostowskietal2009,
 
@InProceedings{Mostowskietal2009,
   author = {Wojciech Mostowski and Erik Poll and Julien Schmaltz and Jan Tretmans and Ronny Wichers Schreur},
+
   author =       {Wojciech Mostowski and Erik Poll and Julien Schmaltz and Jan Tretmans and Ronny Wichers Schreur},
   title = {Model-Based Testing of Electronic Passports},
+
   title =       {Model-Based Testing of Electronic Passports},
   booktitle = {Formal Methods for Industrial Critical Systems 2009, Proceedings},
+
   booktitle =   {Formal Methods for Industrial Critical Systems 2009, Proceedings},
 
   year =        2009,
 
   year =        2009,
 
   month =        {November},
 
   month =        {November},
 
   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},
 
   pages =        {207--209},
 
   pages =        {207--209},
 
   volume =      {5825},
 
   volume =      {5825},
Line 234: Line 226:
 
   month =        {September},
 
   month =        {September},
 
   publisher =    {Springer},
 
   publisher =    {Springer},
   pages =        {1--16}
+
   pages =        {1--16}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 240: Line 232:
 
<div id="RichterMostowskiPoll2008"><pre>
 
<div id="RichterMostowskiPoll2008"><pre>
 
@InProceedings{RichterMostowskiPoll2008,
 
@InProceedings{RichterMostowskiPoll2008,
   author = {Henning Richter and Wojciech Mostowski and Erik Poll},
+
   author =       {Henning Richter and Wojciech Mostowski and Erik Poll},
   title = {Fingerprinting Passports},
+
   title =       {Fingerprinting Passports},
 
   booktitle =    {NLUUG 2008 Spring Conference on Security, Proceedings},
 
   booktitle =    {NLUUG 2008 Spring Conference on Security, Proceedings},
 
   month =        {May},
 
   month =        {May},
Line 250: Line 242:
 
<div id="Mostowski2007"><pre>
 
<div id="Mostowski2007"><pre>
 
@InProceedings{Mostowski2007,
 
@InProceedings{Mostowski2007,
   author = {Wojciech Mostowski},
+
   author =       {Wojciech Mostowski},
   title = {Fully Verified {Java Card API} Reference Implementation},
+
   title =       {Fully Verified {Java Card API} Reference Implementation},
   booktitle = {Verify'07 4th International Verification Workshop},
+
   booktitle =   {Verify'07 4th International Verification Workshop},
   year = 2007,
+
   year =         2007,
   editor = {Bernhard Beckert},
+
   editor =       {Bernhard Beckert},
 
   month =        {July},
 
   month =        {July},
 
   volume =      {259},
 
   volume =      {259},
Line 263: Line 255:
 
<div id="HubbersMostowskiPoll2006"><pre>
 
<div id="HubbersMostowskiPoll2006"><pre>
 
@InProceedings{HubbersMostowskiPoll2006,
 
@InProceedings{HubbersMostowskiPoll2006,
   author = {Engelbert Hubbers and Wojciech Mostowski and Erik Poll},
+
   author =       {Engelbert Hubbers and Wojciech Mostowski and Erik Poll},
   title = {Tearing {Java Cards}},
+
   title =       {Tearing {Java Cards}},
   booktitle = {Proceedings, e-Smart 2006, Sophia-Antipolis, France, September 20--22},
+
   booktitle =   {Proceedings, e-Smart 2006, Sophia-Antipolis, France, September 20--22},
   url =         {http://www.cs.ru.nl/~woj/papers/download/esmart2006.pdf},
+
   note =         {Available on-line},
   year =        {2006}
+
   year =        2006
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 273: Line 265:
 
<div id="Mostowski2006"><pre>
 
<div id="Mostowski2006"><pre>
 
@InProceedings{Mostowski2006,
 
@InProceedings{Mostowski2006,
   author = {Wojciech Mostowski},
+
   author =       {Wojciech Mostowski},
   title = {Formal Reasoning about Non-Atomic {Java Card} Methods in {Dynamic Logic}},
+
   title =       {Formal Reasoning about Non-Atomic {Java Card} Methods in {Dynamic Logic}},
   booktitle = {Proceedings, Formal Methods (FM) 2006, Hamilton, Ontario, Canada},  
+
   booktitle =   {Proceedings, Formal Methods (FM) 2006, Hamilton, Ontario, Canada},  
 
   year =        2006,
 
   year =        2006,
 
   month =        {August},
 
   month =        {August},
 
   editor =      {Jayadev Misra and Tobias Nipkow and Emil Sekerinski},
 
   editor =      {Jayadev Misra and Tobias Nipkow and Emil Sekerinski},
   series = {LNCS},
+
   series =       {LNCS},
 
   pages =        {444--459},
 
   pages =        {444--459},
 
   volume =      {4085},
 
   volume =      {4085},
Line 288: Line 280:
 
<div id="Mostowski2005"><pre>
 
<div id="Mostowski2005"><pre>
 
@InProceedings{Mostowski2005,
 
@InProceedings{Mostowski2005,
   author = {Wojciech Mostowski},
+
   author =       {Wojciech Mostowski},
   title =        {Formalisation and Verification of {Java Card}
+
   title =        {Formalisation and Verification of {Java Card} Security Properties in {Dynamic Logic}},
                  Security Properties in {Dynamic Logic}},
+
   booktitle =    {Proceedings, Fundamental Approaches to Software Engineering (FASE) Conference 2005, Edinburgh, Scotland},  
   booktitle =    {Proceedings,
+
   year =         2005,
                  Fundamental Approaches to Software Engineering (FASE)
+
                  Conference 2005, Edinburgh, Scotland},  
+
   year = 2005,
+
 
   editor =      {Maura Cerioli},
 
   editor =      {Maura Cerioli},
 
   volume =      {3442},
 
   volume =      {3442},
 
   pages =        {357--371},
 
   pages =        {357--371},
   series = {LNCS},
+
   series =       {LNCS},
 
   month =        {April},
 
   month =        {April},
 
   publisher =    {Springer}
 
   publisher =    {Springer}
Line 308: Line 297:
 
   author =      {Reiner H\"ahnle and Wojciech Mostowski},
 
   author =      {Reiner H\"ahnle and Wojciech Mostowski},
 
   title =        {Verification of Safety Properties in the Presence of Transactions},
 
   title =        {Verification of Safety Properties in the Presence of Transactions},
   booktitle =    {Proceedings, Construction and Analysis of Safe, Secure
+
   booktitle =    {Proceedings, Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS'04) Workshop},
                  and Interoperable Smart devices (CASSIS'04) Workshop},
+
   editor  =    {Gilles Barthe and Lilian Burdy and Marieke Huisman and Jean-Louis Lanet and Traian Muntean},
   editor  =    {Gilles Barthe and Lilian Burdy and Marieke Huisman and  
+
                  Jean-Louis Lanet and Traian Muntean},
+
 
   publisher =    {Springer},
 
   publisher =    {Springer},
 
   pages =        {151--171},
 
   pages =        {151--171},
Line 322: Line 309:
 
<div id="LarssonMostowski2003"><pre>
 
<div id="LarssonMostowski2003"><pre>
 
@InProceedings{LarssonMostowski2003,
 
@InProceedings{LarssonMostowski2003,
   author = {Daniel Larsson and Wojciech Mostowski},
+
   author =       {Daniel Larsson and Wojciech Mostowski},
   title = {Specifying {Java Card API} in {OCL}},
+
   title =       {Specifying {Java Card API} in {OCL}},
   booktitle = {OCL 2.0 Workshop at UML 2003},
+
   booktitle =   {OCL 2.0 Workshop at UML 2003},
 
   pages =        {3--19},
 
   pages =        {3--19},
 
   year =        2004,
 
   year =        2004,
 
   editor =      {Peter H. Schmitt},
 
   editor =      {Peter H. Schmitt},
   volume = {102C},
+
   volume =       {102C},
   series = {ENTCS},
+
   series =       {ENTCS},
   month = {November},
+
   month =       {November},
   publisher = {Elsevier}
+
   publisher =   {Elsevier}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 337: Line 324:
 
<div id="BeckertMostowski2003"><pre>
 
<div id="BeckertMostowski2003"><pre>
 
@InProceedings{BeckertMostowski2003,
 
@InProceedings{BeckertMostowski2003,
   author = {Bernhard Beckert and Wojciech Mostowski},
+
   author =       {Bernhard Beckert and Wojciech Mostowski},
   title = {A Program Logic for Handling {Java Card}'s Transaction Mechanism},
+
   title =       {A Program Logic for Handling {Java Card}'s Transaction Mechanism},
   booktitle = {Proceedings,
+
   booktitle =   {Proceedings, Fundamental Approaches to Software Engineering (FASE) Conference 2003, Warsaw, Poland},  
                  Fundamental Approaches to Software Engineering (FASE)
+
                  Conference 2003, Warsaw, Poland},  
+
 
   pages =        {246--260},
 
   pages =        {246--260},
   year = 2003,
+
   year =         2003,
   editor = {Mauro Pezz\`{e}},
+
   editor =       {Mauro Pezz\`{e}},
   volume = 2621,
+
   volume =       {2621},
   series = {LNCS},
+
   series =       {LNCS},
 
   month =        {April},
 
   month =        {April},
 
   publisher =    {Springer}
 
   publisher =    {Springer}
Line 354: Line 339:
 
<div id="KeYFASE2002"><pre>
 
<div id="KeYFASE2002"><pre>
 
@InProceedings{KeYFASE2002,
 
@InProceedings{KeYFASE2002,
   author =   {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert and Martin Giese and
+
   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},
+
                  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},
+
   title =       {The {KeY} System: {I}ntegrating Object-Oriented Design and Formal Methods},
   booktitle = {Proceedings,
+
   booktitle =   {Proceedings, Fundamental Approaches to Software Engineering (FASE) Conference, Grenoble, France},
              Fundamental Approaches to Software Engineering (FASE) Conference},
+
   editor =       {Ralf-Detlef Kutsche and Herbert Weber},
   editor =   {Ralf-Detlef Kutsche and Herbert Weber},
+
   pages =       {327--330},
   pages =     {327--330},
+
   month =       {April},
  address =  {Grenoble, France},
+
   publisher =   {Springer},
   month =     {April},
+
   series =       {LNCS},
   publisher = {Springer},
+
   volume =       {2306},
   series =   {LNCS},
+
   year =         2002
   volume =   2306,
+
   year =     2002,
+
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 378: Line 361:
 
   month =        {March},
 
   month =        {March},
 
   editor =      {T. Clarke and A. Evans and K. Lano},
 
   editor =      {T. Clarke and A. Evans and K. Lano},
   note =        {Available from \url{http://www.cs.chalmers.se/~woj/papers/room2002.ps.gz}}       
+
   note =        {Available on-line}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 384: Line 367:
 
<div id="JanowskiMostowski2000"><pre>
 
<div id="JanowskiMostowski2000"><pre>
 
@InProceedings{JanowskiMostowski2000,
 
@InProceedings{JanowskiMostowski2000,
   author = {Tomasz Janowski and Wojciech Mostowski},
+
   author =       {Tomasz Janowski and Wojciech Mostowski},
   title = {Fail-Stop Components by Pattern Matching},
+
   title =       {Fail-Stop Components by Pattern Matching},
   booktitle = {Formal Methods for Open Object-Based Distributed Systems},
+
   booktitle =   {Formal Methods for Open Object-Based Distributed Systems},
   editor = {Scott F. Smith and Carolyn L. Talcott},
+
   editor =       {Scott F. Smith and Carolyn L. Talcott},
   year = 2000,
+
   year =         2000,
   publisher = {Kluwer Academic Publishers},
+
   publisher =   {Kluwer Academic Publishers},
 
   month =        {September}
 
   month =        {September}
 
}
 
}
Line 396: Line 379:
 
<div id="BJMPV-STWICT2010"><pre>
 
<div id="BJMPV-STWICT2010"><pre>
 
@Misc{BJMPV-STWICT2010,
 
@Misc{BJMPV-STWICT2010,
   author = {Lejla Batina and Bart Jacobs and Wojciech Mostowski and
+
   author =       {Lejla Batina and Bart Jacobs and Wojciech Mostowski and Erik Poll and Pim Vullers},
                  Erik Poll and Pim Vullers},
+
   title =       {{Security and Privacy of Smartcard-based e-Identity}},
   title = {{Security and Privacy of Smartcard-based e-Identity}},
+
 
   howpublished = {Poster Presentation at STW.ICT 2010 Conference, Veldhoven, the Netherlands},
 
   howpublished = {Poster Presentation at STW.ICT 2010 Conference, Veldhoven, the Netherlands},
 
   month =        {November},
 
   month =        {November},
 
   year =        2010,
 
   year =        2010,
   note = {Available at \url{http://www.cs.ru.nl/~woj/papers/download/stwict2010.pdf}}
+
   note =         {Available on-line}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 408: Line 390:
 
<div id="KeYBook-Chapter9"><pre>
 
<div id="KeYBook-Chapter9"><pre>
 
@InBook{KeYBook-Chapter9,
 
@InBook{KeYBook-Chapter9,
   author = {Wojciech Mostowski},
+
   author =       {Wojciech Mostowski},
   editor = {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
+
   editor =       {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
   title = {Verification of Object-Oriented Software: {The} {KeY} Approach},
+
   title =       {Verification of Object-Oriented Software: {The} {KeY} Approach},
 
   chapter =      {9. From Sequential {Java} to {Java Card}},
 
   chapter =      {9. From Sequential {Java} to {Java Card}},
   publisher = {Springer},
+
   publisher =   {Springer},
 
   series =      {LNAI},
 
   series =      {LNAI},
 
   volume =      4334,
 
   volume =      4334,
Line 422: Line 404:
 
<div id="KeYBook-Chapter14"><pre>
 
<div id="KeYBook-Chapter14"><pre>
 
@InBook{KeYBook-Chapter14,
 
@InBook{KeYBook-Chapter14,
   author = {Wojciech Mostowski},
+
   author =       {Wojciech Mostowski},
   editor = {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
+
   editor =       {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
   title = {Verification of Object-Oriented Software: {The} {KeY} Approach},
+
   title =       {Verification of Object-Oriented Software: {The} {KeY} Approach},
   chapter = {14. The {Demoney} Case Study},
+
   chapter =     {14. The {Demoney} Case Study},
   publisher = {Springer},
+
   publisher =   {Springer},
 
   series =      {LNAI},
 
   series =      {LNAI},
 
   volume =      4334,
 
   volume =      4334,
Line 437: Line 419:
 
@InBook{KeYBook-AppendixB,
 
@InBook{KeYBook-AppendixB,
 
   author =      {Wojciech Mostowski},
 
   author =      {Wojciech Mostowski},
   editor = {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
+
   editor =       {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
   title = {Verification of Object-Oriented Software: {The} {KeY} Approach},
+
   title =       {Verification of Object-Oriented Software: {The} {KeY} Approach},
   chapter = {Appendix B. The {KeY} Syntax},
+
   chapter =     {Appendix B. The {KeY} Syntax},
 
   series =      {LNAI},
 
   series =      {LNAI},
 
   volume =      4334,
 
   volume =      4334,
Line 462: Line 444:
 
<div id="MostowskiPhD2005"><pre>
 
<div id="MostowskiPhD2005"><pre>
 
@PhdThesis{MostowskiPhD2005,
 
@PhdThesis{MostowskiPhD2005,
   author =     {Wojciech Mostowski},
+
   author =       {Wojciech Mostowski},
   title =     {Formal Development of Safe and Secure {Java Card} Applets},
+
   title =       {Formal Development of Safe and Secure {Java Card} Applets},
   school =     {Chalmers University of Technology, Department of Computer Science and Engineering,
+
   school =       {Chalmers University of Technology, Department of Computer Science and Engineering, G\"oteborg, Sweden},
                G\"oteborg, Sweden},
+
   year =         2005,
   year =       2005,
+
   month =       {February},
   month =     {February},
+
   isbn =         {91-7291-575-7}
   isbn =       {91-7291-575-7}
+
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 485: Line 466:
  
 
<div id="Mostowski2013-TR"><pre>
 
<div id="Mostowski2013-TR"><pre>
@techreport{Mostowski2013-TR,
+
@TechReport{Mostowski2013-TR,
   author =     {Afshin Amighi and Stefan Blom and Marieke Huisman and Wojciech Mostowski and Marina Zaharieva-Stojanovski},
+
   author =       {Afshin Amighi and Stefan Blom and Marieke Huisman and Wojciech Mostowski and Marina Zaharieva-Stojanovski},
   title =       {Formal Specifications for {Java}'s Synchronisation Classes},
+
   title =       {Formal Specifications for {Java}'s Synchronisation Classes},
   number =     {TR--CTIT--13--18},
+
   number =       {TR--CTIT--13--18},
   institution = {University of Twente},
+
   institution = {University of Twente},
   year =       2013,
+
   year =         2013,
 
}
 
}
 
</pre></div>
 
</pre></div>
  
 
<div id="2010-Mostowski-ElectronicNutshell"><pre>
 
<div id="2010-Mostowski-ElectronicNutshell"><pre>
@techreport{2010-Mostowski-ElectronicNutshell,
+
@TechReport{2010-Mostowski-ElectronicNutshell,
 
   author =      {{Mostowski}, Wojciech and {Poll}, Erik},
 
   author =      {{Mostowski}, Wojciech and {Poll}, Erik},
 
   title =        {{Electronic Passports in a Nutshell}},
 
   title =        {{Electronic Passports in a Nutshell}},
Line 502: Line 483:
 
   institution =  {Radboud University Nijmegen},
 
   institution =  {Radboud University Nijmegen},
 
   year =        {2010},
 
   year =        {2010},
   note =        {Available at \url{https://pms.cs.ru.nl/iris-diglib/src/getContent.php?id=2010-Mostowski-ElectronicNutshell}},
+
   note =        {Available at \url{https://pms.cs.ru.nl/iris-diglib/src/getContent.php?id=2010-Mostowski-ElectronicNutshell}}
  class =        {Report}
+
 
}
 
}
 
</pre></div>
 
</pre></div>
  
 
<div id="2009-Mostowski-MidletGraphs"><pre>
 
<div id="2009-Mostowski-MidletGraphs"><pre>
@techreport{2009-Mostowski-MidletGraphs,
+
@TechReport{2009-Mostowski-MidletGraphs,
   author =       {{Mostowski}, Wojciech and {Poll}, Erik},
+
   author =       {{Mostowski}, Wojciech and {Poll}, Erik},
   title =         {{Midlet Navigation Graphs in JML}},
+
   title =       {{Midlet Navigation Graphs in JML}},
   number =       {ICIS--R09004},
+
   number =       {ICIS--R09004},
   month =         {August},
+
   month =       {August},
   institution =   {Radboud University Nijmegen},
+
   institution = {Radboud University Nijmegen},
   year =         {2009},
+
   year =         2009,
   note =         {Available at \url{https://pms.cs.ru.nl/iris-diglib/src/getContent.php?id=2009-Mostowski-MidletGraphs}},
+
   note =         {Available at \url{https://pms.cs.ru.nl/iris-diglib/src/getContent.php?id=2009-Mostowski-MidletGraphs}}
  class =        {Report}
+
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 522: Line 501:
 
<div id="MostowskiPoll2007"><pre>
 
<div id="MostowskiPoll2007"><pre>
 
@techreport{MostowskiPoll2007,
 
@techreport{MostowskiPoll2007,
   author = {{Mostowski}, Wojciech and {Poll}, Erik},
+
   author =       {{Mostowski}, Wojciech and {Poll}, Erik},
   title = {{Testing the Java Card Applet Firewall}},
+
   title =       {{Testing the Java Card Applet Firewall}},
   number = {ICIS--R07029},
+
   number =       {ICIS--R07029},
   month = {December},
+
   month =       {December},
   institution = {Radboud University Nijmegen},
+
   institution = {Radboud University Nijmegen},
   year = {2007},
+
   year =         2007,
  class = {Report},
+
   note =         {Available on-line}
   note                 = {Available at \url{https://pms.cs.ru.nl/iris-diglib/src/icis_tech_reports.php}}
+
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 535: Line 513:
 
<div id="STReport2007"><pre>
 
<div id="STReport2007"><pre>
 
@TechReport{STReport2007,
 
@TechReport{STReport2007,
   author = {Wojciech Mostowski and Jing Pan and Srikanth Akkiraju and Erik de Vink
+
   author =       {Wojciech Mostowski and Jing Pan and Srikanth Akkiraju and Erik de Vink and Erik Poll and Jerry den Hartog},
                  and Erik Poll and Jerry den Hartog},
+
   title =       {A Comparison of {Java Cards}: {State}-of-Affairs 2006},
   title = {A Comparison of {Java Cards}: {State}-of-Affairs 2006},
+
 
   institution =  {Technical University Eindhoven},
 
   institution =  {Technical University Eindhoven},
   year = 2007,
+
   year =         2007,
   number = {CS-Report CSR 07-06},
+
   number =       {CS-Report CSR 07-06},
 
   note =        {Available on request}
 
   note =        {Available on request}
 
}
 
}
Line 547: Line 524:
 
<div id="Mostowski2004"><pre>
 
<div id="Mostowski2004"><pre>
 
@TechReport{Mostowski2004,
 
@TechReport{Mostowski2004,
   author = {Wojciech Mostowski},
+
   author =       {Wojciech Mostowski},
   title = {Formalisation and Verification of {Java Card} Security
+
   title =       {Formalisation and Verification of {Java Card} Security Properties in {Dynamic Logic}},
                  Properties in {Dynamic Logic}},
+
 
   institution =  {Department of Computing Science, Chalmers University of Technology, G\"{o}teborg, Sweden},
 
   institution =  {Department of Computing Science, Chalmers University of Technology, G\"{o}teborg, Sweden},
   year = 2004,
+
   year =         2004,
 
   month =        {October},
 
   month =        {October},
   number = {2004--08}
+
   number =       {2004--08}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 559: Line 535:
 
<div id="Mostowski-JCtools"><pre>
 
<div id="Mostowski-JCtools"><pre>
 
@Unpublished{Mostowski-JCtools,
 
@Unpublished{Mostowski-JCtools,
   author = {Wojciech Mostowski},
+
   author =       {Wojciech Mostowski},
   title = {{Java Card} Tools for {Together Control Center}},
+
   title =       {{Java Card} Tools for {Together Control Center}},
   note = {\url{http://www.cs.chalmers.se/~woj/papers/jctools.pdf}}
+
   note =         {Available on-line}
 
}
 
}
 
</pre></div>
 
</pre></div>
Line 567: Line 543:
 
<div id="KeYTool2003"><pre>
 
<div id="KeYTool2003"><pre>
 
@TechReport{KeYTool2003,
 
@TechReport{KeYTool2003,
   author = {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert and Richard Bubel and Martin Giese  
+
   author =     {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert and Richard Bubel and Martin Giese and Reiner H\"{a}hnle
                  and Reiner H\"{a}hnle and Wolfram Menzel and Wojciech Mostowski and Andreas Roth and  
+
                and Wolfram Menzel and Wojciech Mostowski and Andreas Roth and Steffen Schlager and Peter H. Schmitt},
                  Steffen Schlager and Peter H. Schmitt},
+
   title =       {The {KeY} Tool},
   title = {The {KeY} Tool},
+
   institution = {Department of Computing Science, Chalmers University of Technology, G\"{o}teborg, Sweden},
   institution = {Department of Computing Science, Chalmers University of Technology, G\"{o}teborg, Sweden},
+
   year =       2003,
   year = 2003,
+
   number =     {2003--05}
   number = {2003--05}
+
 
}
 
}
 
</pre></div>
 
</pre></div>

Revision as of 19:01, 17 May 2015

@Article{Mostowski-VerifyThis2012,
  author =       {Daniel Bruns and Wojciech Mostowski and Mattias Ulbrich},
  title =        {Implementation-level Verification of Algorithms with {KeY}},
  journal =      {Software Tools for Technology Transfer},
  year =         2013,
  publisher =    {Springer},
  note =         {On-line first, to appear.}
}
@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},
  publisher =    {Springer}
}
@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)},
  note =         {To appear}
}
@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)},
  editor =       {Dimitra Giannakopoulou and Daniel Kroening},
  pages =        {1--17},
  series =       {LNCS},
  volume =       {8471},
  year =         2014,
  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},
  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},
  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},
  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},
  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},
  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},
  year =         2010,
  series =       {LNCS},
  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},
  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},
  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},
  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},
  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},
  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},
  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},
  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},
  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},
  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}
}
@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},
  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},
  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},
  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}
}
@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{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,
  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,
  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{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}
}