Publications

2007

• On Boolean Functions Encodable as a Single Linear Pseudo-Boolean Constraint. J.-G. Smaus. In Pascal Van Hentenryck and Laurence Wolsey, editors, CPAIOR'07. Volume 4510 of LNCS, Springer-Verlag, pages 288-302, 2007. Long version available as Technical Report No. 230 (Universität Freiburg) or Technical Report No. 13 (AVACS project).

2006

• Using Predicate Abstraction to Generate Heuristic Functions in Uppaal. J. Hoffmann, J.-G. Smaus, A. Rybalchenko, S. Kupferschmid and A. Podelski. In S. Edelkamp and A. R. Lomuscio, editors, MoChArt'06. Volume 4428 of LNCS, Springer-Verlag, pages 51-66, 2007.
• Representing Boolean Functions as Linear Pseudo-Boolean Constraints. J.-G. Smaus. In Youssef Hamadi, editor, SAT+CP'06.
• Using Predicate Abstraction to Generate Heuristic Functions in Uppaal. J. Hoffmann, J.-G. Smaus, A. Rybalchenko, S. Kupferschmid and A. Podelski. In S. Edelkamp and A. R. Lomuscio, editors, Pre-Proceedings of MoChArt'06.
• Verification-Integrated Falsification of Non-deterministic Hybrid Systems. S. Ratschan and J.-G. Smaus. In C. G. Cassandras, A. Giua, and J. Zaytoon, editors, ADHS'06.

2004

• Termination of Logic Programs Using Various Dynamic Selection Rules. J.-G. Smaus. In B. Demoen and V. Lifschitz, editors, ICLP'04. Volume 3132 of LNCS, Springer-Verlag, pages 43-57, September 2004. Long version available as Technical Report No. 203 (Universität Freiburg)
• Characterisations of Termination in Logic Programming. D. Pedreschi, S. Ruggieri and J.-G. Smaus. In M. Bruynooghe and K. Lau, editors, Program Development in Computational Logic, special LNCS volume on the occasion of ten years LOPSTR conference. Volume 3049 of LNCS, Springer-Verlag, pages 376-431, June 2004.
• Termination of Simply Moded Logic Programs with Dynamic Scheduling. A. Bossi, S. Etalle, S. Rossi and J.-G. Smaus. Transactions on Computational Logic, 5(3), pages 470-507, 2004.

2003

• Is there an Optimal Generic Semantics for First-Order Equations?. J.-G. Smaus. In C, Palamidessi, editor, ICLP'03. Volume 2916 of LNCS, Springer-Verlag, pages 438-450, December 2003.
• Termination of Logic Programs for Various Dynamic Selection Rules. J.-G. Smaus. In C, Palamidessi, editor, ICLP'03. Abstract of poster presentation. Volume 2916 of LNCS, Springer-Verlag, pages 511-512, December 2003. Long version available as Technical Report No. 191 (Universität Freiburg)
• MultiMedia Instruction in Safe and Secure Systems. B. Krieg-Brückner, D. Hutter, A. Lindow, C. Lüth, A. Mahnke, E. Melis, P. Meier, A. Poetzsch-Heffter, M. Roggenbach, G. Russell, J.-G. Smaus and M. Wirsing. In M. Wirsing, D. Pattinson and R. Henecker, editors, WADT'02. Volume 2755 of LNCS, Springer-Verlag, November 2003.

2002

• The Head Condition and Polymorphic Recursion. J.-G. Smaus. In Z. Hu and M. Rodríguez-Artalejo, editors, FLOPS'02. Volume 2441 of LNCS, Springer-Verlag, pages 259-274, September 2002.
• Subject Reduction of Logic Programs as Proof-Theoretic Property. P. Deransart and J.-G. Smaus. Journal of Functional and Logic Programming, volume 2002, number 2. Extended version of FLOPS'01 paper.
• Classes of Terminating Logic Programs. D. Pedreschi and S. Ruggieri and J.-G. Smaus. Theory and Practice of Logic Programming, 2(3), pages 369-418, 2002. Available via CoRR.

2001

