publications

2024

1. Efficient Cost Bounds with Linear Maps David Kahn, Jan Hoffmann, and Thomas Reps Working paper. 2024
2. Robust Resource Bounds with Static Analysis and Bayesian Inference Long Pham, Feras Saad, and Jan Hoffmann Working paper. 2024
3. Probabilistic Inference with Soundly Composed Guide Programs Long Pham, Di Wang, Feras Saad, and Jan Hoffmann Working paper. 2024
4. Modeling and Analyzing Evaluation Cost of CUDA Kernels Stefan Muller, and Jan Hoffmann ACM Transactions on Parallel Computing. 2024

2023

1. Nomos-UC: A Programming Framework for Cryptography Based on Resource-Aware Session Types Surya Bakshi, Ankush Das, Andrew Miller, and Jan Hoffmann Working paper. 2023
2. Automatic Amortized Resource Analysis with Regular Recursive Types Jessie Grosen, David Kahn, and Jan Hoffmann In 38th ACM/IEEE Symposium on Logic in Computer Science (LICS’ 23). 2023 [pdf] [tr]
3. Worst-Case Input Generation for Concurrent Processes Long Pham, and Jan Hoffmann Working paper. 2023
4. Probabilistic Resource-Aware Session Types Ankush Das, Di Wang, and Jan Hoffmann In 50th Symposium on Principles of Programming Languages (POPL ’23). 2023 [pdf] [tr]

2022

1. Nomos: A Protocol-Enforcing, Asset-Tracking, and Gas-Aware Language for Smart Contracts Ankush Das, Jan Hoffmann, and Frank Pfenning Technical Report. 2022 [pdf]
2. Two Decades of Automatic Amortized Resource Analysis Jan Hoffmann, and Steffen Jost Math. Struct. Comput. Sci.. 2022 [pdf]

2021

1. Automatic Resource Analysis with the Quantum Physicist’s Method David Kahn, and Jan Hoffmann In 26th International Conference on Functional Programming (ICFP’21). 2021 [pdf]
2. Central Moment Analysis for Cost Accumulators in Probabilistic Programs Di Wang, Jan Hoffmann, and Thomas Reps In 42th Conference on Programming Language Design and Implementation (PLDI’21). 2021 [pdf]
3. Sound Probabilistic Inference via Guide Types Di Wang, Jan Hoffmann, and Thomas Reps In 42th Conference on Programming Language Design and Implementation (PLDI’21). 2021 [pdf]
4. Modeling and Analyzing Evaluation Cost of CUDA Kernels Stefan Muller, and Jan Hoffmann In 48th Symposium on Principles of Programming Languages (POPL’21). 2021 [pdf]
5. A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis Vineet Rajani, Marco Gaboardi, Deepak Garg, and Jan Hoffmann In 48th Symposium on Principles of Programming Languages (POPL’21). 2021 [pdf]
6. Typable Fragments of Polynomial Automatic Amortized Resource Analysis Long Pham, and Jan Hoffmann In 29th EACSL Annual Conference on Computer Science Logic (CSL’21). 2021 [pdf]
7. Resource-Aware Session Types for Digital Contracts Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, and Ishani Santurkar In 2021 IEEE Computer Security Foundations Symposium (CSF’21). 2021 [pdf]

2020

1. Combining Source and Target Level Cost Analyses for OCaml Programs Stefan Muller, and Jan Hoffmann Working paper. 2020 [pdf]
2. Liquid Resource Types Tristan Knoth, Di Wang, Adam Reynolds, Nadia Polikarpova, and Jan Hoffmann In 25th International Conference on Functional Programming (ICFP’20). 2020 [pdf]
3. Raising Expectations: Automating Expected Cost Analysis with Types Di Wang, David M. Kahn, and Jan Hoffmann In 25th International Conference on Functional Programming (ICFP’20). 2020 [pdf]
4. Exponential Automatic Amortized Resource Analysis David Kahn, and Jan Hoffmann In 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’20). 2020 [pdf]

