![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Peter H. Schmitt
Person information
- affiliation: Karlsruhe Institute of Technology, Germany
Refine list
![note](https://dblp.uni-trier.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2020
- [c46]Peter H. Schmitt:
Two First-Order Theories of Ordinals. Fields of Logic and Computation III 2020: 247-257 - [p6]Peter H. Schmitt:
A Short History of KeY. 20 Years of KeY 2020: 3-18
2010 – 2019
- 2017
- [c45]Peter H. Schmitt:
A Mechanizable First-Order Theory of Ordinals. TABLEAUX 2017: 331-346 - [c44]Bernhard Beckert
, Jonas Schiffl
, Peter H. Schmitt, Mattias Ulbrich
:
Proving JDK's Dual Pivot Quicksort Correct. VSTTE 2017: 35-48 - 2016
- [p5]Peter H. Schmitt:
First-Order Logic. Deductive Software Verification 2016: 23-47 - [p4]Peter H. Schmitt, Richard Bubel:
Theories. Deductive Software Verification 2016: 149-166 - [p3]Daniel Grahl, Richard Bubel, Wojciech Mostowski, Peter H. Schmitt, Mattias Ulbrich
, Benjamin Weiß:
Modular Specification and Verification. Deductive Software Verification 2016: 289-351 - [p2]Bernhard Beckert
, Reiner Hähnle
, Martin Hentschel, Peter H. Schmitt:
Formal Verification with KeY: A Tutorial. Deductive Software Verification 2016: 541-570 - [e6]Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle
, Peter H. Schmitt, Mattias Ulbrich:
Deductive Software Verification - The KeY Book - From Theory to Practice. Lecture Notes in Computer Science 10001, Springer 2016, ISBN 978-3-319-49811-9 [contents] - 2015
- [j17]Markus Krötzsch
, Sebastian Rudolph
, Peter H. Schmitt:
A closer look at the semantic relationship between Datalog and description logics. Semantic Web 6(1): 63-79 (2015) - [c43]Peter H. Schmitt, Mattias Ulbrich
:
Axiomatization of Typed First-Order Logic. FM 2015: 470-486 - 2014
- [c42]Christoph Scheben, Peter H. Schmitt:
Efficient Self-composition for Weakest Precondition Calculi. FM 2014: 579-594 - [c41]Wolfgang Ahrendt
, Bernhard Beckert
, Daniel Bruns
, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle
, Martin Hentschel, Mihai Herda
, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, Mattias Ulbrich
:
The KeY Platform for Verification and Analysis of Java Programs. VSTTE 2014: 55-71 - 2013
- [c40]Bernhard Beckert, Daniel Bruns
, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, Mattias Ulbrich:
Information Flow in Object-Oriented Software. LOPSTR 2013: 19-37 - [i10]Gary T. Leavens, Peter H. Schmitt, Jooyong Yi:
The Java Modeling Language (JML) (NII Shonan Meeting 2013-3). NII Shonan Meet. Rep. 2013 (2013) - 2011
- [c39]Christoph Scheben, Peter H. Schmitt:
Verification of Information Flow Properties of Java Programs without Approximations. FoVeOOS 2011: 232-249 - 2010
- [c38]Peter H. Schmitt, Mattias Ulbrich, Benjamin Weiß:
Dynamic Frames in Java Dynamic Logic. FoVeOOS 2010: 138-152 - [c37]Markus Krötzsch
, Sebastian Rudolph
, Peter H. Schmitt:
On the Semantic Relationship between Datalog and Description Logics. RR 2010: 88-102
2000 – 2009
- 2009
- [c36]David Faragó, Peter H. Schmitt:
Improving Non-Progress Cycle Checks. SPIN 2009: 50-67 - 2008
- [c35]Richard Bubel, Reiner Hähnle, Peter H. Schmitt:
Specification Predicates with Explicit Dependency Information. VERIFY 2008 - 2007
- [c34]Bernhard Beckert, Martin Giese, Reiner Hähnle
, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt:
The KeY system 1.0 (Deduction Component). CADE 2007: 379-384 - [c33]Peter H. Schmitt, Benjamin Weiß:
Inferring Invariants by Symbolic Execution. VERIFY 2007 - [c32]Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle
, Peter H. Schmitt:
KeY: A Formal Method for Object-Oriented Systems. FMOODS 2007: 32-43 - [c31]Peter H. Schmitt, Isabel Tonin:
Verifying the Mondex Case Study. SEFM 2007: 47-58 - [p1]Andreas Roth, Peter H. Schmitt:
Formal Specification. The KeY Approach 2007: 245-294 - [e5]Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt:
Verification of Object-Oriented Software. The KeY Approach - Foreword by K. Rustan M. Leino. Lecture Notes in Computer Science 4334, Springer 2007, ISBN 978-3-540-68977-5 [contents] - 2006
- [c30]Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle
, Philipp Rümmer, Peter H. Schmitt:
Verifying Object-Oriented Programs with KeY: A Tutorial. FMCO 2006: 70-101 - [c29]Peter H. Schmitt, Isabel Tonin, Claus Wonnemann, Eric Jenn, Stéphane Leriche, James J. Hunt:
A case study of specification and verification using JML in an avionics application. JTRES 2006: 107-116 - [c28]James J. Hunt, Fridtjof Siebert, Peter H. Schmitt, Isabel Tonin:
Provably correct loops bounds for realtime Java programs. JTRES 2006: 162-169 - [c27]Bernhard Beckert, Reiner Hähnle
, Peter H. Schmitt:
Integrating Object-Oriented Design and Deductive Verification of Software. SEFM 2006: 260 - 2005
- [j16]Wolfgang Ahrendt
, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle
, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, Peter H. Schmitt:
The KeY tool. Softw. Syst. Model. 4(1): 32-54 (2005) - [c26]Bernhard Beckert, Steffen Schlager, Peter H. Schmitt:
An Improved Rule for While Loops in Deductive Program Verification. ICFEM 2005: 315-329 - [c25]Thomas Baar, Dan Chiorean, Alexandre L. Correa, Martin Gogolla, Heinrich Hußmann, Octavian Patrascoiu, Peter H. Schmitt, Jos Warmer:
Tool Support for OCL and Related Formalisms - Needs and Trends. MoDELS (Satellite Events) 2005: 1-9 - [c24]Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt:
Verification of JCSP Programs. CPA 2005: 203-218 - 2004
- [c23]Jean Bézivin, Thomas Baar, Tracy Gardner, Martin Gogolla, Reiner Hähnle, Heinrich Hußmann, Octavian Patrascoiu, Peter H. Schmitt, Jos Warmer:
OCL and Model Driven Engineering. UML Satellite Activities 2004: 67-75 - [e4]Peter H. Schmitt:
Proceedings of the Workshop OCL 2.0 - Industry Standard or Scientific Playground?, OCL 2.0, San Francisco, CA, USA, October 21, 2003. Electronic Notes in Theoretical Computer Science 102, Elsevier 2004 [contents] - 2003
- [c22]Bernhard Beckert, Peter H. Schmitt:
Program Verification Using Change Information. SEFM 2003: 91- - [c21]Peter H. Schmitt:
Preface. OCL 2.0 @ UML 2003: 1-2 - 2002
- [c20]Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle
, Wolfram Menzel, Wojciech Mostowski, Peter H. Schmitt:
The KeY System: Integrating Object-Oriented Design and Formal Methods. FASE 2002: 327-330 - 2001
- [c19]Peter H. Schmitt:
Iterate Logic. Proof Theory in Computer Science 2001: 191-201 - [c18]Thomas Baar, Bernhard Beckert, Peter H. Schmitt:
An Extension of Dynamic Logic for Modelling OCL's @pre Operator. Ershov Memorial Conference 2001: 47-54 - 2000
- [j15]Thomas Baar, Reiner Hähnle, Theo Sattler, Peter H. Schmitt:
Entwurfgesteuerte Erzeugung von OCL-Constraints. Softwaretechnik-Trends 20(3) (2000) - [c17]Thomas Baar, Reiner Hähnle
, Theo Sattler, Peter H. Schmitt:
Entwurfsmustergesteuerte Erzeugung von OCL-Constraints. GI Jahrestagung 2000: 389-404 - [c16]Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, Peter H. Schmitt:
The KeY Approach: Integrating Object Oriented Design and Formal Verification. JELIA 2000: 21-36
1990 – 1999
- 1999
- [j14]Reiner Hähnle, Wolfram Menzel, Peter H. Schmitt, Wolfgang Reif:
J.UCS Special Issue on Integration of Deduction Systems. J. Univers. Comput. Sci. 5(3) (1999) - 1998
- [j13]Harald Ganzinger, Jörg H. Siekmann, Peter H. Schmitt:
Wohin geht die automatische Deduktion? Künstliche Intell. 12(4): 33-37 (1998) - [j12]Reiner Hähnle, Wolfram Menzel, Peter H. Schmitt:
Integrierter Deduktiver Software-Entwurf. Künstliche Intell. 12(4): 40-41 (1998) - [j11]Peter H. Schmitt:
Serviceteil Deduktion und Anwendungen. Künstliche Intell. 12(4): 64 (1998) - [c15]Uwe Glässer, Peter H. Schmitt:
Workshop: Abstract State Machines. GI Jahrestagung 1998: 381-382 - [e3]Uwe Glässer, Peter H. Schmitt:
Fifth International Workshop on Abstract State Machines, ASM 1998, Magdeburg, Germany, September 21-22, Proceedings. 1998 [contents] - 1997
- [j10]Egon Börger, Peter H. Schmitt:
A Description of the Tableau Method Using Abstract State Machines. J. Log. Comput. 7(5): 659-681 (1997) - [c14]Peter H. Schmitt, Jean Goubault-Larrecq:
A Tableau System for Linear-TIME Temporal Logic. TACAS 1997: 130-144 - 1996
- [c13]Wolfgang May, Peter H. Schmitt:
A Tableau Calculus for First-Order Branching Time Logic. FAPR 1996: 399-413 - 1995
- [j9]Joachim Posegga, Peter H. Schmitt:
Automated Deduction with Shannon Graphs. J. Log. Comput. 5(6): 697-729 (1995) - 1994
- [j8]Reiner Hähnle
, Peter H. Schmitt:
The Liberalized delta-Rule in Free Variable Semantic Tableaux. J. Autom. Reason. 13(2): 211-221 (1994) - 1993
- [j7]Jürgen Dix, Peter H. Schmitt:
Nichtmonotones Schließen: Wieviel Nichtmonotonie ist nötig? Kognitionswissenschaft 3(1): 53-69 (1993) - [c12]Bernhard Beckert, Reiner Hähnle
, Peter H. Schmitt:
The Even More Liberalized delta-Rule in Free Variable Semantic Tableaux. Kurt Gödel Colloquium 1993: 108-119 - [e2]Gerhard Brewka, Klaus P. Jantke, Peter H. Schmitt:
Nonmonotonic and Inductive Logic, Second International Workshop, Reinhardsbrunn Castle, Germany, December 2-6, 1991, Proceedings. Lecture Notes in Computer Science 659, Springer 1993, ISBN 3-540-56433-0 [contents] - 1992
- [b1]Peter H. Schmitt:
Theorie der logischen Programmierung. Springer 1992, ISBN 3-540-55702-4 - [j6]Christoph Beierle, Ulrich Hedtstück, Udo Pletat, Peter H. Schmitt, Jörg H. Siekmann:
An Order-Sorted Logic for Knowledge Representation Systems. Artif. Intell. 55(2): 149-191 (1992) - 1991
- [c11]Peter H. Schmitt:
Deductive Aspects of Three-Valued Logic. Text Understanding in LILOG 1991: 394-401 - [e1]Jürgen Dix, Klaus P. Jantke, Peter H. Schmitt:
Nonmonotonic and Inductive Logic, 1st International Workshop, Karlsruhe, Germany, December 4-7, 1990, Proceedings. Lecture Notes in Computer Science 543, Springer 1991, ISBN 3-540-54564-6 [contents] - 1990
- [c10]Jürgen Dix, Joachim Posegga, Peter H. Schmitt:
Modal logics for AI planning. Expert Planning Systems 1990: 157-162 - [c9]Egon Börger, Peter H. Schmitt:
A Formal Operational Semantics for Languages of Type Prolog III. CSL 1990: 67-79 - [i9]Peter H. Schmitt, Wolfgang Wernecke:
Tableau Calculus for Order Sorted Logic. IWBS Report 108 (1990) - [i8]Christoph Beierle, Ulrich Hedtstück, Udo Pletat, Peter H. Schmitt, Jörg H. Siekmann:
An Order-Sorted Logic for Knowledge Representation Systems. IWBS Report 113 (1990) - [i7]Egon Börger, Peter H. Schmitt:
A Formal Operational Semantics for PROLOG III: Using Dynamic Algebras. IWBS Report 144 (1990)
1980 – 1989
- 1989
- [c8]Peter H. Schmitt:
Perspectives in Multi-Valued Logic. Natural Language and Logic 1989: 206-220 - [c7]Peter H. Schmitt, Wolfgang Wernecke:
Tableau Calculus for Order Sorted Logic. Sorts and Types in Artificial Intelligence 1989: 49-60 - [c6]Ulrich Hedtstück, Peter H. Schmitt:
A Calculus for Order-Sorted Predicate Logic with Sort Literals. Sorts and Types in Artificial Intelligence 1989: 61-72 - [i6]Ulrich Hedtstück, Peter H. Schmitt:
A Calculus for Order-Sorted Predicate Logic with Sort Literals. IWBS Report 95 (1989) - 1988
- [c5]Christoph Beierle, Jochen Dörre, Udo Pletat, Claus-Rainer Rollinger, Peter H. Schmitt, Rudi Studer:
The Knowledge Representation Language LLILOG. CSL 1988: 14-51 - [i5]Christoph Beierle, Jochen Dörre, Udo Pletat, Claus-Rainer Rollinger, Peter H. Schmitt, Rudi Studer:
The Knowledge Representation Language LLILOG. LILOG-Report 41 (1988) - 1987
- [j5]Peter H. Schmitt:
Eine dreiwertige Logik zur Verarbeitung partieller Information. Inform. Forsch. Entwickl. 2(4): 182-190 (1987) - [c4]Marek Karpinski, Hans Kleine Büning, Peter H. Schmitt:
On the Computational Complexity of Quantified Horn Clauses. CSL 1987: 129-137 - [c3]Peter H. Schmitt:
A Survey of Rewrite Systems. CSL 1987: 235-262 - [c2]Peter H. Schmitt:
Vererbungshierarchien und Prädikatenlogik. Wissensrepräsentation in Expertensystemen 1987: 79-97 - [i4]Peter H. Schmitt:
Mathematical Logic and Artificial Intelligence. LILOG-Report 6 (1987) - [i3]Peter H. Schmitt:
Computational aspects of three-valued logic. LILOG-Report 26 (1987) - [i2]Peter H. Schmitt:
Eine dreiwertige Logik zur Verarbeitung partieller Information. LILOG-Report 27 (1987) - 1986
- [c1]Peter H. Schmitt:
Computational Aspects of Three-Valued Logic. CADE 1986: 190-198 - [i1]Otthein Herzog, Claus-Rainer Rollinger, Peter H. Schmitt, Petra Steffens, Rudi Studer, Birgit Wesche, Brigitte Bartsch-Spörl, F. Günthner, Christopher Habel, Siegfried Kanngießer, Christian Rohrer:
LILOG - Linguistische und logische Methoden für das maschinelle Verstehen des Deutschen - Projektbeschreibung. LILOG-Report 1 (1986) - 1984
- [j4]Peter H. Schmitt:
Diamond Formulas: A Fragment of Dynamic Logic with Recursively Enumerable Validity Problem. Inf. Control. 61(2): 147-158 (1984) - 1983
- [j3]Gregory L. Cherlin, Peter H. Schmitt:
Locally pure topological abelian groups: elementary invariants. Ann. Pure Appl. Log. 24(1): 49-85 (1983) - 1982
- [j2]Peter H. Schmitt:
The Elementary Theory of Torsionfree Abelian Groups With a Predicate Specifying a Subgroup. Math. Log. Q. 28(22-24): 323-329 (1982) - 1981
- [j1]Gregory L. Cherlin, Peter H. Schmitt:
Undecidable Lt Theories of Topological Abelian Groups. J. Symb. Log. 46(4): 761-772 (1981)
Coauthor Index
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-05-02 21:46 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint