I am a Ph.D. Candidate at the University of Waterloo, studying theoretical aspects of computer science. Specifically, I'm interested in fixed-parameter tractability of graph problems and their relation to mathematical logic. I am supervised by Jonathan Buss.

I have an M.Sc. from the Department of Mathematics and Statistics, University of Victoria, where I studied algorithmic graph theory under the supervision of Jing Huang. I characterized the end-vertices of lexicographic breadth first search on proper interval bipartite graphs.

I am also interested in software engineering, particularly model-driven software engineering and formal methods. I completed an M.Sc. in model-driven software engineering at the Department of Computer Science, University of Toronto, where I was supervised by Marsha Chechik. Historically, my research has focused on explicating design uncertainty in software models, and mitigating the effects of uncertainty while modelling, but my interest in this field extends to all areas of model-driven software engineering.

I have also participated in the Google Summer of Code program twice, most recently working on proof compression methods for first order resolution proofs. I have also worked on integrating Java Pathfinder and PRISM model checkers in a project aptly called jpf-prism. The Javadoc for the code can be found here, while the code itself can be found here.

Although I grew up in Toronto, I obtained my B.Math. in combinatorics, optimization, and computer science at the University of Waterloo.

When I'm not conducting research, I like to read, play board games, catch up on the latest video game, or travel. I also enjoy the occasional fishing or camping trip, and I have recently starting cycling.


Journal Publications

Lifting propositional proof compression algorithms to first-order logic. J. Gorzny, E. Postan, B. Woltzenlogel Paleo. Journal of Logic and Computation.

End-Vertices of LBFS of (AT-free) bigraphs. J. Gorzny and J. Huang. Discrete Applied Mathematics. [pdf]

Exact Values for the ε-ascent chromatic index of complete graphs. C. M. van Bommel and J. Gorzny. The Journal of Combinatorial Mathematics and Combinatorial Computing. [pdf]

Verification of uncertainty reducing model transformations. R. Salay, M. Chechik, M. Famelis, and J. Gorzny. The Journal of Object Technology. [pdf]

Conference & Workshop Papers

Computing Imbalance-Minimal Orderings for Bipartite Permutation Graphs and Threshold Graphs. Jan Gorzny. COCOA 2020. (Errata)

Constant-Time Updates Using Token Mechanics. Sebastian Banescu, Martin Derka, Jan Gorzny, Sung-Shine Lee, and Alex Murashkin. Blockchain 2020.

End-Vertices of AT-Free Bigraphs. Jan Gorzny and Jing Huang. COCOON 2020. (Errata)

Partial Regularization of First-Order Resolution Proofs. J. Gorzny, E. Postan, and B. Woltzenlogel Paleo. GCAI 2020 Best Paper Award

Imbalance, cutwidth, and the structure of optimal orderings. Jan Gorzny and Jonathan F. Buss. COCOON 2019. (Errata)

Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses. Jan Gorzny and Bruno Woltzenlogel Paleo. CADE 2015 [pdf | slides].

Change Propagation Due to Uncertainty Change. Rick Salay, Jan Gorzny, and Marsha Chechik. FASE 2013 [pdf].

Feature Interaction Analysis of the Feature-Oriented Requirements-Modelling Language Using Alloy. David Dietrich, Pourya Shaker, Joanne M. Atlee, Derek Rayside, and Jan Gorzny. MoDeVVa 2012 [pdf].

Comparing the Effectiveness of Reasoning Formalisms for Partial Models. Pooya Saadatpanah, Michalis Famelis, Jan Gorzny, Nathan Robinson, Marsha Chechik, and Rick Salay. MoDeVVa 2012 [pdf].

Towards a Methodology for Verifying Partial Model Refinements. Rick Salay, Marsha Chechik, and Jan Gorzny. VOLT 2012 [pdf].


On End Vertices of Search Algorithms. Jan Gorzny. M.Sc. Thesis, 2015, University of Victoria. [pdf]


Fundamentals of Smart Contract Security. Richard Ma, Jan Gorzny, Ed Zulkoski, Kacper Bak, and Olga V. Mack. Momentum Press, 2019.


Imbalance, Cutwidth, and the Structure of Optimal Orderings. J. Gorzny and J. Buss. DIMEA Days 2019, Brno, Czech Republic.

Partial Regularization of First-Order Resolution Proofs. J. Gorzny, E. Postan, and B. Woltzenlogel Paleo. User Interfaces for Theorem Provers, University of Oxford, Oxford, United Kingdom, 2018 and North American Summer School on Logic, Language, and Information, 2016.

Uncertainty management with partial models. M. Famelis, J. Gorzny, P. SaadatPanah, M. Chechik, and R. Salay. Research in Action Showcase, University of Toronto, Toronto, ON, Canada, 2012.

Feature-oriented modelling and analysis. J. M. Atlee, P. Shaker, and J. Gorzny CASCON, Toronto, ON, Canada, 2011.

JSCOOP: Simple concurrency for Java.J. Gorzny, F. Torshizi, and M. Chechik. Department Showcase, University of Toronto, Toronto, ON, Canada, 2010.