SAMSON2: An Event Driven VLSI Circuit Simulator. - Karem A. Sakallah; Stephen W. Director (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1985)

check Tc and min Tc: Timing Verification and Optimal Clocking of Synchronous Digtal Circuits. - Karem A. Sakallah; Trevor N. Mudge; Kunle Olukotun (ICCAD, 1990)

Clock Qualification Algorithm for Timing Analysis of Custom CMOS VLSI Circuits with Overlapped Clocking Disciplines and On-section Clock Derivation. - Somanathan C. Menon; Karem A. Sakallah (ICSI, 1990)

A first-order charge conserving MOS capacitance model. - Karem A. Sakallah; Yao-Tsung Yen; Steve S. Greenberg (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1990)

FPD - An Environment for Exact Timing Analysis. - João P. Marques Silva; Karem A. Sakallah; Luís M. Vidigal (ICCAD, 1991)

Optimal Clocking of Circular Pipelines. - Karem A. Sakallah; Trevor N. Mudge; Timothy M. Burks; Edward S. Davidson (ICCD, 1991)

The Design of a Microsupercomputer. - Trevor N. Mudge; Richard B. Brown; William P. Bimingham; Jeffrey A. Dykstra; Ayman I. Kayssi; Ronald J. Lomax; Kunle Olukotun; Karem A. Sakallah; Raymond A. Milano (Computer, 1991)

Multilevel optimization in the design of a high-performance GaAs microcomputer. - Oyekunle A. Olukotun; Richard B. Brown; Ronald J. Lomax; Trevor N. Mudge; Karem A. Sakallah (IEEE J. Solid State Circuits, 1991)

Delay macromodels for the timing analysis of GaAs DCFL. - Ayman I. Kayssi; Karem A. Sakallah (EURO-DAC, 1992)

Identification of critical paths in circuits with level-sensitive latches. - Timothy M. Burks; Karem A. Sakallah; Trevor N. Mudge (ICCAD, 1992)

Using constraint geometry to determine maximum rate pipeline clocking. - Chuan-Hua Chang; Edward S. Davidson; Karem A. Sakallah (ICCAD, 1992)

Ravel: assigned-delay compiled-code logic simulation. - Emily J. Shriver; Karem A. Sakallah (ICCAD, 1992)

Analysis and design of latch-controlled synchronous digital circuits. - Karem A. Sakallah; Trevor N. Mudge; Oyekunle A. Olukotun (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1992)

Concurrent path sensitization in timing analysis. - João P. Marques Silva; Karem A. Sakallah (EURO-DAC, 1993)

Min-max linear programming and the timing analysis of digital circuits. - Timothy M. Burks; Karem A. Sakallah (ICCAD, 1993)

An Analysis of Path Sensitization Criteria. - João P. Marques Silva; Karem A. Sakallah (ICCD, 1993)

Synchronization of pipelines. - Karem A. Sakallah; Trevor N. Mudge; Timothy M. Burks; Edward S. Davidson (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1993)

Dynamic Search-Space Pruning Techniques in Path Sensitization. - João P. Marques Silva; Karem A. Sakallah (DAC, 1994)

Optimization of critical paths in circuits with level-sensitive latches. - Timothy M. Burks; Karem A. Sakallah (ICCAD, 1994)

Macromodel Simplification Using Dimensional Analysis. - Ayman I. Kayssi; Karem A. Sakallah (ISCAS, 1994)

Efficient and Robust Test Generation-Based Timing Analysis. - João P. Marques Silva; Karem A. Sakallah (ISCAS, 1994)

The Aurora RAM Compiler. - Ajay Chandna; C. David Kibler; Richard B. Brown; Mark Roberts; Karem A. Sakallah (DAC, 1995)

Maximum rate single-phase clocking of a closed pipeline including wave pipelining, stoppability, and startability. - Chuan-Hua Chang; Edward S. Davidson; Karem A. Sakallah (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1995)

Timing models for gallium arsenide direct-coupled FET logic circuits. - Ayman I. Kayssi; Karem A. Sakallah (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1995)

Critical paths in circuits with level-sensitive latches. - Timothy M. Burks; Karem A. Sakallah; Trevor N. Mudge (IEEE Trans. Very Large Scale Integr. Syst., 1995)

Modeling the Effects of Temporal Proximity of Input Transitions on Gate Propagation Delay and Transition Time. - V. Chandramouli; Karem A. Sakallah (DAC, 1996)

Timing verification of sequential domino circuits. - David Van Campenhout; Trevor N. Mudge; Karem A. Sakallah (ICCAD, 1996)

