@MastersThesis{Sma96-masters,
  author = 	 {Jan-Georg Smaus},
  key =          {Abc},
  title = 	 {Resolution {K}-Transformations},
  school = 	 {Universit{\"a}t des Saarlandes (Max-Planck-Institut f{\"u}r
   Informatik)},
  year = 	 1996
}

@techreport{SHK97-tr,
     author = {Jan-Georg Smaus and Patricia M. Hill and Andy King},
     title = {Domain Construction for Mode Analysis of Typed Logic Programs},
     institution = {Computing Laboratory, University of Kent at Canterbury, United Kingdom},
     year = 1997,
     number = {8-97},
     note = {Early version of~\cite{SHK00-lopstr}}   
}

@InProceedings{SHK97-poster,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Domain Construction for Mode Analysis of Typed Logic Programs},
  booktitle = 	 {Proceedings of the 14th Joint International Conference
                  and Symposium on Logic Programming},
  pages =	 418,
  year =	 1997,
  editor =	 {Lee Naish},
  publisher =	 {MIT Press},
  note =	 {Abstract of Poster Presentation}
}

@TechReport{Sma98-tr,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Well-Terminating, Input-Driven Logic Programs},
  institution =  {University of Kent at Canterbury},
  year = 	 1998,
  number =	 {16-98},
  note = {Early version of~\cite{Sma99-iclp}}
}

@TechReport{SHK98-tr,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Verification of Logic Programs with {\tt block} Declarations
Running in Several Modes},
  institution =  {University of Kent at Canterbury},
  number = {7-98},
  year = 	 1998,
  address =	 {Canterbury, CT2~7NF, United Kingdom},
  month =	 {July},
  note =         {Contains proofs for~\cite{SHK98-plilp,SHK99-lopstr}; see also~\cite{SHK01}}
}

@InProceedings{SHK98-prelopstr,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Preventing Instantiation Errors and Loops
for Logic Programs with Several Modes Using {\tt block} Declarations},
  booktitle = 	 {Pre-Proceedings of the 8th International Workshop on Logic-based Program Synthesis and Transformation},
  year =	 1998,
  editor =	 {Pierre Flener},
  number =       {UMCS-98-6-1},
  publisher =	 {University of Manchester},
  pages =        {72--29},
  note =	 {Extended abstract}
}

@InProceedings{SHK98-plilp,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Termination of Logic Programs with {\tt block} Declarations
Running in Several Modes},
  booktitle = 	 {Proceedings of the 10th Symposium on Programming Language Implementations and Logic Programming},
  year =	 1998,
  editor =	 {Catuscia Palamidessi},
  series =	 {LNCS},
  pages =        {73--88},
  volume =       1490, 
  publisher =	 {Springer-Verlag}
}

@TechReport{KSH98-tr,
  author = 	 {Andy King and Jan-Georg Smaus and Patricia M. Hill},
  title = 	 {Practical
  Dependency Analysis through a ${S}hare$ Quotient},
  institution =  {Computing Laboratory, University of Kent},
  year = 	 1998,
  number =	 {11-98},
  note   =       {Early version of~\cite{KSH99}}
}

@PhdThesis{Sma99-phd,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Modes and Types in Logic Programming},
  school = 	 {University of Kent at Canterbury},
  year = 	 1999
}

@InProceedings{Sma99-iclp,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Proving Termination of Input-Consuming Logic Programs},
  booktitle = 	 {Proceedings of the 16th International Conference
                  on Logic Programming},
  year =	 1999,
  editor =	 {Danny De Schreye},
  pages =        {335--349},
  publisher =	 {MIT Press}
}

