Personal tools

Publications

From PUMA Graduiertenkolleg

Jump to: navigation, search

Workshop / Conference Papers 2009

  • Reliable Operating Modes for Distributed Embedded Systems (MOMPES@ICSE 2009)
    Wolfgang Haberl and Stefan Kugele and Uwe Baumgarten
@inproceedings{haberl:kugele:baumgarten:mompes09,
   address   = {Los Alamitos, CA, USA},
   author    = {Wolfgang Haberl and Stefan Kugele and Uwe Baumgarten},
   booktitle = {Proceedings of the ICSE Workshop on Model-based Methodologies for Pervasive and Embedded Software},
   month     = {May},
   pages     = {11--21},
   publisher = {IEEE Computer Society},
   title     = {Reliable Operating Modes for Distributed Embedded Systems},
   volume    = {0},
   year      = {2009}
}
  • Model Analysis via a Translation Schema to Coloured Petri Nets (PNSE 2009)
    Visar Januzaj and Stefan Kugele
@inproceedings{januzaj:kugele:pnse09,
 author    = {Visar Januzaj and Stefan Kugele},
 booktitle = {PNSE'09: Proceedings of the International Workshop on Petri Nets and Software Engineering},
 editor    = {Daniel Moldt},
 month     = {June},
 pages     = {273--292},
 title     = {Model Analysis via a Translation Schema to Coloured Petri Nets},
 year      = {2009}
}
  • Towards Resource Consumption-Aware Programming (ICSEA 2009)
    Andreas Holzer and Visar Januzaj and Stefan Kugele
@inproceedings{holzer:januzaj:kugele:icsea09,
 author    = {Andreas Holzer and
              Visar Januzaj and
              Stefan Kugele},
 title     = {Towards Resource Consumption-Aware Programming},
 booktitle = {The Fourth International Conference on Software Engineering Advances, ICSEA 2009, 20-25 September 2009, Porto, Portugal},
 year      = {2009},
 pages     = {490-493},
 ee        = {http://doi.ieeecomputersociety.org/10.1109/ICSEA.2009.77},
 editor    = {Kenneth Boness and
              Jo{\~a}o M. Fernandes and
              Jon G. Hall and
              Ricardo Jorge Machado and
              Roy Oberhauser},
 publisher = {IEEE Computer Society}

}

@INPROCEEDINGS{HofRod09,
 author    = {Martin Hofmann and Dulma Rodriguez},
 title     = {Efficient Type-Checking for Amortised Heap-Space Analysis},
 booktitle = {CSL: 18th EACSL Annual Conference on Computer Science Logic},
 publisher = {Springer},
 series    = {Lecture Notes in Computer Science},
 volume    = {5771},
 pages     = {317-331},
 editor    = {Erich Gr{\"a}del and Reinhard Kahle},
 year      = {2009}
}
@INPROCEEDINGS{HofRod09,
 author    = {Martin Hofmann and Dulma Rodriguez},
 title     = {Membership Checking in Greatest Fixpoints Revisited},
 booktitle = {FICS: 6th Workshop on Fixed Points in Computer Science, 2009},
 year      = {2009}
}
@inproceedings{GrabowskiB09,
 author    = {Robert Grabowski and Lennart Beringer},
 title     = {Noninterference with Dynamic Security Domains and Policies},
 booktitle = {Advances in Computer Science - ASIAN 2009. Information Security and Privacy},
 publisher = {Springer},
 series    = {Lecture Notes in Computer Science},
 volume    = {5913},
 pages     = {54--68},
 year      = {2009}
}
 @inproceedings{hoelzl2009realineequalities,
   author    = {Johannes H{\"o}lzl},
   title     = {Proving Inequalities over Reals with Computation in {Isabelle/HOL}},
   booktitle = {Proceedings of the {ACM SIGSAM 2009} International Workshop on Programming Languages for Mechanized Mathematics Systems ({PLMMS'09})},
   editor    = {Gabriel Dos Reis and Laurent Th{\'e}ry},
   pages     = {38--45},
   year      = {2009}
 }
 @inproceedings{GS09a,
   address = {Znojmo, Czechia},
   author = {Andreas Gaiser and Stefan Schwoon},
   booktitle = {Proceedings of the 5th Doctoral Workshop on Mathematical and 
                Engineering Methods in Computer Science (MEMICS)},
   editor = {Tom\'a\v{s} Vojnar and Petr Hlin\v{e}n\'y and Vashek Maty\'a\v{s} 
             and David Anto\v{s}},
   month = {November},
   pages = {69--77},
   title = {Comparison of Algorithms for Checking Emptiness on {B\"uchi} 
            Automata},
   year = {2009}
  }
 @inproceedings{Berghofer-Bulwahn-Haftmann:2009:inductive,
  author =      {Stefan Berghofer and Lukas Bulwahn and Florian Haftmann},
  title =       {Turning inductive into equational specifications},
  booktitle =   {TPHOLs '09: Proceedings of the 22th International Conference on Theorem Proving in Higher Order Logics},
  year =        {2009},
  pages =       {131-146},
  publisher =   {Springer},
  series =      {Lecture Notes in Computer Science},
  volume =      {5674},
  editor =      {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel}
 }
  • Continuous-Time Stochastic Games with Time-Bounded Reachability (FSTTCS)
    Tomas Brazdil and Vojtech Forejt and Jan Krcal and Jan Kretinsky and Antonin Kucera
 @inproceedings{DBLP:conf/fsttcs/BrazdilFKKK09,
 author    = {Tomas Brazdil and
              Vojtech Forejt and
              Jan Krcal and
              Jan Kretinsky and
              Antonin Kucera},
 title     = {Continuous-Time Stochastic Games with Time-Bounded Reachability},
 booktitle = {FSTTCS},
 year      = {2009},
 pages     = {61-72},
 ee        = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2009.2307},
 bibsource = {DBLP, http://dblp.uni-trier.de}
 }

Journal or book articles 2009

@incollection{UrbanN2009,
  author = {Christian Urban and Tobias Nipkow},
  title = {Nominal verification of algorithm {W}},
  booktitle = {From Semantics to Computer Science. Essays in Honour of Gilles Kahn},
  editor = {G. Huet and J.-J. Lévy and G. Plotkin},
  publisher = {Cambridge University Press},
  pages = {363--382},
  year = {2009}
}
@article{ObuaN,
  author = {Steven Obua and Tobias Nipkow},
  title = {Flyspeck {II}: The Basic Linear Programs},
  journal = {Annals of Mathematics and Artificial Intelligence},
  volume = {56},
  year = {2009},
  pages = {245-272}
}

Workshop / Conference Papers 2010

@inproceedings{Flexeder10Interprocedural,
 author = {Andrea Flexeder and Bogdan Mihaila and Michael Petter and Helmut Seidl},
 title = {Interprocedural {C}ontrol {F}low {R}econstruction},
 booktitle = {Asian Symposium on Program Languages and Systems},
 editor = {Kazunori Ueda},
 month = {November},
 year = 2010,
 pages = {188-203},
 series = {Lecture Notes in Computer Science},
 volume = {6461},
 publisher = {Springer},
 doi = {10.1007/978-3-642-17164-2_14},
 address = {Shanghai, China},
}


  • Model-Based Generation of Fault-Tolerant Embedded Systems (ESA 2010)
    Wolfgang Haberl and Stefan Kugele
@inproceedings{haberl:kugele:baumgarten:esa10,
   address   = {Las Vegas, Nevada, USA},
   author    = {Wolfgang Haberl and Stefan Kugele and Uwe Baumgarten},
   booktitle = {Proceedings of the 2010 International Conference on Embedded Systems and Applications, ESA 2010},
   editor    = {Hamid R. Arabnia and Ashu M. G. Solo},
   month     = {July},
   pages     = {136--142},
   publisher = {CSREA Press},
   title     = {Model-Based Generation of Fault-Tolerant Embedded Systems},
   year      = {2010}
}


  • From Model-based Design to Model-based Optimization of Embedded Systems (extended abstract) (YRF@MFCS \& CSL 2010)
    Stefan Kugele
@inproceedings{kugele:yrf10,
 title       = {From Model-based Design to Model-based Optimization of Embedded Systems (extended abstract)},
 author      = {Stefan Kugele},
 booktitle   = {Young Researchers Forum. Satellite workshop of MFCS \& CSL},
 editor      = {Jan Strej\v{c}ek},
 publisher   = {DTU Informatics},
 address     = {Brno, Czech Republic},
 pages       = {43--44},
 year        = {2010},
 isbn        = {978-87-643-0565-4},
 month       = {August}
}


  • Seamless Model-Driven Development Put into Practice (ISoLA 2010)
    Wolfgang Haberl, Markus Herrmannsdoerfer, Stefan Kugele, Michael Tautschnig, and Martin Wechs
@inproceedings{haberl:etal:isola10,
   author = {Wolfgang Haberl and Markus Herrmannsdoerfer and Stefan Kugele and Michael Tautschnig and Martin Wechs},
   booktitle = {Leveraging Applications of Formal Methods, Verification, and Validation},
   editor = {Tiziana Margaria and Bernhard Steffen},
   month = {October},
   pages = {18--32},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Seamless Model-Driven Development Put into Practice},
   volume = {6415},
   year = {2010}
}


  • Timely Time Estimates (ISoLA 2010)
    Andreas Holzer, Visar Januzaj, Stefan Kugele, and Michael Tautschnig
@inproceedings{holzer:etal:isola10,
   author = {Andreas Holzer and Visar Januzaj and Stefan Kugele and Michael Tautschnig},
   booktitle = {Leveraging Applications of Formal Methods, Verification, and Validation},
   editor = {Tiziana Margaria and Bernhard Steffen},
   month = {October},
   pages = {33--46},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Timely Time Estimates},
   volume = {6415},
   year = {2010}
}


  • New Challenges in the Development of Critical Embedded Systems---An "aeromotive" Perspective (ISoLA 2010)
    Visar Januzaj, Stefan Kugele, Boris Langer, Christian Schallhart, and Helmut Veith
@incollection {kugele:etal:isola10,
  author = {Januzaj, Visar and Kugele, Stefan and Langer, Boris and Schallhart, Christian and Veith, Helmut},
  title = {New Challenges in the Development of Critical Embedded Systems---An  "aeromotive" Perspective},
  booktitle = {Leveraging Applications of Formal Methods, Verification, and Validation},
  series = {Lecture Notes in Computer Science},
  editor = {Margaria, Tiziana and Steffen, Bernhard},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {978-3-642-16557-3},
  keyword = {Computer Science},
  pages = {1-2},
  volume = {6415},
  year = {2010}
}


 @inproceedings{ctlstar_ijcar_2010,
   title          = "{A} {D}ecision {P}rocedure for {CTL*} {B}ased on {T}ableaux and {A}utomata",
   author         = "Oliver Friedmann and Martin Lange and Markus Latte",
   booktitle      = "Proceedings of the 2010 International Joint Conference on Automated Reasoning (IJCAR~2010, Edinburgh, United Kingdom)", 
   series         = "Lecture Notes in Computer Science",
   volume         = "6173",
   editor         = "J{\"u}rgen Giesl and Reiner H{\"a}hnle",
   publisher      = "Springer",
   isbn           = "978-3-642-14202-4 (print) and 978-3-642-14203-1 (electronic)",
   pages          = "331--345",
   year           = "2010",
 }
 @inproceedings{ctlstar_clodem_2010,
   title          = "{D}ecision {P}rocedures for {CTL*}",
   author         = "Oliver Friedmann and Markus Latte",
   booktitle      = "Proceedings of the 2010 International Workshop on Comparing Logical Decision Methods (CLoDeM~2010, Edinburgh, United Kingdom)", 
   year           = "2010",
 }
 @inproceedings{nonregctl_lpar_2010,
   title          = "Extended {C}omputation {T}ree {L}ogic",
   author         = "Roland Axelsson and Matthew Hague and Stephan Kreutzer and Martin Lange and Markus Latte",
   booktitle      = "Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR~2010, Yogyakarta, Indonesia)", 
   series         = "Lecture Notes in Computer Science",
   volume         = "6397",
   editor         = "Christian Ferm{\"u}ller and Andrei Voronkov",
   publisher      = "Springer",
   isbn           = "978-3-642-16241-1",
   pages          = "67--81",
   year           = "2010",
 }
@inproceedings{ReussSeidl2010,
 author    = {Reu{\ss}, Andreas and Seidl, Helmut},
 editor    = {Christian G. Ferm{\"u}ller and Andrei Voronkov},
 title     = {Bottom-up Tree Automata with Term Constraints},
 booktitle = {Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
 series    = {Lecture Notes in Computer Science},
 volume    = {6397},
 year      = {2010},
 isbn      = {3-642-16241-X, 978-3-642-16241-1},
 location  = {Yogyakarta, Indonesia},
 pages     = {581--593},
 numpages  = {13},
 url       = {http://portal.acm.org/citation.cfm?id=1928380.1928421},
 acmid     = {1928421},
 publisher = {Springer},
}


 @inproceedings{wollic_2010,
   title          = "{A} {CTL-B}ased {L}ogic for {P}rogram {A}bstractions",
   author         = "Martin Lange and Markus Latte",
   booktitle      = "Proceedings of the 17th Workshop on Logic, Language, Information and Computation (WoLLIC~2010, Bras\'ilia, Brazil)", 
   series         = "Lecture Notes in Computer Science",
   volume         = "6188",
   editor         = "Anuj Dawar and Ruy de Queiroz",
   publisher      = "Springer",
   isbn           = "978-3-642-13823-2 (print) and 978-3-642-13824-9 (electronic)",
   pages          = "19--33",
   year           = "2010",
 }
 @inproceedings{arnold2010verifyingsparsematrixcodes,
   author     = {Arnold, Gilad and H\"{o}lzl, Johannes and K\"{o}ksal, Ali Sinan and Bod\'{\i}k, Rastislav and Sagiv, Mooly},
   title      = {Specifying and verifying sparse matrix codes},
   booktitle  = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming},
   series     = {ICFP '10},
   year       = {2010},
   pages      = {249--260},
   doi        = {10.1145/1863543.1863581}
 }
 @inproceedings{conffmicsKernE10,
   author    = {Christian Kern and Javier Esparza},
   title     = {Automatic Error Correction of Java Programs},
   booktitle = {FMICS},
   year      = {2010},
   pages     = {67-81},
   ee        = {http://dx.doi.org/10.1007/978-3-642-15898-8_5},
   crossref  = {DBLP:conf/fmics/2010},
   bibsource = {DBLP, http://dblp.uni-trier.de}
 }
 @inproceedings{HoffHof10,
   author    = {Jan Hoffmann and
                Martin Hofmann},
   title     = {Amortized Resource Analysis with Polynomial Potential},
   booktitle = {19th Euro. Symp. on Prog. (ESOP'10)},
   year      = {2010},
   pages     = {287-306}
 }
 @inproceedings{HoffHof10Aplas,
   author    = {Jan Hoffmann and
                Martin Hofmann},
  title     = {Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics},
   booktitle = {8th Asian Symp. on Prog. Langs. (APLAS'10)},
   year      = {2010},
 }
 @incollection{BeringerGH10,
   author = {Beringer, Lennart and Grabowski, Robert and Hofmann, Martin},
   title = {Verifying Pointer and String Analyses with Region Type Systems},
   booktitle = {16th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16)},
   editor = {Clarke, Edmund and Voronkov, Andrei},
   pages = {82-102},
   publisher = {Springer Berlin / Heidelberg},
   series = {Lecture Notes in Computer Science},
   volume = {6355},
   year = {2010}
 }
 @inproceedings{
   author    = {B{\"o}hme, Sascha and Nipkow, Tobias},
   title     = {Sledgehammer: Judgement Day},
   booktitle = {Automated Reasoning},
   editor    = {Giesl, J{\"u}rgen and H{\"a}hnle, Reiner},
   series    = {Lecture Notes in Computer Science},
   volume    = {6173},
   year      = 2010,
   pages     = {107-121},
   publisher = {Springer},
   doi       = {http://dx.doi.org/10.1007/978-3-642-14203-1_9}
 }
 @inproceedings{
   author    = {B{\"o}hme, Sascha and Weber, Tjark},
   title     = {Fast {LCF}-Style Proof Reconstruction for {Z3}},
   booktitle = {Interactive Theorem Proving},
   editor    = {Kaufmann, Matt and Paulson, Lawrence},
   series    = {Lecture Notes in Computer Science},
   volume    = 6172,
   year      = 2010,
   pages     = {179--194},
   publisher = {Springer},
   doi       = {http://dx.doi.org/10.1007/978-3-642-14052-5_14}
 }


 @inproceedings{cheng:2011:SynFTESGames,
   author = {Cheng, C.-H. and Luttenberger, M. and Buckl, C. and Knoll, A.},
   title = {{GAVS}: Game Arena Visualization and Synthesis},
   year = {2010},
   volume = {6252},
   series = {LNCS},
   pages = {347--352},
   publisher = {Springer-Verlag}
 }


 @inproceedings{GuptaATVA2010,
   author    = {Ashutosh Gupta and
                Corneliu Popeea and
                Andrey Rybalchenko},
   title     = {Non-monotonic Refinement of Control Abstraction for Concurrent
                Programs},
   booktitle = {ATVA},
   year      = {2010},
   pages     = {188-202},
   publisher = {Springer-Verlag}
 }
 @inproceedings{EGK10:stacs,
   address = {Nancy, France},
   author = {Javier Esparza and Andreas Gaiser and Stefan Kiefer},
   booktitle = {Proceedings of the 27th International Symposium on Theoretical 
               Aspects of Computer Science (STACS)},
   title = {Computing Least Fixed Points of Probabilistic Systems of 
            Polynomials},
   year = {2010}
 }
  • Stochastic Real-Time Games with Qualitative Timed Automata Objectives (CONCUR)
    Tomas Brazdil and Jan Krcal and Jan Kretinsky and Antonin Kucera and Vojtech Rehak
 @inproceedings{DBLP:conf/concur/BrazdilKKKR10,
 author    = {Tomas Brazdil and
              Jan Krcal and
              Jan Kretinsky and
              Antonin Kucera and
              Vojtech Rehak},
 title     = {Stochastic Real-Time Games with Qualitative Timed Automata
              Objectives},
 booktitle = {CONCUR},
 year      = {2010},
 pages     = {207-221},
 ee        = {http://dx.doi.org/10.1007/978-3-642-15375-4_15},
 bibsource = {DBLP, http://dblp.uni-trier.de}
 }
  • Process Algebra for Modal Transition Systemses (MEMICS)
    Nikola Benes and Jan Kretinsky
 @inproceedings{DBLP:conf/memics/BenesK10,
 author    = {Nikola Benes and
              Jan Kretinsky},
 title     = {Process Algebra for Modal Transition Systemses},
 booktitle = {MEMICS},
 year      = {2010},
 pages     = {9-18},
 ee        = {http://dx.doi.org/10.4230/OASIcs.MEMICS.2010.9},
 bibsource = {DBLP, http://dblp.uni-trier.de}
 }
@inproceedings{HaftmannN-FLOPS2010,
 author={Florian Haftmann and Tobias Nipkow},
 title={Code Generation via Higher-Order Rewrite Systems},
 booktitle={Functional and Logic Programming (FLOPS 2010)},
 editor={M. Blume and N. Kobayashi and G. Vidal},
 publisher={Springer},
 series={LNCS},
 volume={6009},
 pages={103-117},
 year=2010
}
@inproceedings{BlanchetteN-ITP10,
 author={Jasmin Christian Blanchette and Tobias Nipkow},
 title={Nitpick: A ounterexample generator for higher-order logic based on a relational model finder},
 booktitle={Interactive Theorem Proving (ITP 2010)},
 editor={M. Kaufmann and L. Paulson},
 publisher=Springer,series=LNCS,volume={6172},pages={131-146},year=2010
}

Journal Articles 2010

 @article{
   author  = {Sascha B{\"o}hme and Micha{\l} Moskal and Wolfram Schulte and
              Burkhart Wolff},
   title   = {{HOL-Boogie} --- {An} Interactive Prover-Backend
              for the {Verifying} {C} {Compiler}},
   journal = {Journal of Automated Reasoning},
   volume  = 44,
   number  = {1--2},
   pages   = {111--144},
   month   = feb,
   year    = 2010,
   doi     = {http://dx.doi.org/10.1007/s10817-009-9142-9},
 }
@article{HalesHHMNOZ-DCG,
  author = {Thomas C. Hales and John Harrison and Sean McLaughlin and Tobias Nipkow and Steven Obua and Roland Zumkeller},
  title = {A Revision of the Proof of the {Kepler} Conjecture},
  journal = {Discrete and Computational Geometry},
  volume = {44},
  pages = {1--34},
  year = 2010
}
@article{Nipkow-JAR10,
 author = {Tobias Nipkow},
 title = {Linear Quantifier Elimination},
 journal = {J. Automated Reasoning},
 volume = {45},
 pages = {189--212},
 year = {2010}
}
@article{
 author = {Franz Baader and Bernhard Beckert and Tobias Nipkow},
 title = {Deduktion: Von der Theorie zur Anwendung},
 journal = {Informatik Spektrum}
 volume = {33},
 pages = {444--451},
 year = {2010}
}

Unrefereed Publications 2010

 @article{nonregctl_arxiv_2010,
   title          = "{E}xtended {C}omputation {T}ree {L}ogic",
   author         = "Roland Axelsson and Matthew Hague and Stephan Kreutzer and Martin Lange and Markus Latte",
   journal        = "arXiv.org", 
   year           = "2010",
   note           = "Available at \url{http://arxiv.org/abs/1006.3709}",
 }
 @techreport{EG10:TechRep,
   author = {Javier Esparza and Andreas Gaiser},
   institution = {Technische Universit{\"a}t M{\"u}nchen, Institut f\"{u}r 
                  Informatik},
   month = {December},
   title = {Probabilistic Abstractions with Arbitrary Domains},
   year = {2010}
 }

Workshop / Conference Papers 2011

@inproceedings{sepp11precise,
 author = {A. Sepp and B. Mihaila and A. Simon},
 title = {Precise {S}tatic {A}nalysis of {B}inaries by {E}xtracting {R}elational {I}nformation},
 booktitle = {Working Conference on Reverse Engineering},
 editor = { M.Pinzger and D. Poshyvanyk},
 month = {October},
 year = 2011,
 publisher = {IEEE Computer Society},
 address = {Limerick, Ireland},
}
 @inproceedings{HAH11,
   author    = {Jan Hoffmann and
                Klaus Aehlig and
                Martin Hofmann},
   title     = {Multivariate Amortized Resource Analysis},
   booktitle = {38th ACM Symp. on Princ. of Prog. Langs. (POPL'11)},
   year      = {2011},
 }
 @inproceedings{hoelzl2011measuretheory,
   author       = {Johannes H{\"o}lzl and Armin Heller},
   title        = {Three Chapters of Measure Theory in {Isabelle/HOL}},
   year         = {2011},
   pages        = {135-151},
   editor       = {Marko C. J. D. van Eekelen and Herman Geuvers and Julien Schmaltz and Freek Wiedijk},
   booktitle    = {Interactive Theorem Proving (ITP 2011)},
   series       = {LNCS},
   volume       = {6898}
 }
 @inproceedings{cheng:2011:SynFTESGames,
   author = {Cheng, C.-H. and Ruess, H. and Buckl, C. and Knoll, A.},
   title = {Synthesis of Fault-Tolerant Embedded Systems using Games: from Theory to Practice},
   year = {2011},
   volume = {6538},
   series = {LNCS},
   pages = {118-133},
   publisher = {Springer-Verlag}
 }
 @inproceedings{cheng:2011:SynFTESGames,
   author = {Cheng, C.-H. and Knoll, A. and Luttenberger, M. and Buckl, C.},
   title = {{GAVS+}: An Open Framework for the Research of Algorithmic Game Solving},
   year = {2011},
   volume = {6605},
   series = {LNCS},
   pages = {258-261},
   publisher = {Springer-Verlag}
 }
 @inproceedings{cheng:vissbip:2011,
   author = {Cheng, C.-H. and Bensalem, S. and Jobstmann, B. and Yan, R-J. and Knoll, A. and Ruess, H.},
   title = {Model Construction and Priority Synthesis for Simple Interaction Systems},
   year = {2011},
   volume = {6617},
   series = {LNCS},
   pages = {466-471},
   publisher = {Springer-Verlag}
 }
 @inproceedings{cheng:hardness:2011,
   author = {Cheng, C.-H. and Jobstmann, B. and Buckl, C. and Knoll, A.},
   title = {On the hardness of priority synthesis},
   year = {2011},
   volume = {6807},
   series = {LNCS},
   publisher = {Springer-Verlag}
 }
 @inproceedings{cheng:algo.priority.syn:2011,
   author = {Cheng, C.-H. and Bensalem, S. and Chen, Y.-F. and Yan, R-J. and Jobstmann, B. and Knoll, A. and Buckl, C. and Ruess, H.},
   title = {Algorithms for synthesizing priorities in component-based systems},
   year = {2011},
   series = {LNCS},
   publisher = {Springer-Verlag},
   note = {to appear}
 }
 @inproceedings{GuptaPOPL2011,
   author    = {Ashutosh Gupta and
                Corneliu Popeea and
                Andrey Rybalchenko},
   title     = {Predicate abstraction and refinement for verifying multi-
                threaded programs},
   booktitle = {POPL},
   year      = {2011},
   pages     = {331-344}
 }
 @inproceedings{GuptaCAV2011,
   author    = {Ashutosh Gupta and
                Corneliu Popeea and
                Andrey Rybalchenko},
   title     = {Threader: A Constraint-Based Verifier for Multi-threaded
                Programs},
   booktitle = {CAV},
   year      = {2011},
   pages     = {412-417}
 }
 @inproceedings{lochbihler11itp,
  title = {Animating the Formalised Semantics of a Java-like Language},
  booktitle = {Interactive Theorem Proving},
  year = {2011},
  publisher = {Springer},
  volume = {6898},
  pages = {216--232},
  author = {Andreas Lochbihler and Lukas Bulwahn},
  editor = {Marko van Eekelen and Herman Geuvers and Julien Schmalz and Freek Wiedijk},
  series = {LNCS}
 }
 @inproceedings{BlanchetteBN-FROCOS11,
  author={Jasmin Christian Blanchette and Lukas Bulwahn and Tobias Nipkow},
  title={Automatic Proof and Disproof in Isabelle/HOL},
  booktitle={Frontiers of Combining Systems (FroCoS 2011)},
  editor={C. Tinelli and V. Sofronie-Stokkermans},
  publisher=Springer,
  series=LNCS,
  volume={6989},
  pages={12-27},
  year=2011
 }
 @inproceedings{bulwahn-2011,
  author =	{Lukas Bulwahn},
  title =	Template:Smart test data generators via logic programming,
  booktitle =	{Technical Communications of the 27th International Conference on Logic Programming (ICLP'11) },
  pages =	{139--150},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  year =	{2011},
  volume =	{11},
  editor =	{John Gallagher and Michael Gelfond},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
 }
 @inproceedings{nonregpdl_gandalf_2011,
   title          = "Separation of Test-Free {P}ropositional {D}ynamic {L}ogics over Context-Free Languages",
   author         = "Markus Latte",
   booktitle      = "Proceedings of the 2nd International Symposium on Games, Automata, Logics and Formal Verification (GandALF~2011, Minori, Italy)",
   year           = "2011",
   pages          = "207--221",
   editor         = "Giovanna D'Agostino and Salvatore La Torre",
   doi            = "10.4204/EPTCS.54.15",
   series         = "EPTCS",
   volume         = "54",
 }
  • Measuring performance of continuous-time stochastic processes using timed automata (HSCC)
    Tomas Brazdil and Jan Krcal and Jan Kretinsky and Antonin Kucera and Vojtech Rehak
 @inproceedings{DBLP:conf/hybrid/BrazdilKKKR11,
 author    = {Tomas Brazdil and
              Jan Krcal and
              Jan Kretinsky and
              Antonin Kucera and
              Vojtech Rehak},
 title     = {Measuring performance of continuous-time stochastic processes
              using timed automata},
 booktitle = {HSCC},
 year      = {2011},
 pages     = {33-42},
 ee        = {http://doi.acm.org/10.1145/1967701.1967709},
 bibsource = {DBLP, http://dblp.uni-trier.de}
 }
  • Fixed-Delay Events in Generalized Semi-Markov Processes Revisited (CONCUR)
    Tomas Brazdil and Jan Krcal and Jan Kretinsky and Antonin Kucera and Vojtech Rehak
 @inproceedings{DBLP:conf/concur/BrazdilKKR11,
 author    = {Tom{a}s Br{a}zdil and
              Jan Krc{a}l and
              Jan Kretinsky and
              Vojtech Reh{a}k},
 title     = {Fixed-Delay Events in Generalized Semi-Markov Processes
              Revisited},
 booktitle = {CONCUR},
 year      = {2011},
 pages     = {140-155},
 ee        = {http://dx.doi.org/10.1007/978-3-642-23217-6_10},
 bibsource = {DBLP, http://dblp.uni-trier.de}
 }
  • Modal Transition Systems: Composition and LTL Model Checking (ATVA)
    Nikola Benes and Ivana Cerna and Jan Kretinsky
@inproceedings{DBLP:conf/atva/BenesCK11,
 author    = {Nikola Benes and
              Ivana Cerna and
              Jan Kretinsky},
 title     = {Modal Transition Systems: Composition and {LTL} Model Checking},
 booktitle = {ATVA},
 year      = {2011},
 pages     = {228-242},
 ee        = {http://dx.doi.org/10.1007/978-3-642-24372-1_17},
 bibsource = {DBLP, http://dblp.uni-trier.de}
 }
  • Parametric Modal Transition Systems (ATVA)
    Nikola Benes and Jan Kretinsky and Kim G. Larsen and Mikael H. Moller and Jiri Srba
 @inproceedings{DBLP:conf/atva/BenesKLMS11,
 author    = {Nikola Benes and
              Jan Kretinsky and
              Kim G. Larsen and
              Mikael H. Moller and
              Jiri Srba},
 title     = {Parametric Modal Transition Systems},
 booktitle = {ATVA},
 year      = {2011},
 pages     = {275-289},
 ee        = {http://dx.doi.org/10.1007/978-3-642-24372-1_20},
 bibsource = {DBLP, http://dblp.uni-trier.de}
 }
  • Model Checking Industrial Robot Systems (SPIN)
    Markus Weißmann and Stefan Bedenk and Christian Buckl and Alois Knoll
 @inproceedings{DBLP:conf/spin/WeissmannBBK11,
 author    = {Markus Wei{\ss}mann and
              Stefan Bedenk and
              Christian Buckl and
              Alois Knoll},
 title     = {Model Checking Industrial Robot Systems},
 booktitle = {SPIN},
 year      = {2011},
 pages     = {161-176},
 ee        = {http://dx.doi.org/10.1007/978-3-642-22306-8_11},
 crossref  = {DBLP:conf/spin/2011},
 bibsource = {DBLP, http://dblp.uni-trier.de}
 }
@inproceedings{Nipkow-ITP11,
 author={Tobias Nipkow},
 title={Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism},
 booktitle={Interactive Theorem Proving (ITP 2011)},
 editor={},
 publisher=Springer,series=LNCS,volume={},pages={},year=2011}
@inproceedings{TraytelBN-APLAS11,
 author={Dmitriy Traytel and Stefan Berghofer and Tobias Nipkow},
 title={Extending Hindley-Milner Type Inference with Coercive Structural Subtyping},
 booktitle={Programming Languages and Systems (APLAS 2011)},
 editor={H. Yang},
 publisher=Springer,series=LNCS,volume={7078},pages={89-104},year=2011
}

Journal Articles 2011

@article{ReussSeidl2011,
 author    = {Helmut Seidl and Andreas Reu{\ss}},
 title     = {Extending {H}1-Clauses with Disequalities},
 journal   = {Information Processing Letters},
 year      = {2011},
 volume    = {111},
 number    = {20},
 pages     = {1007--1013},
 publisher = {Elsevier},
}
@article{Nipkow-IJSI11,
 author={Tobias Nipkow},
 title={Majority Vote Algorithm Revisited Again},
 journal={International Journal of Software and Informatics},
 volume={5},pages={21-28},year={2011}}

Theses 2011

 @phdthesis{Hoffmann11,
 author = {Jan Hoffmann},
 title = {Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis},
 school = {Ludwig-Maximilians-Universi{\"a}t M{\"u}nchen},
 year =  2011
 }


Workshop / Conference Papers 2012

 @inproceedings{NNH13,
   author    = {Neelakantan R. Krishnaswami and
                Nick Benton and
                Jan Hoffmann},
   title     = {Higher-Order Functional Reactive Programming in Bounded Space},
   booktitle = {39th ACM Symp. on Princ. of Prog. Langs. (POPL'12)},
   year      = {2012},
 }
 @inproceedings{hoelzl2012verifyingpctl,
   title      = {Verifying {pCTL} Model Checking},
   author     = {Johannes H{\"o}lzl and Tobias Nipkow},
   year       = {2012},
   booktitle  = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)},
   editor     = {C. Flanagan and B. K{\"o}nig},
   series     = {LNCS}
   volume     = {7214},
   pages      = {347--361}
 }


 @inproceedings{SeidlReuss2012,
   title      = {Extending {H}1-Clauses with Path Disequalities},
   author     = {Helmut Seidl and Andreas Reu{\ss},
   year       = {2012},
   booktitle  = {15th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2012)},
   series     = {LNCS}
 }
 @inproceedings{Bulwahn2012,
   title      = {Smart testing of functional programs in Isabelle},
   author     = {Lukas Bulwahn},
   year       = {2012},
   booktitle  = {18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2012)},
   series     = {LNCS}
 }
 @inproceedings{KernACSD2012,
   author = {Javier Esparza and Christian Kern},
   booktitle = {ACSD},
   note = {To appear},
   title = {Reactive and Proactive Diagnosis of Distributed Systems using Net Unfoldings},
   year = {2012}
  }
 @inproceedings{HofRod2012,
   title      = {Linear constraints over infinite trees},
   author     = {Martin Hofmann and Dulma Rodriguez},
   year       = {2012},
   booktitle  = {18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2012)},
   series     = {LNCS}
 }
  • Dual-Priced Modal Transition Systems with Time Durations (LPAR)
    Nikola Benes and Jan Kretinsky and Kim Guldstrand Larsen and Mikael H. Moller and Jiri Srba
 @inproceedings{DBLP:conf/lpar/BenesKLMS12,
 author    = {Nikola Benes and
              Jan Kretinsky and
              Kim Guldstrand Larsen and
              Mikael H. Moller and
              Jiri Srba},
 title     = {Dual-Priced Modal Transition Systems with Time Durations},
 booktitle = {LPAR},
 year      = {2012},
 pages     = {122-137},
 ee        = {http://dx.doi.org/10.1007/978-3-642-28717-6_12},
 bibsource = {DBLP, http://dblp.uni-trier.de}
 }


 @InProceedings{Dimitrova+Finkbeiner+Kovacs+Rabe+Seidl/12/SecLTL,
    author    = "Rayna Dimitrova and Bernd Finkbeiner and M\'at\'e Kov\'acs and Markus N. Rabe and Helmut Seidl",
    title     = "Model Checking Information Flow in Reactive Systems",
    booktitle = "13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2012)",
    year      = 2012,
    publisher = "Springer Verlag",
    pages     = "169-185"
 }


 @inproceedings{DBLP:conf/essos/KovacsS12,
   author    = {M{\'a}t{\'e} Kov{\'a}cs and Helmut Seidl},
   title     = {Runtime Enforcement of Information Flow Security in Tree Manipulating Processes},
   booktitle = {ESSoS},
   year      = {2012},
   pages     = {46-59},
   ee        = {http://dx.doi.org/10.1007/978-3-642-28166-2_6},
   crossref  = {DBLP:conf/essos/2012},
   bibsource = {DBLP, http://dblp.uni-trier.de}
 }
@inproceedings{Nipkow-ITP12,
  author={Tobias Nipkow},
  title={Abstract Interpretation of Annotated Commands},
  booktitle={Interactive Theorem Proving (ITP 2012)},
  editor={Beringer and Felty},
  publisher=Springer,series=LNCS,volume={},pages={},year=2012}
@inproceedings{immler2012ode,
  author={Fabian Immler and Johannes H{\"o}lzl},
  title={Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL},
  booktitle={Interactive Theorem Proving (ITP 2012)},
  editor={Beringer and Felty},
  publisher=Springer,series=LNCS,volume={},pages={},year=2012}
@inproceedings{hoelzl2012casestudies,
  author={Johannes H{\"o}lzl and Tobias Nipkow},
  title={Interactive verification of Markov chains: Two distributed protocol case studies},
  booktitle={Quantities in Formal Methods (QFM 2012)},year=2012}

Journal Articles 2012

 @article{wollic_jcss_2012,
   title          = "{B}ranching-{T}ime {L}ogics with {P}ath {R}elativisation",
   author         = "Markus Latte and Martin Lange",
   journal        = "Journal of Computer and System Sciences",
   volume         = "WoLLIC'2010 Special Issue",
   editor         = "Anuj Dawar and Ruy de Queiroz",
   year           = "2012",
   note           = "Accepted for publication",
 }