@techreport{AhrendtBaarEA00,
author = {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert
and Martin Giese and Elmar Habermalz and Reiner
H\"ahnle and Wolfram Menzel and Peter H. Schmitt},
title = {The {KeY} Approach: {I}ntegrating Object Oriented
Design and Formal Verification},
institution = {University of Karlsruhe, Department of Computer Science},
type = {Technical Report},
number = {2000/4},
month = jan,
year = {2000}
}
@inproceedings{AhrendtBHRS06,
author = {Wolfgang Ahrendt and
Bernhard Beckert and
Reiner H{\"a}hnle and
Philipp R{\"u}mmer and
Peter H. Schmitt},
title = {Verifying Object-Oriented Programs with KeY: A Tutorial},
booktitle = {Formal Methods for Components and Objects, 5th International
Symposium, FMCO 2006, Amsterdam, The Netherlands, November
7-10, 2006, Revised Lectures},
editor = {Frank S. de Boer and
Marcello M. Bonsangue and
Susanne Graf and
Willem P. de Roever},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4709},
year = {2006},
pages = {70-101},
ee = {http://dx.doi.org/10.1007/978-3-540-74792-5_4},
isbn = {978-3-540-74791-8}
}
@proceedings{AMAI95,
editor = {Victor Marek and Peter H.~Schmitt},
series = {Annals of Mathematics and Artificial Intelligence},
title = {Special issue on: Non-classical logics and computer science},
volume = {12, Nos. 3,4},
year = {1994}
}
@techreport{asm98,
author = {Uwe Gl\"{a}sser and Peter H. Schmitt},
address = {Magdeburg, Germany, September 21-22},
institution = {Otto von Guericke University Magdeburg},
title = {Proceedings of the Fifth International
Workshop on Abstract State Machines},
year = {1998}
}
@techreport{BaarBS01TR,
author = {Thomas Baar and
Bernhard Beckert and
Peter H. Schmitt},
title = {An extension of dynamic logic for modelling
{OCL}'s (at)pre operator},
institution = {Fakultät für Informatik, Universität Karlsruhe},
year = {2001},
type = {Interner Bericht},
number = {2001-7},
annote = {final version appeared in LNCS Vol. 2244}
}
@inproceedings{BaarCCGHPSW05,
author = {Thomas Baar and
Dan Chiorean and
Alexandre L. Correa and
Martin Gogolla and
Heinrich Hu{\ss}mann and
Octavian Patrascoiu and
Peter H. Schmitt and
Jos Warmer},
title = {Tool Support for OCL and Related Formalisms - Needs and
Trends},
booktitle = {Satellite Events at the MoDELS 2005 Conference, MoDELS 2005
International Workshops, Doctoral Symposium, Educators Symposium,
Montego Bay, Jamaica, October 2-7, 2005, Revised Selected
Papers},
editor = {Jean-Michel Bruel},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3844},
year = {2005},
pages = {1-9},
isbn = {3-540-31780-5},
ee = {http://dx.doi.org/10.1007/11663430_1}
}
@techreport{BeckertBrunsKlebanovEtAl13,
author = {Bernhard Beckert and Daniel Bruns and Vladimir Klebanov
and Christoph Scheben and Peter H. Schmitt and Mattias
Ulbrich },
title = {Information Flow in Object-Oriented Software -- Extended
Version --},
year = 2013,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2013-14},
series = {Karlsruhe Reports in Informatics},
issn = {2190-4782},
license = {http://creativecommons.org/licenses/by-nc-nd/3.0/},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000037606},
urn = {urn:nbn:de:swb:90-376067},
annote = {Revised and extended version of
\cite{BeckertBrunsKlebanovEtAl13b}.}
}
@inproceedings{BeckertGHKRSS07,
author = {Bernhard Beckert and
Martin Giese and
Reiner H{\"a}hnle and
Vladimir Klebanov and
Philipp R{\"u}mmer and
Steffen Schlager and
Peter H. Schmitt},
title = {The KeY system 1.0 (Deduction Component)},
booktitle = {CADE},
editor = {Frank Pfenning},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4603},
year = {2007},
pages = {379-384},
isbn = {978-3-540-73594-6},
ee = {http://dx.doi.org/10.1007/978-3-540-73595-3_26}
}
@incollection{BeckertKS02,
author = {Bernhard Beckert and
Uwe Keller and
Peter H. Schmitt},
title = {Translating the object constraint language
into first-order predicate logic},
booktitle = {Proceedings of {VERIFY} Workshop at
Federated Logic Conferences ({FL}o{C}), Copenhagen, Denmark },
editor = { Serge Autexier},
year = 2002,
pages = {113-123},
number = {},
series = {}
}
@techreport{BeckertKSST12,
author = {Bernhard Beckert and Daniel Bruns and Ralf K\"{u}sters and Christoph Scheben and
Peter H. Schmitt and Tomasz Truderung, Tomasz},
title = {The KeY Approach for the Cryptographic Verification of JAVA Programs: A Case Study},
year = 2012,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2012-8},
series = {Karlsruhe Reports in Informatics},
issn = {2190-4782},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000027497 },
urn = {urn:nbn:de:swb:90-274973 }
}
@techreport{BeckertSS05TR,
author = {Bernhard Beckert and
Steffen Schlager and
Peter H. Schmitt},
title = {An Improved Rule for While Loops in Deductive Program Verification},
year = 2005,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2005-26},
series = {Interner Bericht. Fakultät für Informatik},
issn = {1432-7864},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000004124 },
urn = {urn:nbn:de:swb:90-41244 },
annotate = {final version published in LNCS Vol 3785}
}
@inproceedings{BezivinBGGHHPSW04,
author = {Jean B{\'e}zivin and
Thomas Baar and
Tracy Gardner and
Martin Gogolla and
Reiner H{\"a}hnle and
Heinrich Hu{\ss}mann and
Octavian Patrascoiu and
Peter H. Schmitt and
Jos Warmer},
title = {OCL and Model Driven Engineering},
editor = {Nuno Jardim Nunes and
Bran Selic and
Alberto Rodrigues da Silva and
Jos{\'e} Ambrosio Toval {\'A}lvarez},
booktitle = {UML Modeling Languages and Applications, UML
2004 Satellite Activities, Lisbon, Portugal, October 11-15,
2004, Revised Selected Papers},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3297},
year = {2004},
pages = {67-75},
isbn = {3-540-25081-6},
ee = {http://dx.doi.org/10.1007/978-3-540-31797-5_8}
}
@techreport{cade96,
author = {(Eds.) Gerard Allwein and Joachim Posegga and
Peter H. Schmitt},
institution = {Rutgers University, New Brunswick},
title = {Visual Reasoning},
type = {Workshop at {CADE} 13},
year = {1996}
}
@techreport{cadews98,
author = {Nikolaj~S.~Bj{\o}rner and Reiner
H\"{a}hnle and Wolfram Menzel and Wofgang Reif and
Peter~H.~Schmitt},
address = {Lindau, Germany, July 5-10},
institution = {Workshop at the 15th International
Conference on Automated Deduction},
title = {Integration of Deductive Systems},
year = {1998}
}
@techreport{cost97,
author = {(Eds.) Peter H. Schmitt and Daniele Mundici and
Lotfi Zadeh},
institution = {IBFI, Schloss Dagstuhl},
title = {Multiple-valued Logic},
type = {Dagstuhl-Seminar-Report},
number = {194},
year = {1997}
}
@techreport{EngelRSW09,
author = {Christian Engel and
Andreas Roth and
Peter H. Schmitt and
Benjamin Wei{\ss}},
title = {Verification of Modifies Clauses in Dynamic Logic with
Non-rigid Functions},
year = 2009,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2009-9},
series = {Interner Bericht. Fakultät für Informatik},
issn = {1432-7864},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000011471 },
urn = {urn:nbn:de:swb:90-114717}
}
@incollection{EngelSchmitt10,
author = {Christian Engel and Peter H. Schmitt},
title = {A Formalization of the {RTSJ} Scoped Memory Model in Dynamic Logic },
booktitle = {Formal Verification of Object-Oriented Software},
editor = {Bernhard Beckert and Claude March\'{e}},
pages = {298 - 313 },
year = 2010,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2010-13},
series = {Karlsruhe Reports in Informatics},
issn = {2190-4782},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019095 },
urn = {urn:nbn:de:swb:90-190956 }
}
@article{GanzingerSS98,
author = {Harald Ganzinger and
J{\"o}rg H. Siekmann and
Peter H. Schmitt},
title = {Wohin geht die automatische Deduktion?},
journal = {KI},
volume = {12},
number = {4},
year = {1998},
pages = {33-37},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{GlasserS98,
author = {Uwe Gl{\"a}sser and
Peter H. Schmitt},
title = {Workshop: Abstract State Machines},
booktitle = {GI Jahrestagung},
year = {1998},
pages = {381-382},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{HahnleMS98,
author = {Reiner H{\"a}hnle and
Wolfram Menzel and
Peter H. Schmitt},
title = {Integrierter {D}eduktiver {S}oftware-{E}ntwurf},
journal = {KI},
volume = {12},
number = {4},
year = {1998},
pages = {40-41},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{HahnleMSR99,
author = {Reiner H{\"a}hnle and
Wolfram Menzel and
Peter H. Schmitt and
Wolfgang Reif},
title = {J.UCS Special Issue on Integration of Deduction Systems},
journal = {J. UCS},
volume = {5},
number = {3},
year = {1999},
ee = {http://www.jucs.org/jucs_5_3/j_ucs_special_issue},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{HMRS99E,
author = {Reiner H\"{a}hnle and Wolfram Menzel and Wolfgang Reif and
Peter H. Schmitt{, editors}},
title = {Special Issue on Integration of Deduction Systems},
journal = {Journal of Universal Computer Science},
publisher = {Springer},
volume = {5},
number = {3},
pages = {50--51},
year = {1999}
}
@article{IWBS113,
author = {Christoph Beierle and
Ulrich Hedtst{\"u}ck and
Udo Pletat and
Peter H. Schmitt and
J{\"o}rg H. Siekmann},
title = {An Order-Sorted Logic for Knowledge Representation Systems},
journal = {IWBS Report},
publisher = {IBM Germany Science Center, Institute for Knowledge Based
Systems},
volume = {113},
year = {1990},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{IWBS144,
author = {Egon B{\"o}rger and
Peter H. Schmitt},
title = {A Formal Operational Semantics for PROLOG III: Using Dynamic
Algebras},
journal = {IWBS Report},
publisher = {IBM Germany Science Center, Institute for Knowledge Based
Systems},
volume = {144},
year = {1990},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{IWBS95,
author = {Ulrich Hedtst{\"u}ck and
Peter H. Schmitt},
title = {A Calculus for Order-Sorted Predicate Logic with Sort Literals},
journal = {IWBS Report},
publisher = {IBM Germany Science Center, Institute for Knowledge Based
Systems},
volume = {95},
year = {1989},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{KISchmitt98,
author = {Peter H. Schmitt},
title = {Serviceteil {D}eduktion und {A}nwendungen},
journal = {KI},
volume = {12},
number = {4},
year = {1998},
pages = {64},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{LILOG1a,
author = {Otthein Herzog and
Claus-Rainer Rollinger and
Peter H. Schmitt and
Petra Steffens and
Rudi Studer and
Birgit Wesche and
Brigitte Bartsch-Sp{\"o}rl and
F. G{\"u}nthner and
Christopher Habel and
Siegfried Kanngie{\ss}er and
Christian Rohrer},
title = {{LILOG} - {L}inguistische und logische {M}ethoden f{\"u}r das
maschinelle {V}erstehen des {D}eutschen - {P}rojektbeschreibung},
journal = {LILOG-Report},
publisher = {IBM Deutschland GmbH},
volume = {1},
year = {1986},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@techreport{NanchenSSS03,
author = {Stanislas Nanchen and
Hubert Schmid and
Peter H. Schmitt and
Robert F. St{\"a}rk},
title = {The {ASMKeY} Prover},
institution = {Department of Computer Science, ETH Z{\"u}rich and
Institute for Logic,\ Complexity and Deduction Systems, Universit\"{a}t Karlsruhe},
year = {2004},
number = {436},
url = {http://dx.doi.org/10.3929/ethz-a-006733218}
}
@incollection{PapeSchmitt98,
author = {Christian Pape and
Peter H. Schmitt},
title = {Interaktive {V}isualisierungen in der {L}ehre
der {T}heoretischen {I}nformatik},
booktitle = {Informatik und Ausbildung,
{GI}-{F}achtagung 98, Stuttgart},
publisher = {Springer},
year = {1998},
editor = { Volker Claus},
optvolume = {},
series = {Informatik Aktuell},
isbn = {3-540-64178-5},
pages = { 102-111}
}
@incollection{RothSchmitt04,
author = {Andreas Roth and
Peter H. Schmitt},
title = {Ensuring Invariant Contracts for Modules in Java.},
booktitle = {Proceedings of the {ECOOP} Workshop {FT}f{JP} 2004
Formal Techniques for Java-like Programs, Oslo, Norwegen,},
year = 2004,
pages = {93-102},
number = {NIII-R0426},
series = {Technical Reports University of Nijmegen}
}
@incollection{SchebenSTR11,
author = {Christoph Scheben and Peter H. Schmitt},
title = {Verification of Information Flow Properties of Java Programs without Approximations},
booktitle = {Formal Verification of Object-Oriented Software},
editor = {Bernhard Beckert},
pages = { 324--341},
year = 2011,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2011-26},
series = {Karlsruhe Reports in Informatics},
issn = {2190-4782},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000024811 },
urn = {urn:nbn:de:swb:90-248110},
annote = {final version published in FoVeOOS proceedings LCNS Vol.7421}
}
@inproceedings{Schmitt01,
author = {Peter H. Schmitt},
title = {Iterate Logic},
editor = {Reinhard Kahle and
Peter Schroeder-Heister and
Robert F. St{\"a}rk},
booktitle = {Proof Theory in Computer Science, International Seminar,
PTCS 2001, Dagstuhl Castle, Germany, October 7-12, 2001,
Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2183},
year = {2001},
pages = {191-201},
isbn = {3-540-42752-X},
ee = {http://dx.doi.org/10.1007/3-540-45504-3_12}
}
@incollection{Schmitt01IJCAR,
author = {Peter H. Schmitt},
title = {A model theoretic semantics of {OCL}},
booktitle = {{IJCAR} Workshop on Precise Modelling and Deduction
for Object-Oriented Software, Siena, Italy},
editor = {Bernhard Beckert },
year = {2001},
pages = {43--57},
number = {D II 07/01},
institution = { Dip. di Ingegneria dell'Informazione,
Universita degli Studi di Siena},
series = {Technical reports Universita degli Studi di Siena}
}
@article{Schmitt04,
author = {Peter H. Schmitt},
title = {Preface},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {102},
year = {2004},
pages = {1-2},
ee = {http://dx.doi.org/10.1016/j.entcs.2004.09.008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@techreport{Schmitt11,
author = {Peter H. Schmitt},
title = {A Computer-Assisted Proof of the {B}ellman-{F}ord Lemma},
year = 2011,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2011-15},
series = {Karlsruhe Reports in Informatics},
issn = {2190-4782},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000022513 },
urn = {urn:nbn:de:swb:90-225138}
}
@phdthesis{Schmitt75,
author = {Peter H. Schmitt},
school = {Universit\"{a}t Heidelberg},
title = {Categorical Lattices},
year = {1975}
}
@misc{Schmitt82b,
author = {Peter H. Schmitt},
howpublished = {Habilitationsschrift},
school = {Universit\"{a}t Heidelberg},
title = {Model Theory of Ordered Abelian Groups},
year = {1982}
}
@techreport{Schmitt86,
author = {Peter~H.~Schmitt},
institution = {IBM Deutschland GmbH, Stuttgart},
number = {6},
title = {Mathematical logic and artificial intelligence},
type = {LILOG Report},
year = {1986}
}
@techreport{Schmitt87a,
author = {Peter~H.~Schmitt},
institution = {IBM Heidelberg Scientific Center},
number = {TR--87.09.007},
title = {The {THOT} theorem prover},
type = {Technical Report},
year = {1987}
}
@inproceedings{Schmitt87c,
author = {Peter~H. Schmitt},
booktitle = {PROLOG und PROLOG-Anwendungen,
Proc. of the 9$^{th}$ 5-Tage-Kurs},
pages = {131 -- 155},
publisher = {Universit\"{a}t Bielefeld, FSP Mathematisierung},
title = {Topics in three-valued logic},
year = {1987}
}
@inproceedings{Schmitt87d,
author = {Peter~H. Schmitt},
booktitle = {Wissensrepr\"{a}sentation in Expertensystemen},
editor = {G.~Rahmstorf},
pages = {79 -- 97},
publisher = {Springer Verlag},
series = {Informatik Fachberichte},
title = {Vererbungshierarchien und {P}r\"{a}dikatenlogik},
volume = {172},
year = {1987}
}
@article{Schmitt92c,
author = {Schmitt Peter H.},
journal = {Journal of Symbolic Logic},
month = sep,
number = {3},
pages = {1138 - 1140},
title = {Review of: Nichtklassische {L}ogik, eine {E}inf\"{u}hrung},
volume = {57},
year = {1992}
}
@techreport{Schmitt94,
author = {Peter~H.~Schmitt},
institution = {Fakult\"{a}t f\"{u}r Informatik, Universit\"{a}t Karlsruhe},
number = {33/94},
title = {Proving {WAM} Compiler Correctness},
type = {Technical Report},
year = {1994}
}
@techreport{Schmitt95,
author = {(Hrsg.) Peter H. Schmitt},
institution = {Universit\"{a}t Karlsruhe},
month = {Mai},
number = {23/95},
title = {Logik in der {I}nformatik. 3. {J}ahrestagung der
{GI}-{F}achgruppe 0.1.6},
type = {Technical Report},
year = {1995}
}
@techreport{SchmittSchmitz88,
author = {Peter~H.~Schmitt and Michael Schmitz},
institution = {IBM Heidelberg Scientific Center},
number = {88.06.005},
title = {Knuth-{B}endix {A}lgorithmen},
type = {Technical Report},
year = {1988}
}
@techreport{SchmittUW10TRa,
author = {Peter H. Schmitt and Mattias Ulbrich and Benjamin Wei{\ss}},
title = {Dynamic Frames in {J}ava Dynamic Logic },
year = 2010,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2010-11},
series = {Karlsruhe Reports in Informatics},
issn = {2190-4782},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000018332 },
urn = {urn:nbn:de:swb:90-183320 },
annotate = {complementary definitions and proof for Karlsruhe Reports in Informatics 2010-13}
}
@incollection{SchmittUW10TR,
author = {Peter H. Schmitt and Mattias Ulbrich and Benjamin Wei{\ss}},
title = {Dynamic Frames in Java Dynamic Logic },
booktitle = {Formal Verification of Object-Oriented Software},
editor = {Bernhard Beckert and Claude March\'{e}},
pages = { 113 - 127 },
year = 2010,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2010-13},
series = {Karlsruhe Reports in Informatics},
issn = {2190-4782},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019092},
urn = {urn:nbn:de:swb:90-190920 },
annotate = {final version published in LNCS Vol. 6528}
}
@techreport{SchmittWerner07,
author = {Peter H. Schmitt and
Frank Werner},
title = {Model Checking for Energy Efficient Scheduling in
Wireless Sensor Networks},
year = 2007,
institution = {Department of Informatics, Karlsruhe Institute of
Technology},
number = {2007-1 },
series = {Interner Bericht. Fakultät für Informatik},
issn = {1432-7864},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000005771 },
urn = {urn:nbn:de:swb:90-57710}
}
This file was generated by bibtex2html 1.98.