Karem A. Sakallah

ORCID

Publication Activity (10 Years)

Years Active: 1985-2023
Publications (10 Years): 15

Top Venues

Publications

Aman Goel, Karem A. Sakallah
Regularity and quantification: a new approach to verify distributed protocols. Innov. Syst. Softw. Eng. 19 (4) (2023)
Katalin Fazekas, Aman Goel, Karem A. Sakallah
SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols. FMCAD (2023)
Aman Goel, Stephan Merz, Karem A. Sakallah
Towards an Automatic Proof of the Bakery Algorithm. FORTE (2023)
Aman Goel, Karem A. Sakallah
On Symmetry and Quantification: A New Approach to Verify Distributed Protocols. NFM (2021)
Aman Goel, Karem A. Sakallah
Towards an Automatic Proof of Lamport's Paxos. CoRR (2021)
Karem A. Sakallah
Invited Talk: AVR: Word-Level Verification by Equality Abstraction of Data State. SMT (2021)
Aman Goel, Karem A. Sakallah
On Symmetry and Quantification: A New Approach to Verify Distributed Protocols. CoRR (2021)
Aman Goel, Karem A. Sakallah
Towards an Automatic Proof of Lamport's Paxos. FMCAD (2021)
Aman Goel, Karem A. Sakallah
AVR: Abstractly Verifying Reachability. TACAS (1) (2020)
Denis Bueno, Arlen Cox, Karem A. Sakallah
EUFicient Reachability in Software with Arrays. FMCAD (2020)
Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, Karem A. Sakallah
Towards Automatic Inference of Inductive Invariants. HotOS (2019)
Aman Goel, Karem A. Sakallah
Model Checking of Verilog RTL Using IC3 with Syntax-Guided Abstraction. NFM (2019)
Denis Bueno, Karem A. Sakallah
euforia: Complete Software Model Checking with Uninterpreted Functions. VMCAI (2019)
Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, Karem A. Sakallah
I4: incremental inference of inductive invariants for verification of distributed protocols. SOSP (2019)
Aman Goel, Karem A. Sakallah
Empirical Evaluation of IC3-Based Model Checking Techniques on Verilog RTL Designs. DATE (2019)
Suho Lee, Karem A. Sakallah
Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction. CAV (2014)
Paolo Codenotti, Hadi Katebi, Karem A. Sakallah, Igor L. Markov
Conflict Analysis and Branching Heuristics in the Search for Graph Automorphisms. ICTAI (2013)
Denis Bueno, Kevin J. Compton, Karem A. Sakallah, Michael Bailey
Detecting Traditional Packers, Decisively. RAID (2013)
Hadi Katebi, Karem A. Sakallah, Igor L. Markov
Generalized Boolean symmetries through nested partition refinement. ICCAD (2013)
Hadi Katebi, Karem A. Sakallah, Igor L. Markov
Conflict Anticipation in the Search for Graph Automorphisms. LPAR (2012)
Hadi Katebi, Karem A. Sakallah, Igor L. Markov
Graph Symmetry Detection and Canonical Labeling: Differences and Synergies. Turing-100 (2012)
Hadi Katebi, Karem A. Sakallah, Igor L. Markov
Graph Symmetry Detection and Canonical Labeling: Differences and Synergies CoRR (2012)
Hadi Katebi, Karem A. Sakallah, Igor L. Markov
Conflict Anticipation in the Search for Graph Automorphisms CoRR (2012)
Heqing Huang, Su Zhang, Xinming Ou, Atul Prakash, Karem A. Sakallah
Distilling critical attack graph surface iteratively through minimum-cost SAT solving. ACSAC (2011)
Hadi Katebi, Karem A. Sakallah, João P. Marques Silva
Empirical Study of the Anatomy of Modern Sat Solvers. SAT (2011)
Mahmoud Said, Chao Wang, Zijiang Yang, Karem A. Sakallah
Generating Data Race Witnesses by an SMT-Based Analysis. NASA Formal Methods (2011)
Karem A. Sakallah, João Marques-Silva
Anatomy and Empirical Evaluation of Modern SAT Solvers. Bull. EATCS 103 (2011)
Fadi A. Aloul, Igor L. Markov, Arathi Ramani, Karem A. Sakallah
Breaking Instance-Independent Symmetries In Exact Graph Coloring CoRR (2011)
Hadi Katebi, Karem A. Sakallah, Igor L. Markov
Symmetry and Satisfiability: An Update. SAT (2010)
Jina Huh, Martha E. Pollack, Hadi Katebi, Karem A. Sakallah, Ned Kirsch
Incorporating user control in automated interactive scheduling systems. Conference on Designing Interactive Systems (2010)
Zijiang Yang, Karem A. Sakallah
Trace-Driven Verification of Multithreaded Programs. ICFEM (2010)
Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah
Dynamic symmetry-breaking for Boolean satisfiability. Ann. Math. Artif. Intell. 57 (1) (2009)
Mark H. Liffiton, Maher N. Mneimneh, Inês Lynce, Zaher S. Andraus, João Marques-Silva, Karem A. Sakallah
A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints An Int. J. 14 (4) (2009)
Mark H. Liffiton, Karem A. Sakallah
Generalizing Core-Guided Max-SAT. SAT (2009)
Zijiang Yang, Bashar Al-Rawi, Karem A. Sakallah, Xiaowan Huang, Scott A. Smolka, Radu Grosu
Dynamic Path Reduction for Software Model Checking. IFM (2009)
Mark H. Liffiton, Karem A. Sakallah
Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. J. Autom. Reason. 40 (1) (2008)
Paul T. Darga, Karem A. Sakallah, Igor L. Markov
Faster symmetry discovery using sparsity of symmetries. DAC (2008)
Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah
Reveal: A Formal Verification Tool for Verilog Designs. LPAR (2008)
Mark H. Liffiton, Karem A. Sakallah
Searching for Autarkies to Trim Unsatisfiable Clause Sets. SAT (2008)
Fadi A. Aloul, Arathi Ramani, Karem A. Sakallah, Igor L. Markov
Solution and Optimization of Systems of Pseudo-Boolean Constraints. IEEE Trans. Computers 56 (10) (2007)
Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah
Symmetry breaking for pseudo-Boolean formulas. ACM J. Exp. Algorithmics 12 (2007)
João Marques-Silva, Karem A. Sakallah, Inês Lynce
Report on the SAT 2007 Conference on Theory and Applications of Satisfiability Testing. AI Mag. 28 (4) (2007)
Sean Safarpour, Hratch Mangassarian, Andreas G. Veneris, Mark H. Liffiton, Karem A. Sakallah
Improved Design Debugging Using Maximum Satisfiability. FMCAD (2007)
Hossein M. Sheini, Karem A. Sakallah
): a step toward scalability in system verification. ICCAD (2006)
Hossein M. Sheini, Karem A. Sakallah
Ario: A Linear Integer Arithmetic Logic Solver. FMCAD (2006)
Arathi Ramani, Igor L. Markov, Karem A. Sakallah, Fadi A. Aloul
Breaking Instance-Independent Symmetries In Exact Graph Coloring. J. Artif. Intell. Res. 26 (2006)
Hossein M. Sheini, Karem A. Sakallah
From Propositional Satisfiability to Satisfiability Modulo Theories. SAT (2006)
Fadi A. Aloul, Karem A. Sakallah, Igor L. Markov
Efficient Symmetry Breaking for Boolean Satisfiability. IEEE Trans. Computers 55 (5) (2006)
Hossein M. Sheini, Karem A. Sakallah
A Progressive Simplifier for Satisfiability Modulo Theories. SAT (2006)
Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah
Refinement strategies for verification methods based on datapath abstraction. ASP-DAC (2006)
Hossein M. Sheini, Karem A. Sakallah
Pueblo: A Hybrid Pseudo-Boolean SAT Solver. J. Satisf. Boolean Model. Comput. 2 (1-4) (2006)
Hossein M. Sheini, Karem A. Sakallah
A SAT-Based Decision Procedure for Mixed Logical/Integer Linear Problems. CPAIOR (2005)
Hossein M. Sheini, Bart Peintner, Karem A. Sakallah, Martha E. Pollack
On Solving Soft Temporal Constraints Using SAT Techniques. CP (2005)
Mark H. Liffiton, Michael D. Moffitt, Martha E. Pollack, Karem A. Sakallah
Identifying Conflicts in Overconstrained Temporal Problems. IJCAI (2005)
Maher N. Mneimneh, Karem A. Sakallah
Principles of Sequential-Equivalence Verification. IEEE Des. Test Comput. 22 (3) (2005)
Mark H. Liffiton, Karem A. Sakallah
On Finding All Minimally Unsatisfiable Subformulas. SAT (2005)
Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah
Dynamic symmetry-breaking for improved Boolean optimization. ASP-DAC (2005)
Hossein M. Sheini, Karem A. Sakallah
A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic. SAT (2005)
Maher N. Mneimneh, Inês Lynce, Zaher S. Andraus, João P. Marques Silva, Karem A. Sakallah
A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas. SAT (2005)
Hossein M. Sheini, Karem A. Sakallah
Pueblo: A Modern Pseudo-Boolean SAT Solver. DATE (2005)
Zaher S. Andraus, Karem A. Sakallah
Automatic abstraction and verification of verilog models. DAC (2004)
Maher N. Mneimneh, Karem A. Sakallah, John Moondanos
Preserving synchronizing sequences of sequential circuits after retiming. ASP-DAC (2004)
Gi-Joon Nam, Fadi A. Aloul, Karem A. Sakallah, Rob A. Rutenbar
A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints. IEEE Trans. Computers 53 (6) (2004)
Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah
ShatterPB: symmetry-breaking for pseudo-Boolean formulas. ASP-DAC (2004)
Arathi Ramani, Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah
Breaking Instance-Independent Symmetries in Exact Graph Coloring. DATE (2004)
Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah
MINCE: A Static Global Variable-Ordering Heuristic for SAT Search and BDD Manipulation. J. Univers. Comput. Sci. 10 (12) (2004)
Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah, Igor L. Markov
Exploiting structure in symmetry detection for CNF. DAC (2004)
Yoonna Oh, Maher N. Mneimneh, Zaher S. Andraus, Karem A. Sakallah, Igor L. Markov
AMUSE: a minimally-unsatisfiable subformula extractor. DAC (2004)
Maher N. Mneimneh, Karem A. Sakallah
Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution. SAT (2003)
Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah
Shatter: efficient symmetry-breaking for boolean satisfiability. DAC (2003)
Fadi A. Aloul, Karem A. Sakallah, Igor L. Markov
Efficient Symmetry Breaking for Boolean Satisfiability. IJCAI (2003)
Michael A. Riepe, Karem A. Sakallah
Transistor placement for noncomplementary digital VLSI cell synthesis. ACM Trans. Design Autom. Electr. Syst. 8 (1) (2003)
Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah
Solving difficult instances of Boolean satisfiability in the presence of symmetry. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 22 (9) (2003)
Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah
FORCE: a fast and easy-to-implement variable-ordering heuristic. ACM Great Lakes Symposium on VLSI (2003)
Fadi A. Aloul, Brian D. Sierawski, Karem A. Sakallah
Satometer: how much have we searched? IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 22 (8) (2003)
Maher N. Mneimneh, Karem A. Sakallah
SAT-based sequential depth computation. ASP-DAC (2003)
Hui Xu, Rob A. Rutenbar, Karem A. Sakallah
sub-SAT: a formulation for relaxed Boolean satisfiability with applications in routing. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 22 (6) (2003)
Gi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar
Hybrid Routing for FPGAs by Integrating Boolean Satisfiability with Geometric Search. FPL (2002)
Fadi A. Aloul, Maher N. Mneimneh, Karem A. Sakallah
ZBDD-Based Backtrack Search SAT Solver. IWLS (2002)
Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah
Generic ILP versus specialized 0-1 ILP: an update. ICCAD (2002)
Gi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar
A new FPGA detailed routing approach via search-based Booleansatisfiability. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 21 (6) (2002)
Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah
Solving difficult SAT instances in the presence of symmetry. DAC (2002)
Fadi A. Aloul, Brian D. Sierawski, Karem A. Sakallah
Satometer: how much have we searched? DAC (2002)
Fadi A. Aloul, Maher N. Mneimneh, Karem A. Sakallah
Search-Based SAT Using Zero-Suppressed BDDs. DATE (2002)
Hui Xu, Rob A. Rutenbar, Karem A. Sakallah
sub-SAT: a formulation for relaxed boolean satisfiability with applications in routing. ISPD (2002)
Luís Guerra e Silva, João P. Marques Silva, Luís Miguel Silveira, Karem A. Sakallah
Satisfiability models and algorithms for circuit delay computation. ACM Trans. Design Autom. Electr. Syst. 7 (1) (2002)
Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah
Efficient Gate and Input Ordering for Circuit-to-BDD Conversion. IWLS (2002)
Fadi A. Aloul, Soha Hassoun, Karem A. Sakallah, David T. Blaauw
Robust SAT-Based Search Algorithm for Leakage Power Reduction. PATMOS (2002)
Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah
Improving the Efficiency of Circuit-to-BDD Conversion by Gate and Input Ordering. ICCD (2002)
Victor N. Kravets, Karem A. Sakallah
Resynthesis of multi-level circuits under tight constraints using symbolic optimization. ICCAD (2002)
Leyla Nazhandali, Karem A. Sakallah
Majority-Based Decomposition of Carry Logic in Binary Adders. IWLS (2002)
Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah
Faster SAT and Smaller BDDs via Common Function Structure. ICCAD (2001)
Hakan Yalcin, Robert Palermo, Mohammad Mortazavi, Cyrus Bamji, Karem A. Sakallah, John P. Hayes
An Advanced Timing Characterization Method Using Mode Dependency. DAC (2001)
Gi-Joon Nam, Fadi A. Aloul, Karem A. Sakallah, Rob A. Rutenbar
A comparative study of two Boolean formulations of FPGA detailed routing constraints. ISPD (2001)
Hakan Yalcin, Mohammad Mortazavi, Robert Palermo, Cyrus Bamji, Karem A. Sakallah, John P. Hayes
Fast and accurate timing characterization using functionalinformation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 20 (2) (2001)
Gi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar
A boolean satisfiability-based incremental rerouting approach with application to FPGAs. DATE (2001)
Maher N. Mneimneh, Fadi A. Aloul, Christopher T. Weaver, Saugata Chatterjee, Karem A. Sakallah, Todd M. Austin
Scalable Hybrid Verification of Complex Microprocessors. DAC (2001)
Jesse Whittemore, Joonyoung Kim, Karem A. Sakallah
SATIRE: A New Incremental Satisfiability Engine. DAC (2001)
Karem A. Sakallah, Fadi A. Aloul, João P. Marques Silva
An Experimental Study of Satisfiability Search Heuristics. DATE (2000)
Victor N. Kravets, Karem A. Sakallah
Generalized Symmetries in Boolean Functions. ICCAD (2000)

Karem A. Sakallah.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Karem A. Sakallah