• Rule-based versus Procedure-based View of Logic Programming. K. R. Apt and J.-G. Smaus. Joint Bulletin of the Novosibirsk Computing Center and Institute of Informatics Systems; Series: Computer Science, 16, pages 75-97, 2001.
• Analysis of Polymorphically Typed Logic Programs Using ACI-Unification. J.-G. Smaus. In R. Nieuwenhuis and A. Voronkov, editors, LPAR'01. Volume 2250 of LNAI, Springer-Verlag, pages 280-295, October 2001. Long version available via CoRR.
• Semantics and Termination of Logic Programs with Dynamic Scheduling. A. Bossi and S. Etalle and S. Rossi and J.-G. Smaus. In D. Sands, editor, ESOP'01. Volume 2028 of LNCS, Springer-Verlag, pages 402-416, April 2001. Long version available via CoRR.
• Verifying termination and error-freedom of logic programs with block declarations. J.-G. Smaus, P.M. Hill, and A.M. King. Theory and Practice of Logic Programming, 1(4), pages 447-486, 2001.
• Well-Typed Logic Programs Are not Wrong. P. Deransart and J.-G. Smaus. In H. Kuchen and K. Ueda, editors, FLOPS'01. Volume 2024 of LNCS, Springer-Verlag, pages 280-295, March 2001. Long version appeared as Technical Report INRIA-Rocquencourt, available via CoRR.

2000

• Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping. J.-G. Smaus, F. Fages and P. Deransart. In S. Kapoor and S. Prasad, editors, FST&TCS'00. Volume 1974 of LNCS, Springer-Verlag, pages 214-226, December 2000. Long version appeared as Technical Report INRIA-Rocquencourt, available via CoRR.
• Well-typed Programs Are not Wrong. J.-G. Smaus and P. Deransart. In M. Leuschel et al., editors, VCL workshop , held within CL'2000. Technical report DSEE-TR-2000-6 of the University of Southampton, 2000.
• Les programmes bien typés ont tout bon. J.-G. Smaus and P. Deransart. In Touraïvane, editor, JFPLC'00. Hermes Science Publications, pages 49-65, 2000. (English abstract)
• Mode Analysis Domains for Typed Logic Programs. J.-G. Smaus, P.M. Hill, and A.M. King. Technical report 2000.06, University of Leeds, 2000. Long version of paper with same title at LOPSTR'99.
• Mode analysis domains for typed logic programs. J.-G. Smaus, P.M. Hill, and A.M. King. In A. Bossi, editor, LOPSTR'99. Volume 1817 of LNCS, Springer-Verlag, pages 83-102, January 2000.

1999

• Modes and Types in Logic Programming. J.-G. Smaus. PhD thesis, University of Kent at Canterbury, December 1999.
• Proving termination of input-consuming logic programs. J.-G. Smaus. In D. De Schreye, editor, ICLP'99. 15 pages. MIT Press, pages 335-349, November 1999.
• Proving Termination of Input-Consuming Logic Programs. J.-G. Smaus. Technical Report 10-99, Computing Laboratory, University of Kent at Canterbury, Kent, CT2 7NF, UK, September 1999. Long version of paper with same title at ICLP'99.
• Mode analysis domains for typed logic programs. J.-G. Smaus, Pat Hill, and Andy King. In A. Bossi, editor, LOPSTR'99 Pre-Proceedings. 8 pages. Universita Ca Foscari di Venezia, September 1999. Extended abstract (see full version).
• Quotienting share for dependency analysis. A. King, J.-G. Smaus, and P.M. Hill. In D. Swierstra, editor, ESOP'99. Volume 1576 of LNCS, Springer-Verlag, pages 59-73, April 1999.
• Preventing instantiation errors and loops for logic programs with multiple modes using block declarations. J.-G. Smaus, P.M. Hill, and A.M. King. In P. Flener, editor, LOPSTR'98, LNCS, pages 289-307. Volume 1559 of LNCS, Springer-Verlag, March 1999.

1998

• Verification of logic programs with block declarations running in several modes. J.-G. Smaus, Pat Hill, and Andy King. Technical Report 7-98, University of Kent at Canterbury, Canterbury, CT2 7NF, United Kingdom, July 1998. Contains proofs for PLILP/ALP'98 and LOPSTR'98 papers; see also TPLP 2001 paper.
• Preventing instantiation errors and loops for logic programs with several modes using block declarations. J.-G. Smaus, P.M. Hill, and A.M. King. In P. Flener, editor, LOPSTR'98 Pre-Proceedings. 8 pages. Technical Report UMCS-98-6-1 (University of Manchester), June 1998. Extended abstract.
• Termination of logic programs with block declarations running in several modes. J.-G. Smaus, P.M. Hill, and A.M. King. In Catuscia Palamidessi, editor, PLILP/ALP '98, pages 73-99, Volume 1490 of LNCS, Springer-Verlag, June 1998.

1997

• Domain Construction for Mode Analysis of Typed Logic Programs. J.-G. Smaus, Pat Hill, and Andy King. Abstract of poster presentation. In Lee Naish, editor, ICLP'97, MIT Press, page 418, 1997. See LOPSTR'99 paper.

1996

• Resolution K-Transformations. J.-G. Smaus. Master's thesis, Universität des Saarlandes (Max-Planck-Institut für Informatik), Saarbrücken, Germany, February 1996.