| 2025 | CAV | QSM-Cutoff: Systematic Derivation of Quantified Cutoff Formulas for Distributed Protocols. | Yun-Rong Luo, Aman Goel, Karem A. Sakallah |
| 2024 | ISoLA | SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols: An Update. | Yun-Rong Luo, Aman Goel, Karem A. Sakallah |
| 2023 | FMCAD | SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols. | Katalin Fazekas, Aman Goel, Karem A. Sakallah |
| 2023 | FORTE | Towards an Automatic Proof of the Bakery Algorithm. | Aman Goel, Stephan Merz, Karem A. Sakallah |
| 2021 | FMCAD | Towards an Automatic Proof of Lamport's Paxos. | Aman Goel, Karem A. Sakallah |
| 2020 | FMCAD | EUFicient Reachability in Software with Arrays. | Denis Bueno, Arlen Cox, Karem A. Sakallah |
| 2020 | TACAS | AVR: Abstractly Verifying Reachability. | Aman Goel, Karem A. Sakallah |
| 2019 | DATE | Empirical Evaluation of IC3-Based Model Checking Techniques on Verilog RTL Designs. | Aman Goel, Karem A. Sakallah |
| 2019 | HotOS | Towards Automatic Inference of Inductive Invariants. | Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, Karem A. Sakallah |
| 2019 | SOSP | I4: incremental inference of inductive invariants for verification of distributed protocols. | Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, Karem A. Sakallah |
| 2019 | VMCAI | euforia: Complete Software Model Checking with Uninterpreted Functions. | Denis Bueno, Karem A. Sakallah |
| 2014 | CAV | Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction. | Suho Lee, Karem A. Sakallah |
| 2013 | ICCAD | Generalized Boolean symmetries through nested partition refinement. | Hadi Katebi, Karem A. Sakallah, Igor L. Markov |
| 2013 | ICTAI | Conflict Analysis and Branching Heuristics in the Search for Graph Automorphisms. | Paolo Codenotti, Hadi Katebi, Karem A. Sakallah, Igor L. Markov |
| 2013 | RAID | Detecting Traditional Packers, Decisively. | Denis Bueno, Kevin J. Compton, Karem A. Sakallah, Michael D. Bailey |
| 2012 | LPAR | Conflict Anticipation in the Search for Graph Automorphisms. | Hadi Katebi, Karem A. Sakallah, Igor L. Markov |
| 2011 | ACSAC | Distilling critical attack graph surface iteratively through minimum-cost SAT solving. | Heqing Huang, Su Zhang, Xinming Ou, Atul Prakash, Karem A. Sakallah |
| 2011 | SAT | Empirical Study of the Anatomy of Modern Sat Solvers. | Hadi Katebi, Karem A. Sakallah, Joo P. Marques Silva |
| 2010 | ICFEM | Trace-Driven Verification of Multithreaded Programs. | Zijiang Yang, Karem A. Sakallah |
| 2010 | SAT | Symmetry and Satisfiability: An Update. | Hadi Katebi, Karem A. Sakallah, Igor L. Markov |
| 2009 | IFM | Dynamic Path Reduction for Software Model Checking. | Zijiang Yang, Bashar Al-Rawi, Karem A. Sakallah, Xiaowan Huang, Scott A. Smolka, Radu Grosu |
| 2009 | SAT | Generalizing Core-Guided Max-SAT. | Mark H. Liffiton, Karem A. Sakallah |
| 2008 | DAC | Faster symmetry discovery using sparsity of symmetries. | Paul T. Darga, Karem A. Sakallah, Igor L. Markov |
| 2008 | LPAR | Reveal: A Formal Verification Tool for Verilog Designs. | Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah |
| 2008 | SAT | Searching for Autarkies to Trim Unsatisfiable Clause Sets. | Mark H. Liffiton, Karem A. Sakallah |
| 2007 | FMCAD | Improved Design Debugging Using Maximum Satisfiability. | Sean Safarpour, Hratch Mangassarian, Andreas G. Veneris, Mark H. Liffiton, Karem A. Sakallah |
| 2006 | ASPDAC | Refinement strategies for verification methods based on datapath abstraction. | Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah |
| 2006 | FMCAD | Ario: A Linear Integer Arithmetic Logic Solver. | Hossein M. Sheini, Karem A. Sakallah |
| 2006 | ICCAD | SMT( | Hossein M. Sheini, Karem A. Sakallah |
| 2006 | SAT | From Propositional Satisfiability to Satisfiability Modulo Theories. | Hossein M. Sheini, Karem A. Sakallah |
| 2006 | SAT | A Progressive Simplifier for Satisfiability Modulo Theories. | Hossein M. Sheini, Karem A. Sakallah |
| 2005 | ASPDAC | Dynamic symmetry-breaking for improved Boolean optimization. | Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah |
| 2005 | CP | On Solving Soft Temporal Constraints Using SAT Techniques. | Hossein M. Sheini, Bart Peintner, Karem A. Sakallah, Martha E. Pollack |
| 2005 | CPAIOR | A SAT-Based Decision Procedure for Mixed Logical/Integer Linear Problems. | Hossein M. Sheini, Karem A. Sakallah |
| 2005 | DATE | Pueblo: A Modern Pseudo-Boolean SAT Solver. | Hossein M. Sheini, Karem A. Sakallah |
| 2005 | IJCAI | Identifying Conflicts in Overconstrained Temporal Problems. | Mark H. Liffiton, Michael D. Moffitt, Martha E. Pollack, Karem A. Sakallah |
| 2005 | SAT | On Finding All Minimally Unsatisfiable Subformulas. | Mark H. Liffiton, Karem A. Sakallah |
| 2005 | SAT | A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas. | Maher N. Mneimneh, Ins Lynce, Zaher S. Andraus, Joo Marques-Silva, Karem A. Sakallah |
| 2005 | SAT | A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic. | Hossein M. Sheini, Karem A. Sakallah |
| 2004 | ASPDAC | ShatterPB: symmetry-breaking for pseudo-Boolean formulas. | Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah |
| 2004 | ASPDAC | Preserving synchronizing sequences of sequential circuits after retiming. | Maher N. Mneimneh, Karem A. Sakallah, John Moondanos |
| 2004 | DAC | Automatic abstraction and verification of verilog models. | Zaher S. Andraus, Karem A. Sakallah |
| 2004 | DAC | Exploiting structure in symmetry detection for CNF. | Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah, Igor L. Markov |
| 2004 | DAC | AMUSE: a minimally-unsatisfiable subformula extractor. | Yoonna Oh, Maher N. Mneimneh, Zaher S. Andraus, Karem A. Sakallah, Igor L. Markov |
| 2004 | DATE | Breaking Instance-Independent Symmetries in Exact Graph Coloring. | Arathi Ramani, Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah |
| 2003 | ASPDAC | SAT-based sequential depth computation. | Maher N. Mneimneh, Karem A. Sakallah |
| 2003 | DAC | Shatter: efficient symmetry-breaking for boolean satisfiability. | Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah |
| 2003 | IJCAI | Efficient Symmetry Breaking for Boolean Satisfiability. | Fadi A. Aloul, Karem A. Sakallah, Igor L. Markov |
| 2003 | SAT | Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution. | Maher N. Mneimneh, Karem A. Sakallah |
| 2002 | DAC | Solving difficult SAT instances in the presence of symmetry. | Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah |
| 2002 | DAC | Satometer: how much have we searched? | Fadi A. Aloul, Brian D. Sierawski, Karem A. Sakallah |
| 2002 | DATE | Search-Based SAT Using Zero-Suppressed BDDs. | Fadi A. Aloul, Maher N. Mneimneh, Karem A. Sakallah |
| 2002 | FPL | Hybrid Routing for FPGAs by Integrating Boolean Satisfiability with Geometric Search. | Gi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar |
| 2002 | ICCAD | Generic ILP versus specialized 0-1 ILP: an update. | Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah |
| 2002 | ICCAD | Resynthesis of multi-level circuits under tight constraints using symbolic optimization. | Victor N. Kravets, Karem A. Sakallah |
| 2002 | ICCD | Improving the Efficiency of Circuit-to-BDD Conversion by Gate and Input Ordering. | Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah |
| 2001 | DAC | Scalable Hybrid Verification of Complex Microprocessors. | Maher N. Mneimneh, Fadi A. Aloul, Christopher T. Weaver, Saugata Chatterjee, Karem A. Sakallah, Todd M. Austin |
| 2001 | DAC | SATIRE: A New Incremental Satisfiability Engine. | Jesse Whittemore, Joonyoung Kim, Karem A. Sakallah |
| 2001 | DAC | An Advanced Timing Characterization Method Using Mode Dependency. | Hakan Yalcin, Robert Palermo, Mohammad Mortazavi, Cyrus Bamji, Karem A. Sakallah, John P. Hayes |
| 2001 | DATE | A boolean satisfiability-based incremental rerouting approach with application to FPGAs. | Gi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar |
| 2001 | ICCAD | Faster SAT and Smaller BDDs via Common Function Structure. | Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah |
| 2000 | CAV | Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation. | Joo Marques-Silva, Karem A. Sakallah |
| 2000 | DAC | Boolean satisfiability in electronic design automation. | Joo P. Marques Silva, Karem A. Sakallah |
| 2000 | DATE | On Applying Incremental Satisfiability to Delay Fault Testing. | Joonyoung Kim, Jesse Whittemore, Karem A. Sakallah, Joo P. Marques Silva |
| 2000 | DATE | Constructive Library-Aware Synthesis Using Symmetries. | Victor N. Kravets, Karem A. Sakallah |
| 2000 | DATE | An Experimental Study of Satisfiability Search Heuristics. | Karem A. Sakallah, Fadi A. Aloul, Joo P. Marques Silva |
| 2000 | ICCAD | Generalized Symmetries in Boolean Functions. | Victor N. Kravets, Karem A. Sakallah |
| 2000 | ICCD | On Solving Stack-Based Incremental Satisfiability Problems. | Joonyoung Kim, Jesse Whittemore, Karem A. Sakallah |
| 1999 | DAC | Functional Timing Analysis for IP Characterization. | Hakan Yalcin, Mohammad Mortazavi, Robert Palermo, Cyrus Bamji, Karem A. Sakallah |
| 1999 | FPGA | Satisfiability-Based Layout Revisited: Detailed Routing of Complex FPGAs vis Search-Based Boolean SAT. | Gi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar |
| 1999 | VLSID | Satisfiability-Based Detailed FPGA Routing. | Gi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar |
| 1998 | DAC | M32: A Constructive multilevel Logic Synthesis System. | Victor N. Kravets, Karem A. Sakallah |
| 1998 | DAC | Congestion Driven Quadratic Placement. | Phiroze N. Parakh, Richard B. Brown, Karem A. Sakallah |
| 1998 | DATE | AFTA: A Formal Delay Model for Functional Timing Analysis. | V. Chandramouli, Jesse Whittemore, Karem A. Sakallah |
| 1996 | DAC | Modeling the Effects of Temporal Proximity of Input Transitions on Gate Propagation Delay and Transition Time. | V. Chandramouli, Karem A. Sakallah |
| 1996 | ICCAD | Timing verification of sequential domino circuits. | David Van Campenhout, Trevor N. Mudge, Karem A. Sakallah |
| 1996 | ICCAD | GRASP - a new search algorithm for satisfiability. | Joo P. Marques Silva, Karem A. Sakallah |
| 1996 | ICCAD | An approximate timing analysis method for datapath circuits. | Hakan Yalcin, John P. Hayes, Karem A. Sakallah |
| 1996 | ICTAI | Conflict Analysis in Search Algorithms for Satisfiability. | Joo P. Marques Silva, Karem A. Sakallah |
| 1995 | DAC | The Aurora RAM Compiler. | Ajay Chandna, C. David Kibler, Richard B. Brown, Mark Roberts, Karem A. Sakallah |
| 1994 | DAC | Dynamic Search-Space Pruning Techniques in Path Sensitization. | Joo P. Marques Silva, Karem A. Sakallah |
| 1994 | ICCAD | Optimization of critical paths in circuits with level-sensitive latches. | Timothy M. Burks, Karem A. Sakallah |
| 1994 | ISCAS | Macromodel Simplification Using Dimensional Analysis. | Ayman I. Kayssi, Karem A. Sakallah |
| 1994 | ISCAS | Efficient and Robust Test Generation-Based Timing Analysis. | Joo P. Marques Silva, Karem A. Sakallah |
| 1993 | ICCAD | Min-max linear programming and the timing analysis of digital circuits. | Timothy M. Burks, Karem A. Sakallah |
| 1993 | ICCD | Ravel-XL: A Hardware Accelerator for Assigned-Delay Compiled-Code Logic Gate Simulation. | Michael A. Riepe, Joo P. Marques Silva, Karem A. Sakallah, Richard B. Brown |
| 1993 | ICCD | An Analysis of Path Sensitization Criteria. | Joo P. Marques Silva, Karem A. Sakallah |
| 1992 | ICCAD | Identification of critical paths in circuits with level-sensitive latches. | Timothy M. Burks, Karem A. Sakallah, Trevor N. Mudge |
| 1992 | ICCAD | Using constraint geometry to determine maximum rate pipeline clocking. | Chuan-Hua Chang, Edward S. Davidson, Karem A. Sakallah |
| 1992 | ICCAD | Ravel: assigned-delay compiled-code logic simulation. | Emily J. Shriver, Karem A. Sakallah |
| 1991 | ICCAD | FPD - An Environment for Exact Timing Analysis. | Joo P. Marques Silva, Karem A. Sakallah, Lus M. Vidigal |
| 1991 | ICCD | Optimal Clocking of Circular Pipelines. | Karem A. Sakallah, Trevor N. Mudge, Timothy M. Burks, Edward S. Davidson |
| 1990 | DAC | Analysis and Design of Latch-Controlled Synchronous Digital Circuits. | Karem A. Sakallah, Trevor N. Mudge, Kunle Olukotun |
| 1990 | ICCAD | Untitled record | Karem A. Sakallah, Trevor N. Mudge, Kunle Olukotun |