2019

1. BLT: Exact Bayesian Inference with Distribution Transformers Charles Yuan, and Jan Hoffmann Technical Report. 2019 [pdf]
2. Resource-Guided Program Synthesis Tristan Knoth, Di Wang, Jan Hoffmann, and Nadia Polikarpova In 40th Conference on Programming Language Design and Implementation (PLDI’19). 2019 [pdf] [tr]
3. Type-Guided Worst-Case Input Generation Di Wang, and Jan Hoffmann In 46th Symposium on Principles of Programming Languages (POPL’19). 2019 [pdf] [slides] [tr]
4. A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism Di Wang, Jan Hoffmann, and Thomas Reps In Mathematical Foundations of Programming Semantics XXXV (MFPS’19). 2019 [pdf] [slides] [tr]

2018

1. Automatic Space Bound Analysis for Functional Programs with Garbage Collection Yue Niu, and Jan Hoffmann In 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR’18). 2018 [pdf]
2. Parallel Complexity Analysis with Temporal Session Types Ankush Das, Jan Hoffmann, and Frank Pfenning In 23rd International Conference on Functional Programming (ICFP’18). 2018 [pdf]
3. Work Analysis with Resource-Aware Session Types Ankush Das, Jan Hoffmann, and Frank Pfenning In 33th ACM/IEEE Symposium on Logic in Computer Science (LICS’18). 2018 [pdf]
4. PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs Di Wang, Jan Hoffmann, and Thomas Reps In 39th Conference on Programming Language Design and Implementation (PLDI’18). 2018 [pdf] [slides]
5. Bounded Expectations: Resource Analysis for Probabilistic Programs Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann In 39th Conference on Programming Language Design and Implementation (PLDI’18). 2018 [pdf] [tr] [code]

2017

1. Arrays and References in Resource Aware ML Benjamin Lichtman, and Jan Hoffmann In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD’17). 2017 [pdf]
2. Automated Resource Analysis with Coq Proof Objects Quentin Carbonneaux, Jan Hoffmann, Thomas Reps, and Zhong Shao In 29th International Conference on Computer-Aided Verification (CAV’17). 2017 [pdf]
3. ML for ML: Learning Cost Semantics by Experiment Ankush Das, and Jan Hoffmann In 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17). 2017 [pdf]
4. Verifying and Synthesizing Constant-Resource Implementations with Types Van Chan Ngo, Mario Dehesa-Azuara, Matthew Fredrikson, and Jan Hoffmann In 38th IEEE Symposium on Security and Privacy (S&P ’17). 2017 [pdf] [tr] [code]
5. Relational Cost Analysis Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann In 44th Symposium on Principles of Programming Languages (POPL’17). 2017 [pdf] [tr]
6. Towards Automatic Resource Bound Analysis for OCaml Jan Hoffmann, Ankush Das, and Shu-Chun Weng In 44th Symposium on Principles of Programming Languages (POPL’17). 2017 [pdf] [tr]

2016

1. Learning Cost Semantics for Modeling Running Time of OCaml Programs Ankush Das, and Jan Hoffmann Presented at Syntax and Semantics of Low-Level Languages (LOLA’16). 2016 [pdf]

2015

1. Type-Based Amortized Resource Analysis with Integers and Arrays Jan Hoffmann, and Zhong Shao J. Funct. Program.. 2015 [pdf]
2. Compositional Certified Resource Bounds Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao In 36th Conference on Programming Language Design and Implementation (PLDI’15). Artifact submitted and approved. 2015 [pdf] [tr]
3. Automatic Static Cost Analysis for Parallel Programs Jan Hoffmann, and Zhong Shao In 24th European Symposium on Programming (ESOP’15). 2015 [pdf]

2014

1. Type-Based Amortized Resource Analysis with Integers and Arrays Jan Hoffmann, and Zhong Shao In 12th International Symposium on Functional and Logic Programming (FLOPS’14). 2014 [pdf] [tr]
2. End-to-End Verification of Stack-Space Bounds for C Programs Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro, and Zhong Shao In 35th Conference on Programming Language Design and Implementation (PLDI’14). Artifact submitted and approved. 2014 [pdf] [tr]