GRASP - a new search algorithm for satisfiability. - João P. Marques Silva; Karem A. Sakallah (ICCAD, 1996)

An approximate timing analysis method for datapath circuits. - Hakan Yalcin; John P. Hayes; Karem A. Sakallah (ICCAD, 1996)

Conflict Analysis in Search Algorithms for Satisfiability. - João P. Marques Silva; Karem A. Sakallah (ICTAI, 1996)

Ravel-XL: a hardware accelerator for assigned-delay compiled-code logic gate simulation. - Michael A. Riepe; João P. Marques Silva; Karem A. Sakallah; Richard B. Brown (IEEE Trans. Very Large Scale Integr. Syst., 1996)

Signal Delay in Coupled, Distributed RC Lines in the Presence of Temporal Proximity. - V. Chandramouli; Karem A. Sakallah; Ayman I. Kayssi (ARVLSI, 1997)

Robust Search Algorithms for Test Pattern Generation. - João P. Marques Silva; Karem A. Sakallah (FTCS, 1997)

M32: A Constructive multilevel Logic Synthesis System. - Victor N. Kravets; Karem A. Sakallah (DAC, 1998)

Congestion Driven Quadratic Placement. - Phiroze N. Parakh; Richard B. Brown; Karem A. Sakallah (DAC, 1998)

AFTA: A Formal Delay Model for Functional Timing Analysis. - V. Chandramouli; Jesse Whittemore; Karem A. Sakallah (DATE, 1998)

Timing analysis using propositional satisfiability. - Luís Guerra e Silva; João P. Marques Silva; Luís Miguel Silveira; Karem A. Sakallah (ICECS, 1998)

The edge-based design rule model revisited. - Michael A. Riepe; Karem A. Sakallah (ACM Trans. Design Autom. Electr. Syst., 1998)

Overview of complementary GaAs technology for high-speed VLSI circuits. - Richard B. Brown; Bruce Bernhardt; M. LaMacchia; J. Abrokwah; Phiroze N. Parakh; Todd D. Basso; Spencer M. Gold; S. Stetson; Claude R. Gauthier; D. Foster; B. Crawforth; T. McQuire; et al. (IEEE Trans. Very Large Scale Integr. Syst., 1998)

Functional Timing Analysis for IP Characterization. - Hakan Yalcin; Mohammad Mortazavi; Robert Palermo; Cyrus Bamji; Karem A. Sakallah (DAC, 1999)

Satisfiability-Based Layout Revisited: Detailed Routing of Complex FPGAs vis Search-Based Boolean SAT. - Gi-Joon Nam; Karem A. Sakallah; Rob A. Rutenbar (FPGA, 1999)

Satisfiability-Based Functional Delay Fault Testing. - Joonyoung Kim; João Marques-Silva 001; Karem A. Sakallah (VLSI, 1999)

Transistor level micro-placement and routing for two-dimensional digital VLSI cell synthesis. - Michael A. Riepe; Karem A. Sakallah (ISPD, 1999)

Satisfiability-Based Detailed FPGA Routing. - Gi-Joon Nam; Karem A. Sakallah; Rob A. Rutenbar (VLSI Design, 1999)

GRASP: A Search Algorithm for Propositional Satisfiability. - João P. Marques Silva; Karem A. Sakallah (IEEE Trans. Computers, 1999)

Timing verification of sequential dynamic circuits. - David Van Campenhout; Trevor N. Mudge; Karem A. Sakallah (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999)

Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation. - João Marques-Silva 001; Karem A. Sakallah (CAV, 2000)

Boolean satisfiability in electronic design automation. - João P. Marques Silva; Karem A. Sakallah (DAC, 2000)

On Applying Incremental Satisfiability to Delay Fault Testing. - Joonyoung Kim; Jesse Whittemore; Karem A. Sakallah; João P. Marques Silva (DATE, 2000)

Constructive Library-Aware Synthesis Using Symmetries. - Victor N. Kravets; Karem A. Sakallah (DATE, 2000)

An Experimental Study of Satisfiability Search Heuristics. - Karem A. Sakallah; Fadi A. Aloul; João P. Marques Silva (DATE, 2000)

Generalized Symmetries in Boolean Functions. - Victor N. Kravets; Karem A. Sakallah (ICCAD, 2000)

On Solving Stack-Based Incremental Satisfiability Problems. - Joonyoung Kim; Jesse Whittemore; Karem A. Sakallah (ICCD, 2000)

Scalable Hybrid Verification of Complex Microprocessors. - Maher N. Mneimneh; Fadi A. Aloul; Christopher T. Weaver; Saugata Chatterjee; Karem A. Sakallah; Todd M. Austin (DAC, 2001)

