Exploiting structure in symmetry detection for CNF. - Paul T. Darga; Mark H. Liffiton; Karem A. Sakallah; Igor L. Markov (DAC, 2004)

Identifying Conflicts in Overconstrained Temporal Problems. - Mark H. Liffiton; Michael D. Moffitt; Martha E. Pollack; Karem A. Sakallah (IJCAI, 2005)

On Finding All Minimally Unsatisfiable Subformulas. - Mark H. Liffiton; Karem A. Sakallah (SAT, 2005)

Refinement strategies for verification methods based on datapath abstraction. - Zaher S. Andraus; Mark H. Liffiton; Karem A. Sakallah (ASP-DAC, 2006)

Improved Design Debugging Using Maximum Satisfiability. - Sean Safarpour; Hratch Mangassarian; Andreas G. Veneris; Mark H. Liffiton; Karem A. Sakallah (FMCAD, 2007)

Reveal: A Formal Verification Tool for Verilog Designs. - Zaher S. Andraus; Mark H. Liffiton; Karem A. Sakallah (LPAR, 2008)

Searching for Autarkies to Trim Unsatisfiable Clause Sets. - Mark H. Liffiton; Karem A. Sakallah (SAT, 2008)

Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. - Mark H. Liffiton; Karem A. Sakallah (J. Autom. Reason., 2008)

Generalizing Core-Guided Max-SAT. - Mark H. Liffiton; Karem A. Sakallah (SAT, 2009)

A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. - Mark H. Liffiton; Maher N. Mneimneh; Inês Lynce; Zaher S. Andraus; João Marques-Silva 001; Karem A. Sakallah (Constraints An Int. J., 2009)

Analyzing Infeasible Constraint Systems. - Mark H. Liffiton (2009)

MaxSAT-Based MCS Enumeration. - António Morgado 001; Mark H. Liffiton; João Marques-Silva 001 (Haifa Verification Conference, 2012)

A Cardinality Solver: More Expressive Constraints for Free - (Poster Presentation). - Mark H. Liffiton; Jordyn C. Maglalang (SAT, 2012)

Enumerating Infeasibility: Finding Multiple MUSes Quickly. - Mark H. Liffiton; Ammar Malik (CPAIOR, 2013)

Iterative and core-guided MaxSAT solving: A survey and assessment. - António Morgado 001; Federico Heras; Mark H. Liffiton; Jordi Planes; João Marques-Silva 001 (Constraints An Int. J., 2013)

Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets. - Bernard Blackham; Mark H. Liffiton; Gernot Heiser (RTAS, 2014)

Smallest MUS Extraction with Minimal Hitting Set Dualization. - Alexey Ignatiev; Alessandro Previti; Mark H. Liffiton; João Marques-Silva 001 (CP, 2015)

Parallelizing Partial MUS Enumeration. - Wenting Zhao 002; Mark H. Liffiton (ICTAI, 2016)

Fast, flexible MUS enumeration. - Mark H. Liffiton; Alessandro Previti; Ammar Malik; João Marques-Silva 001 (Constraints An Int. J., 2016)

Finding Graph Decompositions via SAT. - Wenting Zhao 002; Mark H. Liffiton; Peter Jeavons 001; Dan Roberts (ICTAI, 2017)

CodeHelp: Using Large Language Models with Guardrails for Scalable Support in Programming Classes. - Mark H. Liffiton; Brad E. Sheese; Jaromír Savelka; Paul Denny 001 (Koli Calling, 2023)

Efficient Classification of Student Help Requests in Programming Courses Using Large Language Models. - Jaromír Savelka; Paul Denny 001; Mark H. Liffiton; Brad Sheese (CoRR, 2023)

Patterns of Student Help-Seeking When Using a Large Language Model-Powered Programming Assistant. - Brad Sheese; Mark H. Liffiton; Jaromír Savelka; Paul Denny 001 (ACE, 2024)