Jump label

Service navigation

Main navigation

You are here:

Sub navigation

  • Staff pages+

Main content

Publications - Prof. Jakob Rehof

Proceedings

  • Modular Synthesis of Product Lines (ModSyn-PL)
    G. T. Heineman and J. Rehof (Eds.)
    SPLC 2015.
    DOI: 10.1145/2791060.2791061
  • Proceedings Seventh Workshop on Intersection Types and Related Systems, ITRS 2014
    EPTCS 177, Electronic Proceedings in Theoretical Computer Science, 2015.
    DOI: 10.4204/EPTCS.177
  • Cloud Computing for Logistics
    M. ten Hompel, J. Rehof and O. Wolf (Eds.)
    Springer Lecture Notes in Logistics 2015.
    DOI: 10.1007/978-3-319-13404-8
  • Tools and Algorithms for the Construction and Analysis of Systems
    C. R. Ramakrishnan and J. Rehof (Eds.)
    14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings Springer 2008.
    DOI: 10.1007/978-3-540-78800-3

Research Papers (peer-reviewed)

2017

  • Typability in Bounded Dimension
    A. Dudenhefner and J. Rehof
    LICS 2017, 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Reykjavik, Iceland, June 2017
    PDF
  • Intersection Type Calculi of Bounded Dimension
    A. Dudenhefner and J. Rehof
    POPL 2017, Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, January 2017
    DOI: 10.1145/3009837.3009862
    PDF

2016

  • Combinatory Process Synthesis
    J. Bessai, A. Dudenhefner, B. Düdder, M. Martens and J. Rehof
    Proceedings of 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Ed. by Tiziana Margaria and Bernhard Steffen. accepted.
    Corfu, October 05-14 2016.
    DOI: 10.1007/978-3-319-47166-2_19
  • A Long and Winding Road Towards Modular Synthesis
    J. Bessai, B. Düdder, G. T. Heineman, and J. Rehof
    Proceedings of 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Ed. by Tiziana Margaria and Bernhard Steffen. accepted.
    Corfu, October 05-14 2016.
    DOI: 10.1007/978-3-319-47166-2_21
  • The Intersection Type Unification Problem
    A. Dudenhefner, M. Martens and J. Rehof
    FSCD 2016, 1st International Conference on Formal Structures for Computation and Deduction, Porto, Portugal, 22 - 26 June 2016.
    Leibniz International Proceedings in Informatics, June 2016.
  • Extracting a Formally Verified Subtyping Algorithm for Intersection Types from Ideals and Filters
    J. Bessai, A. Dudenhefner, B. Düdder and J. Rehof
    TYPES 2016, 22nd International Conference on Types for Proofs and Programs.
    Novi Sad, May 23-26 2016.
  • Rank 3 Inhabitation of Intersection Types Revisited
    J. Bessai, A. Dudenhefner, B. Düdder and J. Rehof
    TYPES 2016, 22nd International Conference on Types for Proofs and Programs.
    Novi Sad, May 23-26 2016.
  • Modal Intersection Types, Two-Level Languages, and Staged Synthesis
    F. Henglein and J. Rehof
    Semantics, Logics, and Calculi. Essays Dedicated to Hanne Riis Nielson and Flemming Nielson.
    Springer LNCS 9560, January 2016.
    DOI: 10.1007/978-3-319-27810-0_15