SATIRE: A New Incremental Satisfiability Engine. - Jesse Whittemore; Joonyoung Kim; Karem A. Sakallah (DAC, 2001)

An Advanced Timing Characterization Method Using Mode Dependency. - Hakan Yalcin; Robert Palermo; Mohammad Mortazavi; Cyrus Bamji; Karem A. Sakallah; John P. Hayes (DAC, 2001)

A boolean satisfiability-based incremental rerouting approach with application to FPGAs. - Gi-Joon Nam; Karem A. Sakallah; Rob A. Rutenbar (DATE, 2001)

Faster SAT and Smaller BDDs via Common Function Structure. - Fadi A. Aloul; Igor L. Markov; Karem A. Sakallah (ICCAD, 2001)

Fast and accurate timing characterization using functionalinformation. - Hakan Yalcin; Mohammad Mortazavi; Robert Palermo; Cyrus Bamji; Karem A. Sakallah; John P. Hayes (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2001)

Solving difficult SAT instances in the presence of symmetry. - Fadi A. Aloul; Arathi Ramani; Igor L. Markov; Karem A. Sakallah (DAC, 2002)

Search-Based SAT Using Zero-Suppressed BDDs. - Fadi A. Aloul; Maher N. Mneimneh; Karem A. Sakallah (DATE, 2002)

Hybrid Routing for FPGAs by Integrating Boolean Satisfiability with Geometric Search. - Gi-Joon Nam; Karem A. Sakallah; Rob A. Rutenbar (FPL, 2002)

Generic ILP versus specialized 0-1 ILP: an update. - Fadi A. Aloul; Arathi Ramani; Igor L. Markov; Karem A. Sakallah (ICCAD, 2002)

Resynthesis of multi-level circuits under tight constraints using symbolic optimization. - Victor N. Kravets; Karem A. Sakallah (ICCAD, 2002)

Improving the Efficiency of Circuit-to-BDD Conversion by Gate and Input Ordering. - Fadi A. Aloul; Igor L. Markov; Karem A. Sakallah (ICCD, 2002)

ZBDD-Based Backtrack Search SAT Solver. - Fadi A. Aloul; Maher N. Mneimneh; Karem A. Sakallah (IWLS, 2002)

Efficient Gate and Input Ordering for Circuit-to-BDD Conversion. - Fadi A. Aloul; Igor L. Markov; Karem A. Sakallah (IWLS, 2002)

Majority-Based Decomposition of Carry Logic in Binary Adders. - Leyla Nazhandali; Karem A. Sakallah (IWLS, 2002)

Robust SAT-Based Search Algorithm for Leakage Power Reduction. - Fadi A. Aloul; Soha Hassoun; Karem A. Sakallah; David T. Blaauw (PATMOS, 2002)

A new FPGA detailed routing approach via search-based Booleansatisfiability. - Gi-Joon Nam; Karem A. Sakallah; Rob A. Rutenbar (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2002)

Satisfiability models and algorithms for circuit delay computation. - Luís Guerra e Silva; João Marques-Silva 001; Luís Miguel Silveira; Karem A. Sakallah (ACM Trans. Design Autom. Electr. Syst., 2002)

SAT-based sequential depth computation. - Maher N. Mneimneh; Karem A. Sakallah (ASP-DAC, 2003)

Shatter: efficient symmetry-breaking for boolean satisfiability. - Fadi A. Aloul; Igor L. Markov; Karem A. Sakallah (DAC, 2003)

FORCE: a fast and easy-to-implement variable-ordering heuristic. - Fadi A. Aloul; Igor L. Markov; Karem A. Sakallah (ACM Great Lakes Symposium on VLSI, 2003)

Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution. - Maher N. Mneimneh; Karem A. Sakallah (SAT, 2003)

Solving difficult instances of Boolean satisfiability in the presence of symmetry. - Fadi A. Aloul; Arathi Ramani; Igor L. Markov; Karem A. Sakallah (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2003)

Satometer: how much have we searched? - Fadi A. Aloul; Brian D. Sierawski; Karem A. Sakallah (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2003)

sub-SAT: a formulation for relaxed Boolean satisfiability with applications in routing. - Hui Xu 001; Rob A. Rutenbar; Karem A. Sakallah (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2003)

Transistor placement for noncomplementary digital VLSI cell synthesis. - Michael A. Riepe; Karem A. Sakallah (ACM Trans. Design Autom. Electr. Syst., 2003)