@Proceedings{ES99,
  title = 	 {Proceedings of the Workshop on Verification of Logic
                  Programs held at ICLP'99},
  year = 	 1999,
  editor =	 {Sandro Etalle and Jan-Georg Smaus},
  volume =	 "30(1)",
  series =	 {Electronic Notes in Theoretical Computer Science},
  publisher =	 {Elsevier}
}

@InProceedings{SHK99-prelopstr,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Mode Analysis Domains for Typed Logic Programs},
  booktitle = 	 {Pre-Proceedings of the 9th International Workshop on 
                  Logic-based Program Synthesis and Transformation},
  year =	 1999,
  editor =	 {Annalisa Bossi},
  publisher =	 {Universit{\`a} C{\`a} Foscari di Venezia},
  note =	 {Extended abstract},
  pages =        {163--170}
}

@TechReport{Sma99-tr,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Proving Termination of Input-Consuming Logic Programs},
  institution =  {Computing Laboratory, University of Kent at Canterbury, United Kingdom},
  year = 	 1999,
  number =	 {10-99},
  note =         {Long version of~\cite{Sma99-iclp}}
}

@InProceedings{KSH99,
  author = 	 {Andy King and Jan-Georg Smaus and Patricia M. Hill},
  title = 	 {Quotienting $\mathit{Share}$ for Dependency Analysis},
  booktitle = 	 {Proceedings of the European Symposium on Programming},
  year =	 1999,
  volume =       1576,
  pages =        {59--73},
  editor =	 {Doaitse Swierstra}
}

@InProceedings{SHK99-lopstr,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Preventing Instantiation Errors and Loops
for Logic Programs with Multiple Modes Using {\tt block} Declarations},
  booktitle = 	 {Proceedings of the 8th International Workshop on Logic-based Program Synthesis and Transformation},
  year =	 1999,
  pages =        {289--307},
  editor =	 {Pierre Flener},
  publisher =	 {Springer-Verlag},
  volume =       {1559},
  series =       {LNCS}
}

@InProceedings{DS00-jfplc,
  author = 	 {Jan-Georg Smaus and Pierre Deransart},
  title = 	 {Les programmes bien typ{\'e}s ont tout bon},
  booktitle = 	 {Proceedings of Journ{\'e}es Francophones de 
                  Programmation en Logique avec Contraintes},
  pages =	 {49--65},
  year =	 2000,
  editor =	 {Toura{\"\i}vane},
  publisher =	 {Hermes Science Publications}
}

@InProceedings{DS00-vcl,
  author = 	 {Jan-Georg Smaus and Pierre Deransart},
  title = 	 {Well-typed Programs Are not Wrong},
  booktitle = 	 {Verification and Computational Logic Workshop},
  year =	 2000,
  editor =	 {Michael Leuschel et al.},
  publisher =	 {Technical report DSEE-TR-2000-6 of the University of Southampton},
  note =	 {Held within CL'2000}
}

@TechReport{SHK00-tr,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Mode Analysis Domains for Typed Logic Programs},
  institution =  {University of Leeds},
  year = 	 2000,
  number =	 {2000.06},
  note =	 {Long version of~\cite{SHK00-lopstr}}
}

@InProceedings{SHK00-lopstr,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Mode Analysis Domains for Typed Logic Programs},
  booktitle = 	 {Proceedings of the 9th International Workshop on Logic-based Program Synthesis and Transformation},
  year =	 2000,
  editor =	 {Annalisa Bossi},
  series =	 {LNCS},
  pages =        {83--102},
  volume =       1817,
  publish =	 {Springer-Verlag}
}


@InProceedings{SFD00,
  author = 	 {Jan-Georg Smaus and Fran{\c c}ois Fages and Pierre Deransart},
  title = 	 {Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping},
  booktitle = 	 {Proceedings of the 20th Conference on the 
                  Foundations of Software Technology 
                  and Theoretical Computer Science},
  year =	 2000,
  publisher =      {Springer-Verlag},
  series =       {LNCS},
  volume =       {1974},
  pages =        {214--226},
  editor =       {Sanjiv Kapoor and Sanjiva Prasad},
}

@TechReport{SFD00-tr,
  author = 	 {Jan-Georg Smaus and Fran{\c c}ois Fages and Pierre Deransart},
  title = 	 {Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping},
  institution =  {INRIA},
  number =       {RR-4020},
  year = 	 2000,
  note =         {Long version of \cite{SFD00}, available via CoRR: {\tt http://arXiv.org/archive/cs/intro.html}}
}

@TechReport{BERS00,
  author = 	 {Annalisa Bossi and Sandro Etalle and Sabina Rossi and Jan-Georg Smaus},
  title = 	 {On the Semantics and Termination of Logic Programs with Dynamic Scheduling},
  institution =  {Universit{\`a} Ca' Foscari di Venezia},
  year = 	 2000,
  note =         {Early version of \cite{BERS01}},
  number =	 {CS2000-11}
}

@TechReport{DS00,
  author = 	 {Pierre Deransart and Jan-Georg Smaus},
  title = 	 {Well-Typed Logic Programs Are not Wrong},
  institution =  {INRIA},
  number =       {RR-4082},
  year = 	 2000,
  note =         {Long version of \cite{DS01}, available via CoRR: {\tt http://arXiv.org/archive/cs/intro.html}}
}

@InProceedings{DS01,
  author = 	 {Pierre Deransart and Jan-Georg Smaus},
  title = 	 {Well-Typed Logic Programs Are not Wrong},
  booktitle = 	 {Proceedings of the 5th International 
                  Symposium on Functional and Logic Programming},
  year =	 2001,
  editor =	 {Herbert Kuchen and Kazunori Ueda},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
  pages =        {280--295},
  volume =       {2024}
}

@Article{SHK01,
  author = 	 {Jan-Georg Smaus and Patricia M. Hill and Andy King},
  title = 	 {Verifying
  Termination and Error-freedom of Logic Programs with {\tt block} Declarations},
  journal = 	 {Theory and Practice of Logic Programming},
  year = 	 2001,
  volume =       1,
  number =       4, 
  pages =        {447--486}
}


@InProceedings{BERS01,
  author = 	 {Annalisa Bossi and Sandro Etalle and Sabina Rossi and Jan-Georg Smaus},
  title = 	 {Semantics and Termination of Simply-Moded Logic Programs with Dynamic
  Scheduling},
  booktitle = 	 {Proceedings of the European Symposium on Programming},
  year =	 2001,
  editor =	 {David Sands},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
  volume = 2028,
  pages = {402--416}  
}

@Unpublished{BERS01-tr,
  author = 	 {Annalisa Bossi and Sandro Etalle and Sabina Rossi and Jan-Georg Smaus},
  title = 	 {Semantics and Termination of Simply-Moded Logic Programs with Dynamic
  Scheduling},
  note = 	 {Long version of \cite{BERS01}, available via CoRR: 
                  {\tt http://arXiv.org/archive/cs/intro.html}},
  year =	 2001
}

@Article{AS01,
  author = 	 {Krzysztof R. Apt and Jan-Georg Smaus},
  title = 	 {Rule-based versus Procedure-based View of Logic Programming},
  journal = 	 {Joint Bulletin of the Novosibirsk Computing Center and Institute of
Informatics Systems; Series: Computer Science},
  year = 	 2001,
  volume =	 16,
  pages =        {75--97},
}

@Unpublished{Sma01-aci-corr,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Analysis of Polymorphically Typed Logic Programs
                  Using {ACI}-Unification},
  note = 	 {Long version of \cite{Sma01-aci-lpar}, 
                  available via CoRR: {\tt http://arXiv.org/archive/cs/intro.html}},
  year =	 2001
}

@InProceedings{Sma01-aci-lpar,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Analysis of Polymorphically Typed Logic Programs
                  Using {ACI}-Unification},
  booktitle = 	 {Proceedings of the 8th International Conference on
                  Logic for Programming, Artificial Intelligence and Reasoning},
  pages =	 {280--295},
  year =	 2001,
  editor =	 {Robert Nieuwenhuis and Andrei Voronkov},
  volume =	 2250,
  series =	 {LNAI},
  publisher =	 {Springer-Verlag}
}

@Article{PRS02,
  author = 	 {Dino Pedreschi and Salvatore Ruggieri and Jan-Georg Smaus},
  title = 	 {Classes of Terminating Logic Programs},
  journal = 	 {Theory and Practice of Logic Programming},
  year = 	 2002,
  volume =       {2},
  number =       {3},
  pages =        {369--418}
}

@Article{DS02,
  author = 	 {Pierre Deransart and Jan-Georg Smaus},
  title = 	 {Subject Reduction of Logic Programs as Proof-Theoretic Property},
  journal = 	 {Journal of Functional and Logic Programming 
                  (electronic journal)},
  publisher =    {EAPLS},  
  year =         {2002},
  volume=        {2002},
  number=        {2}
}

@InProceedings{Sma02-flops,
  author = 	 {Jan-Georg Smaus},
  title = 	 {The Head Condition and Polymorphic Recursion},
  booktitle = 	 {Proceedings of the 6th International 
                  Symposium on Functional and Logic Programming},
  pages =	 {259--274},
  year =	 2002,
  editor =	 {Zhenjiang Hu and Mario Rodr{\'\i}guez-Artalejo},
  volume =	 2441,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{BKBetal03,
  author = 	 {Bernd Krieg-Br{\"u}ckner and Dieter Hutter and Arne Lindow and
                  Christoph L{\"u}th and Achim Mahnke and Erica Melis and Philipp Meier and
                  Arnd Poetzsch-Heffter and Markus Roggenbach and George Russell
                  and Jan-Georg Smaus and Martin Wirsing},
  title = 	 {MultiMedia Instruction in Safe and Secure Systems},
  booktitle = 	 {Recent Trends in Algebraic Development Techniques,
16th International Workshop, WADT 2002},
  pages =	 {82--117},
  year =	 2003,
  editor =	 {Martin Wirsing and Dirk Pattinson and Rolf Henecker},
  volume =	 {2755},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{Sma03-iclp,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Is there an Optimal Generic Semantics for
                  First-Order Equations?},
  booktitle = 	 {Proceedings of the 19th International Conference on
                  Logic Programming},
  pages =	 {438--450},
  year =	 2003,
  editor =	 {Catuscia Palamidessi},
  series =	 {LNCS},
  volume =       {2916},
  publisher =	 {Springer-Verlag}
}

@InProceedings{Sma03-iclp-poster,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Termination of Logic Programs for Various Dynamic
                  Selection Rules},
  booktitle = 	 {Proceedings of the 19th International Conference on
                  Logic Programming},
  pages =	 {511--512},
  year =	 2003,
  editor =	 {Catuscia Palamidessi},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
  volume =       {2916},
  note =	 {Abstract of Poster Presentation}
}

@TechReport{SmaTR191-03,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Termination of Logic Programs for Various Dynamic Selection Rules},
  institution =  {Institut f{\"u}r Informatik, Universit{\"a}t Freiburg},
  year = 	 2003,
  number =	 191
}

@TechReport{SmaTR203-04,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Termination of Logic Programs Using Various Dynamic Selection Rules},
  institution =  {Institut f{\"u}r Informatik, Universit{\"a}t Freiburg},
  year = 	 2004,
  number =	 {203}
}

@Article{BERS04,
  author = 	 {Annalisa Bossi and Sandro Etalle and Sabina Rossi and Jan-Georg Smaus},
  title = 	 {Termination of Simply Moded Logic Programs with Dynamic  
  Scheduling},
  journal = 	 {Transactions on Computational Logic},
  year = 	 2004,
  volume =       5,
  number =       3,
  pages =        {470-507}
}

@InCollection{PRS04,
  author = 	 {Dino Pedreschi and Salvatore Ruggieri and Jan-Georg Smaus},
  title = 	 {Characterisations of Termination in Logic Programming},
  booktitle = 	 {Program Development in Computational Logic},
  publisher =	 {Springer-Verlag},
  year =	 2004,
  volume =       3049,
  editor =	 {Maurice Bruynooghe and Kung-Kiu Lau},
  series =	 {LNCS},
  pages =        {376--431}
}

@InProceedings{Sma04-iclp,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Termination of Logic Programs Using Various Dynamic
                  Selection Rules},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  series =	 {LNCS},
  volume =       {3132},
  publisher =	 {Springer-Verlag},
  pages =        {43-57}
}

@InProceedings{HofSmaRybKupPod06,
  author = 	 {J{\"o}rg Hoffmann and Jan-Georg Smaus and
                  Andrey Rybalchenko and Sebastian Kupferschmid and
                  Andreas Podelski},
  editor =       {Stefan Edelkamp and Alessio R. Lomuscio},   
  title = 	 {Using Predicate Abstraction to Generate Heuristic
                  Functions in {UPPAAL}},
  booktitle = 	 {Proceedings of the 4th Workshop on Model Checking
                  and Artificial Intelligence ({MoChArt} 2006)},
  year =	 2006
}

@InProceedings{RatSma06,
  author = 	 {Stefan Ratschan and Jan-Georg Smaus},
  editor =       {Christos G. Cassandras and Alessandro Giua and Carla
                  Seatzu and Janan Zaytoon},
  title = 	 {Verification-Integrated Falsification of Non-deterministic
Hybrid Systems},
  pages =        {371-376},
  booktitle = 	 {Preprints of the IFAC Conference on Analysis and
                  Design of Hybrid Systems},
  year = 2006,
  note = {Available via \url{http://www.diee.unica.it/~adhs06/CD/PAPERS/FB1.2.pdf}}
}

@InProceedings{Sma-SAT+CP06,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Representing {B}oolean Functions as Linear Pseudo-{B}oolean
  Constraints},
  booktitle = 	 {Proceedings of the {CP} 2006 Workshop on the
Integration of {SAT} and {CP} techniques},
  year =	 2006,
  pages =        {49-63},
  editor =	 {Youssef Hamadi}
}

@TechReport{SmaTR227-06,
  author = 	 {Jan-Georg Smaus},
  title = 	 {Representing {B}oolean Functions as Linear Pseudo-{B}oolean
                  Constraints},
  institution =  {Institut f{\"u}r Informatik, Universit{\"a}t Freiburg},
  year = 	 2006,
  number =	 227,
  note =         {Long version of \cite{Sma-SAT+CP06}}
}

@InProceedings{HofSmaRybKupPod07,
  author = 	 {J{\"o}rg Hoffmann and Jan-Georg Smaus and
                  Andrey Rybalchenko and Sebastian Kupferschmid and
                  Andreas Podelski},
  editor =       {Stefan Edelkamp and Alessio Lomuscio},   
  title = 	 {Using Predicate Abstraction to Generate Heuristic
                  Functions in {UPPAAL}},
  booktitle = 	 {Post-Proceedings of the 4th (2006) Workshop on Model Checking
                  and Artificial Intelligence},
  year =	 2007,
  series =	 {LNCS},
  pages     =    {51-66},
  volume    =    {4428},
  publisher =	 {Springer-Verlag}
}

@InProceedings{Sma-CPAIOR07,
  author = 	 {Jan-Georg Smaus},
  title = 	 {On {B}oolean Functions Encodable as a Single Linear Pseudo-{B}oolean
  Constraint},
  booktitle = 	 {Proceedings of the 4th International Conference on
        Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems},
  year =	 2007,
  editor =	 {Pascal Van Hentenryck and Laurence Wolsey},
  series =	 {LNCS},
  volume =       {4510},
  pages =        {288-302},
  publisher =	 {Springer-Verlag}
}

@TechReport{SmaTR230-07,
  author = 	 {Jan-Georg Smaus},
  title = 	 {On {B}oolean Functions Encodable as a Single Linear Pseudo-{B}oolean
  Constraint},
  institution =  {Institut f{\"u}r Informatik, Universit{\"a}t Freiburg},
  year = 	 2007,
  number =	 230,
  note = {Long version of \cite{Sma-CPAIOR07}. Also available as TR No.~13 on \url{http://www.avacs.org/}}
}