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.
Comments on the page please send to webmaster at ls14.cs.tu-dortmund.de
Last update
21.09.2017 00:11
Privacy Policy
Imprint