ShatterPB: symmetry-breaking for pseudo-Boolean formulas. - Fadi A. Aloul; Arathi Ramani; Igor L. Markov; Karem A. Sakallah (ASP-DAC, 2004)

Preserving synchronizing sequences of sequential circuits after retiming. - Maher N. Mneimneh; Karem A. Sakallah; John Moondanos (ASP-DAC, 2004)

Automatic abstraction and verification of verilog models. - Zaher S. Andraus; Karem A. Sakallah (DAC, 2004)

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

AMUSE: a minimally-unsatisfiable subformula extractor. - Yoonna Oh; Maher N. Mneimneh; Zaher S. Andraus; Karem A. Sakallah; Igor L. Markov (DAC, 2004)

MINCE: A Static Global Variable-Ordering Heuristic for SAT Search and BDD Manipulation. - Fadi A. Aloul; Igor L. Markov; Karem A. Sakallah (J. Univers. Comput. Sci., 2004)

A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints. - Gi-Joon Nam; Fadi A. Aloul; Karem A. Sakallah; Rob A. Rutenbar (IEEE Trans. Computers, 2004)

Dynamic symmetry-breaking for improved Boolean optimization. - Fadi A. Aloul; Arathi Ramani; Igor L. Markov; Karem A. Sakallah (ASP-DAC, 2005)

On Solving Soft Temporal Constraints Using SAT Techniques. - Hossein M. Sheini; Bart Peintner; Karem A. Sakallah; Martha E. Pollack (CP, 2005)

A SAT-Based Decision Procedure for Mixed Logical/Integer Linear Problems. - Hossein M. Sheini; Karem A. Sakallah (CPAIOR, 2005)

Pueblo: A Modern Pseudo-Boolean SAT Solver. - Hossein M. Sheini; Karem A. Sakallah (DATE, 2005)

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)

A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas. - Maher N. Mneimneh; Inês Lynce; Zaher S. Andraus; João Marques-Silva 001; Karem A. Sakallah (SAT, 2005)

A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic. - Hossein M. Sheini; Karem A. Sakallah (SAT, 2005)

Principles of Sequential-Equivalence Verification. - Maher N. Mneimneh; Karem A. Sakallah (IEEE Des. Test Comput., 2005)

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

Ario: A Linear Integer Arithmetic Logic Solver. - Hossein M. Sheini; Karem A. Sakallah (FMCAD, 2006)

SMT(CLU): a step toward scalability in system verification. - Hossein M. Sheini; Karem A. Sakallah (ICCAD, 2006)

From Propositional Satisfiability to Satisfiability Modulo Theories. - Hossein M. Sheini; Karem A. Sakallah (SAT, 2006)

A Progressive Simplifier for Satisfiability Modulo Theories. - Hossein M. Sheini; Karem A. Sakallah (SAT, 2006)

Breaking Instance-Independent Symmetries In Exact Graph Coloring. - Arathi Ramani; Igor L. Markov; Karem A. Sakallah; Fadi A. Aloul (J. Artif. Intell. Res., 2006)

Pueblo: A Hybrid Pseudo-Boolean SAT Solver. - Hossein M. Sheini; Karem A. Sakallah (J. Satisf. Boolean Model. Comput., 2006)

Efficient Symmetry Breaking for Boolean Satisfiability. - Fadi A. Aloul; Karem A. Sakallah; Igor L. Markov (IEEE Trans. Computers, 2006)

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

Report on the SAT 2007 Conference on Theory and Applications of Satisfiability Testing. - João Marques-Silva 001; Karem A. Sakallah; Inês Lynce (AI Mag., 2007)

Symmetry breaking for pseudo-Boolean formulas. - Fadi A. Aloul; Arathi Ramani; Igor L. Markov; Karem A. Sakallah (ACM J. Exp. Algorithmics, 2007)

Solution and Optimization of Systems of Pseudo-Boolean Constraints. - Fadi A. Aloul; Arathi Ramani; Karem A. Sakallah; Igor L. Markov (IEEE Trans. Computers, 2007)

Faster symmetry discovery using sparsity of symmetries. - Paul T. Darga; Karem A. Sakallah; Igor L. Markov (DAC, 2008)

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)

Dynamic Path Reduction for Software Model Checking. - Zijiang Yang 006; Bashar Al-Rawi; Karem A. Sakallah; Xiaowan Huang; Scott A. Smolka; Radu Grosu (IFM, 2009)

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

Dynamic symmetry-breaking for Boolean satisfiability. - Fadi A. Aloul; Arathi Ramani; Igor L. Markov; Karem A. Sakallah (Ann. Math. Artif. Intell., 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)