2015

  • Combinatory Synthesis of Classes using Feature Grammars
    J. Bessai, B. Düdder, G. T. Heineman, and J. Rehof
    In Proceedings of 12th International Conference on Formal Aspects of Component Software (FACS'15), Rio de Janeiro, Brazil, October 14-16, 2015.
  • Towards Migrating Object-Oriented Frameworks to Enable Synthesis of Product Line Members
    G. T. Heineman, A. Hoxha, B. Düdder, and J. Rehof
    In Proceedings of 19th International Software Product Line Conference (SPLC), Nashville, USA, July 20-24, 2015.
    DOI: 10.1145/2791060.2791076
  • Synthesizing Type-safe Compositions in Feature Oriented Software Designs using Staged Composition
    B. Düdder, J. Rehof and G. T. Heineman
    In ModSyn-PL Workshop in proceedings of 19th International Software Product Line Conference (SPLC), Nashville, USA, July 20-24, 2015.
    DOI: 10.1145/2791060.2793677
  • Mixin Composition Synthesis based on Intersection Types
    J. Bessai, A. Dudenhefner, B. Düdder, T. Chen, U. De'Liguoro and J. Rehof
    In Proceedings of TLCA 2015 13th International Conference on Typed Lambda Calculi and Applications, Warsaw, Poland, June 29 - July 03, 2015, to appear
    DOI: 10.4230/LIPIcs.TLCA.2015.76
    PDF
  • Staged Composition Synthesis
    B. Düdder, M. Martens and J. Rehof
    In Proceedings of Software Engineering & Software Management 2015, GI Fachtagung Software Engineering 2015, Dresden, Germany, March 17-20, 2015, Lecture Notes in Informatics (LNI), 89-90.

2014

  • Combinatory Logic Synthesizer
    J. Bessai, A. Dudenhefner, B. Düdder, M. Martens and J. Rehof
    ISoLA 2014, 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Corfu, Greece, October 2014, Part I, LNCS 8802, pp. 26--40. Springer, Heidelberg, 2014
    DOI: 10.1007/978-3-662-45234-9_3
    PDF
  • Design and Synthesis from Components (Dagstuhl Seminar 14232)
    J. Rehof and M. Y. Vardi
    Dagstuhl Reports 4(6): 29-47 (2014).
    DOI: 10.4230/DagRep.4.6.29
  • Staged Composition Synthesis
    B. Düdder, M. Martens and J. Rehof
    Proceedings 23rd European Symposium on Programming, ESOP 2014, Grenoble, France, April 5-13, 2014, LNCS 8410, Springer
    DOI: 10.1007/978-3-642-54833-8_5
    PDF

2013

  • Intersection Type Matching with Subtyping
    B. Düdder, M. Martens and J. Rehof
    Proceedings 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013, LNCS 7941 (ARCoSS), Springer
    DOI: 10.1007/978-3-642-38946-7_11
    PDF
  • Using Inhabitation in Bounded Combinatory Logic with Intersection Types for Composition Synthesis
    B. Düdder, O. Garbe, M. Martens, J. Rehof, and P. Urzyczyn
    Post-proceedings ITRS 2012, EPCTS, Vol. 121, March 2013
    DOI: 10.4204/EPTCS.121.2
    PDF
  • Towards Combinatory Logic Synthesis
    BEAT'13, 1st International Workshop on Behavioural Types
    Rome, January 22 2013.
    Proceedings at http://beat13.cs.aau.dk/
    PDF

2012

  • Bounded Combinatory Logic
    B. Düdder, M. Martens, J. Rehof and P. Urzyczyn
    CSL 2012, 21st EACSL Annual Conferences on Computer Science Logic, Fontainebleau, France, September 2012.
    LIPIcs volume 16.
    DOI: 10.4230/LIPIcs.CSL.2012.243
    PDF
  • Using Inhabitation in Bounded Combinatory Logic with Intersection Types for Composition Synthesis
    J. Rehof, B. Düdder, O.Garbe, M. Martens and P. Urzyczyn
    EPTCS Electronic Proceedings in Theoretical Computer Science, proceedings ITRS 2012 Intersection Types and Related Systems, Dubrovnik, Croatia 2012.
    PDF
  • Using Inhabitation in Bounded Combinatory Logic with Intersection Types for GUI Synthesis
    B. Düdder, O. Garbe, M. Martens, J. Rehof and P. Urzyczyn
    ITRS 2012, Intersection Types and Related Systems, Dubrovnik, Croatia, June 2012
    PDF
  • The Complexity of Inhabitation with Explicit Intersection
    J. Rehof and P. Urzyczyn
    R.L. Constable and A. Silva (Eds.): Logic and Program Semantics. Essays Dedicated to Dexter Kozen.
    Lecture Notes in Computer Science 7230, 2012.
    DOI: 10.1007/978-3-642-29485-3_16
    PDF

2011

  • Finite Combinatory Logic with Intersection Types
    J. Rehof and P. Urzyczyn
    TLCA 2011, Typed Lambda Calculi and Applications, Novi Sad 2011.
    Advanced Research in Computing and Software Science (ARCoSS) Springer LNCS 6690.
    DOI: 10.1007/978-3-642-21691-6_15
    PDF

2009

  • Static Deadlock Prevention in Dynamically Configured Communication Networks
    J. Rehof, M. Fähndrich and S. K. Rajamani
    In Kamal Lodaya, Madhavan Mukund, and R. Ramanujam, editors, Perspectives in Concurrency Theory (Festschrift for P. S. Thiagarajan).
    Universities Press, Indian Association for Research in Computer Science, 2009.

2008

  • Type-based flow analysis and context-free language reachability
    J. Rehof and M. Fähndrich
    Mathematical Structures in Computer Science, volume 18, October 2008, pp 823-894.
    Cambridge University Press.
    DOI: 10.1017/S0960129508006968

2005

  • Context-Bounded Model Checking of Concurrent Software
    J. Rehof and S. Qadeer
    Proceedings TACAS 2005, Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Edinburgh, U.K., April 4-8, 2005.
    DOI: 10.1007/978-3-540-31980-1_7
    PDF

2004

  • Models for Contract Conformance
    J. Rehof and S. K. Rajamani
    Invited paper, ISOLA 2004, First International Symposium on Leveraging Applications of Formal Methods, Paphos, Cyprus, October/November 2004.
    DOI: 10.1007/11925040_12
    PDF
  • Zing: Exploiting Program Structure for Model Checking Concurrent Software
    J. Rehof, T. Andrews, S. Qadeer, S. K. Rajamani, and Y. Xie
    Invited paper, Proceedings CONCUR 04, Fifteenth International Conference on Concurrency Theory, London, UK, August/September 2004.
    DOI: 10.1007/978-3-540-28644-8_1
    PDF
  • Stuck-Free Conformance
    J. Rehof, C. Fournet, T. Hoare, and S. K. Rajamani
    Proceedings CAV 04, 16th International Conference on Computer Aided Verification, Boston, USA, July 2004.
    DOI: 10.1007/978-3-540-27813-9_19
    PDF
  • Zing: A Model Checker for Concurrent Software
    J. Rehof, T. Andrews, S. Qadeer, S. K. Rajamani, and Y. Xie
    Proceedings CAV 04, 16th International Conference on Computer Aided Verification, Boston, USA, July 2004.
    DOI: 10.1007/978-3-540-27813-9_42
    PDF
  • Summarizing Procedures in Concurrent Programs
    J. Rehof, S. Qadeer and S. K. Rajamani
    Proceedings POPL 04, 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Venice, Italy, January 2004.
    DOI: 10.1145/964001.964022
    PDF

2002

  • Conformance Checking for Models of Asynchronous Message Passing Software
    J. Rehof and S. K. Rajamani
    To appear, Proceedings CAV 02, Conference on Computer-Aided Verification, Copenhagen, Denmark, July 27-31, 2002.
    PDF
  • Types as Models: Model Checking Message-Passing Programs
    J. Rehof, S. Chaki and S. K. Rajamani
    Proceedings POPL 02, 29'th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, January 2002.
    DOI: 10.1145/503272.503278
    PDF

2001

  • A Behavioral Module System for the Pi-Calculus
    J. Rehof and S. K. Rajamani
    Proceedings SAS 01, Static Analysis Symposium, Paris, France, July 2001.
    DOI: 10.1007/3-540-47764-0_22
    PDF
  • Estimating the Impact of Scalable Pointer Analysis on Optimization
    J. Rehof, M. Das, B. Liblit and M. Fähndrich
    Proceedings SAS 01, Static Analysis Symposium, Paris, France, July 2001
    DOI: 10.1007/3-540-47764-0_15
    PDF
  • Type Elaboration and Subtype Completion for Java Bytecode
    J. Rehof and T. Knoblock
    ACM TOPLAS, Transactions on Programming Languages and Systems, Volume 23 , No. 2 (Mar. 2001), 243-272.
    DOI: 10.1145/383043.383045
    PDF
  • Type-Based Flow Analysis: From Polymorphic Subtyping to CFL Reachability
    J. Rehof and M. Fähndrich
    Proceedings POPL 01, 28'th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, January 2001.
    PDF

2000

  • Scalable Context-Sensitive Flow Analysis Using Instantiation Constraints
    J. Rehof, M. Fähndrich and M. Das
    Proceedings PLDI 00, Programming Language Design and Implementation, Vancouver, Canada, June 2000.
    DOI: 10.1145/349299.349332
    PDF
  • Type Elaboration and Subtype Completion for Java Bytecode
    J. Rehof and T. Knoblock
    Proceedings POPL 00, 27'th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, MA, USA, January 2000.
    PDF

1999

  • Tractable Constraints in Finite Semilattices
    J. Rehof and T. Mogensen
    Science of Computer Programming 35 (1999) 191-221.
    A shorter conference version appeared in Proceedings SAS '96, Third International Static Analysis Symposium, Aachen, Germany, September 1996. Lecture Notes in Computer Science, vol. 1145.
    DOI: 10.1007/3-540-61739-6_48
    PDF

1998

  • Constraint Automata and the Complexity of Recursive Subtype Entailment
    J. Rehof and F. Henglein
    Proceedings ICALP '98, 25'th International Colloquium on Automata, Languages, and Programming, Aalborg, Denmark, July 1998.
    DOI: 10.1007/BFb0055089
    PDF

1997

  • The Complexity of Subtype Entailment for Simple Types
    J. Rehof and F. Henglein
    Proceedings LICS '97, Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 1997.
    DOI: 10.1109/LICS.1997.614961
    PDF
  • Minimal Typings in Atomic Subtyping
    Proceedings POPL '97, the 24'th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
    Paris, France, January 1997.
    DOI: 10.1145/263699.263738
    PDF

1996

  • Tractable Constraints in Finite Semilattices
    J. Rehof and T. Mogensen
    Proceedings SAS '96, Third International Static Analysis Symposium, Aachen, Germany, September 1996. Lecture Notes in Computer Science, vol. 1145.
    A journal version of this paper appears in Science of Computer Programming 35 (1999) 191-221 (see entry above with link to PDF).
    DOI: 10.1007/3-540-61739-6_48
    PDF
  • Strong Normalization for Non-Structural Subtyping via Saturated Sets
    Information Processing Letters 58 (1996) 157-162.
    DOI: 10.1016/0020-0190(96)00056-7
    PDF

1995

  • Safe Polymorphic Type Inference for a Dynamically Typed Language: Translating Scheme to ML
    J. Rehof and F. Henglein
    Proceedings FPCA '95, ACM SIGPLAN-SIGARCH Conference on Functional Programming Languages and Computer Architecture, La Jolla, California, June 1995.
    PDF

1994

  • The λΔ Calculus
    J. Rehof and M. H. Sørensen
    Proceedings TACS '94, International Symposium on Theoretical Aspects of Computer Software, Sendai, Japan, April 1994. Lecture Notes in Computer Science vol. 789, 1994.
    PDF

Non-peer Reviewed

  • Intelligente Orchestrierung von Planungsprozessen
    J. Winkels, J. Graefenstein, J. Rehof, M. Henke and D. Scholz
    Zeitschrift für wirtschaftlichen Fabrikbetrieb, Jahrg. 112 (2017) 4, S. 209 - 213
    DOI: 10.3139/104.111696
  • Modal Logic and Staged Computation
    B. Düdder and J. Rehof
    In Highlights of Logic, Games and Automata, Prague, Sept. 15–18, 2015
  • Combinatory Logic Synthesis and Alternation
    B. Düdder, M. Martens and J. Rehof
    In Highlights of Logic, Games and Automata, Paris, Sept. 18-21, 2013

Technical Reports

  • A Theory on Staged Composition Synthesis (Extended Version)
    B. Düdder, M. Martens and J. Rehof
    Technical Reports in Computer Science (Technische Universität Dortmund), TR 843, October 2013.
    PDF
  • Using Inhabitation in Bounded Combinatory Logic with Intersection Types for Composition Synthesis (Extended Version)
    B. Düdder, M. Martens, J. Rehof and P. Urzyczyn
    Technical Reports in Computer Science (Technische Universität Dortmund), TR 842, October 2012.
    PDF
  • Intersection Type Matching and Bounded Combinatory Logic (Extended Version)
    B. Düdder, M. Martens and J. Rehof
    Technical Reports in Computer Science (Technische Universität Dortmund), TR 841, October 2012, revised July 2013.
    PDF
  • Bounded Combinatory Logic (Extended Version)
    B. Düdder, M. Martens, J. Rehof, and P. Urzyczyn
    Technical Reports in Computer Science (Technische Universität Dortmund), TR 840, June 2012, revised October 2012.
    PDF
  • Stuck-Free Conformance Theory for CCS
    J. Rehof, C. Fournet, T. Hoare and S. K. Rajamani
    Microsoft Research Technical Report, MSR-TR-2004-69, February 2004, revised July 2004.
    PDF
  • Region-Based Model Abstraction
    J. Rehof, J. Condit, J. R. Larus and S. K. Rajamani
    Microsoft Research Technical Report, MSR-TR-2003-47, August 2003.
    PDF
  • Types as Models: Model Checking Message-Passing Programs
    J. Rehof, S. Chaki and S. K. Rajamani
    Microsoft Research Technical Report, MSR-TR-2001-71, August 2001.
    A shorter version of this paper is to appear in Proceedings POPL 2002.
  • From Polymorphic Subtyping to CFL Reachability: Context-Sensitive Flow Analysis Using Instantiation Constraints
    J. Rehof, M. Fähndrich and M. Das
    Microsoft Research Technical Report, MSR-TR-99-84, March 2000.
    A shorter version of this paper has appeared in Proceedings POPL 2001.
    PDF
  • Type Elaboration and Subtype Completion for Java Bytecode
    J. Rehof and T. Knoblock
    Microsoft Research Technical Report, MSR-TR-99-79, November 1999. This report is obsoleted by the journal version.
    PDF

Thesis

  • The Complexity of Simple Subtyping Systems
    Ph.D thesis, 209 pp., DIKU, April 1998.
    The main objective of this thesis is to understand why polymorphic subtype inference systems may be inherently difficult to scale up. This is done through a study of the complexity of type size, constraint simplification and constraint entailment in simple subtyping systems.
    Some key results in the thesis were presented in conference papers at ICALP '98, LICS '97 and POPL '97.
    PDF
  • Polymorphic Dynamic Typing. Aspects of Proof Theory and Inference.
    M.Sc thesis, 230 pp., DIKU, August 1995. DIKU Technical Report D-249.