2013

1. Tracking Data-Flow with Open Closure Types Gabriel Scherer, and Jan Hoffmann In 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR’13). 2013 [pdf]
2. Characterizing Progress Properties of Concurrent Objects via Contextual Refinements Hongjin Liang, Jan Hoffmann, Xinyu Feng, and Zhong Shao In 24th International Conference on Concurrency Theory (CONCUR’13). 2013 [pdf] [tr]
3. Quantitative Reasoning for Proving Lock-Freedom Jan Hoffmann, Michael Marmar, and Zhong Shao In 28th ACM/IEEE Symposium on Logic in Computer Science (LICS’13). 2013 [pdf] [slides] [tr]
4. The Complexity of Computing Minimal Unidirectional Covering Sets Dorothea Baumeister, Felix Brandt, Felix A. Fischer, Jan Hoffmann, and Jörg Rothe Theory of Computing Systems. 2013 [pdf]

2012

1. Resource Aware ML Jan Hoffmann, Klaus Aehlig, and Martin Hofmann In 24rd International Conference on Computer Aided Verification (CAV’12). 2012 [pdf]
2. Multivariate Amortized Resource Analysis Jan Hoffmann, Klaus Aehlig, and Martin Hofmann ACM Trans. Program. Lang. Syst.. 2012 [pdf]
3. Higher-Order Functional Reactive Programming in Bounded Space Neelakantan R. Krishnaswami, Nick Benton, and Jan Hoffmann In 39th Symposium on Principles of Programming Languages (POPL’12). 2012 [pdf]

2011

1. Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis Jan Hoffmann PhD Thesis. Ludwig-Maximilians-Universität München. 2011 [pdf]
2. Multivariate Amortized Resource Analysis Jan Hoffmann, Klaus Aehlig, and Martin Hofmann In 38th Symposium on Principles of Programming Languages (POPL’11). 2011 [pdf]

2010

1. Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics Jan Hoffmann, and Martin Hofmann In 8th Asian Symposium on Programming Languages (APLAS’10). 2010 [pdf] [tr]
2. Amortized Resource Analysis with Polynomial Potential Jan Hoffmann, and Martin Hofmann In 19th European Symposium on Programming (ESOP’10). 2010 [pdf] [tr]
3. The Complexity of Computing Minimal Unidirectional Covering Sets Dorothea Baumeister, Felix Brandt, Felix A. Fischer, Jan Hoffmann, and Jörg Rothe In Algorithms and Complexity, 7th International Conference (CIAC’10). 2010 [pdf]
4. The Computational Complexity of Weak Saddles Felix Brandt, Markus Brill, Felix A. Fischer, and Jan Hoffmann Theory of Computing Systems. 2010 [pdf]

2009

1. Computing Shapley’s Saddles Felix Brandt, Markus Brill, Felix Fischer, Paul Harrenstein, and Jan Hoffmann ACM SIGecom Exchanges. 2009 [pdf]
2. The Computational Complexity of Weak Saddles Felix Brandt, Markus Brill, Felix A. Fischer, and Jan Hoffmann In Algorithmic Game Theory, Second International Symposium (SAGT’09). 2009 [pdf]
3. Finding a Tree Structure in a Resolution Proof is NP-Complete Jan Hoffmann Theoretical Computer Science. 2009 [pdf]

2008

1. Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning Samuel R. Buss, Jan Hoffmann, and Jan Johannsen Logical Methods in Computer Science. 2008 [pdf]
2. The NP-hardness of Finding a Directed Acyclic Graph for Regular Resolution Samuel R. Buss, and Jan Hoffmann Theoretical Computer Science. 2008 [pdf]

2007

1. Resolution Proofs and DLL-Algorithms with Clause Learning Jan Hoffmann Diploma Thesis, LMU München. 2007 [pdf]