Symmetry and Satisfiability. - Karem A. Sakallah (Handbook of Satisfiability, 2009)

Incorporating user control in automated interactive scheduling systems. - Jina Huh; Martha E. Pollack; Hadi Katebi; Karem A. Sakallah; Ned Kirsch (Conference on Designing Interactive Systems, 2010)

Trace-Driven Verification of Multithreaded Programs. - Zijiang Yang 006; Karem A. Sakallah (ICFEM, 2010)

Symmetry and Satisfiability: An Update. - Hadi Katebi; Karem A. Sakallah; Igor L. Markov (SAT, 2010)

Distilling critical attack graph surface iteratively through minimum-cost SAT solving. - Heqing Huang; Su Zhang; Xinming Ou; Atul Prakash 001; Karem A. Sakallah (ACSAC, 2011)

Generating Data Race Witnesses by an SMT-Based Analysis. - Mahmoud Said; Chao Wang 001; Zijiang Yang 006; Karem A. Sakallah (NASA Formal Methods, 2011)

Empirical Study of the Anatomy of Modern Sat Solvers. - Hadi Katebi; Karem A. Sakallah; João P. Marques Silva (SAT, 2011)

Anatomy and Empirical Evaluation of Modern SAT Solvers. - Karem A. Sakallah; João Marques-Silva 001 (Bull. EATCS, 2011)

Graph Symmetry Detection and Canonical Labeling: Differences and Synergies. - Hadi Katebi; Karem A. Sakallah; Igor L. Markov (Turing-100, 2012)

Conflict Anticipation in the Search for Graph Automorphisms. - Hadi Katebi; Karem A. Sakallah; Igor L. Markov (LPAR, 2012)

Generalized Boolean symmetries through nested partition refinement. - Hadi Katebi; Karem A. Sakallah; Igor L. Markov (ICCAD, 2013)

Conflict Analysis and Branching Heuristics in the Search for Graph Automorphisms. - Paolo Codenotti; Hadi Katebi; Karem A. Sakallah; Igor L. Markov (ICTAI, 2013)

Detecting Traditional Packers, Decisively. - Denis Bueno; Kevin J. Compton; Karem A. Sakallah; Michael D. Bailey (RAID, 2013)

Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction. - Suho Lee; Karem A. Sakallah (CAV, 2014)

Empirical Evaluation of IC3-Based Model Checking Techniques on Verilog RTL Designs. - Aman Goel; Karem A. Sakallah (DATE, 2019)

Towards Automatic Inference of Inductive Invariants. - Haojun Ma; Aman Goel; Jean-Baptiste Jeannin; Manos Kapritsos; Baris Kasikci; Karem A. Sakallah (HotOS, 2019)

Model Checking of Verilog RTL Using IC3 with Syntax-Guided Abstraction. - Aman Goel; Karem A. Sakallah (NFM, 2019)

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 (SOSP, 2019)

euforia: Complete Software Model Checking with Uninterpreted Functions. - Denis Bueno; Karem A. Sakallah (VMCAI, 2019)

EUFicient Reachability in Software with Arrays. - Denis Bueno; Arlen Cox; Karem A. Sakallah (FMCAD, 2020)

AVR: Abstractly Verifying Reachability. - Aman Goel; Karem A. Sakallah (TACAS (1), 2020)

Towards an Automatic Proof of Lamport's Paxos. - Aman Goel; Karem A. Sakallah (FMCAD, 2021)

On Symmetry and Quantification: A New Approach to Verify Distributed Protocols. - Aman Goel; Karem A. Sakallah (NFM, 2021)

Invited Talk: AVR: Word-Level Verification by Equality Abstraction of Data State. - Karem A. Sakallah (SMT, 2021)

Symmetry and Satisfiability. - Karem A. Sakallah (Handbook of Satisfiability, 2021)

SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols. - Katalin Fazekas; Aman Goel; Karem A. Sakallah (FMCAD, 2023)

Towards an Automatic Proof of the Bakery Algorithm. - Aman Goel; Stephan Merz; Karem A. Sakallah (FORTE, 2023)

Regularity and quantification: a new approach to verify distributed protocols. - Aman Goel; Karem A. Sakallah (Innov. Syst. Softw. Eng., 2023)

SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols: An Update. - Yun-Rong Luo; Aman Goel; Karem A. Sakallah (ISoLA (3), 2024)

QSM-Cutoff: Systematic Derivation of Quantified Cutoff Formulas for Distributed Protocols. - Yun-Rong Luo; Aman Goel; Karem A. Sakallah (CAV (3), 2025)