Karem A. Sakallah

Proceedings of the NASA Formal Methods - 13th International Symposium, 2021

Towards an Automatic Proof of Lamport's Paxos.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer Aided Design, 2021

2020

AVR: Abstractly Verifying Reachability.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

EUFicient Reachability in Software with Arrays.

[BibT_eX]

[DOI]

Denis Bueno

Arlen Cox

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

2019

euforia: Complete Software Model Checking with Uninterpreted Functions.

[BibT_eX]

[DOI]

Denis Bueno

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2019

I4: incremental inference of inductive invariants for verification of distributed protocols.

[BibT_eX]

[DOI]

Haojun Ma

Jean-Baptiste Jeannin

Manos Kapritsos

Baris Kasikci

Proceedings of the 27th ACM Symposium on Operating Systems Principles, 2019

Model Checking of Verilog RTL Using IC3 with Syntax-Guided Abstraction.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 11th International Symposium, 2019

Towards Automatic Inference of Inductive Invariants.

[BibT_eX]

[DOI]

Haojun Ma

Jean-Baptiste Jeannin

Manos Kapritsos

Baris Kasikci

Proceedings of the Workshop on Hot Topics in Operating Systems, 2019

Empirical Evaluation of IC3-Based Model Checking Techniques on Verilog RTL Designs.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2019

2014

Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction.

[BibT_eX]

[DOI]

Suho Lee

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

Detecting Traditional Packers, Decisively.

[BibT_eX]

[DOI]

Proceedings of the Research in Attacks, Intrusions, and Defenses, 2013

Conflict Analysis and Branching Heuristics in the Search for Graph Automorphisms.

[BibT_eX]

[DOI]

Proceedings of the 25th IEEE International Conference on Tools with Artificial Intelligence, 2013

Generalized Boolean symmetries through nested partition refinement.

[BibT_eX]

[DOI]

Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, 2013

2012

Conflict Anticipation in the Search for Graph Automorphisms.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Graph Symmetry Detection and Canonical Labeling: Differences and Synergies.

[BibT_eX]

[DOI]

Proceedings of the Turing-100, 2012

2011

Anatomy and Empirical Evaluation of Modern SAT Solvers.

[BibT_eX]

[DOI]

Bull. EATCS, 2011

Empirical Study of the Anatomy of Modern Sat Solvers.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

Generating Data Race Witnesses by an SMT-Based Analysis.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods, 2011

Distilling critical attack graph surface iteratively through minimum-cost SAT solving.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Seventh Annual Computer Security Applications Conference, 2011

2010

Symmetry and Satisfiability: An Update.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2010

Trace-Driven Verification of Multithreaded Programs.

[BibT_eX]

[DOI]

Zijiang Yang

Proceedings of the Formal Methods and Software Engineering, 2010

Incorporating user control in automated interactive scheduling systems.

[BibT_eX]

[DOI]

Proceedings of the Conference on Designing Interactive Systems, 2010

2009

Symmetry and Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability, 2009

A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas.

[BibT_eX]

[DOI]

Constraints An Int. J., 2009

Dynamic symmetry-breaking for Boolean satisfiability.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2009

Generalizing Core-Guided Max-SAT.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

Dynamic Path Reduction for Software Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods, 7th International Conference, 2009

2008

Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints.

[BibT_eX]

[DOI]

J. Autom. Reason., 2008

Searching for Autarkies to Trim Unsatisfiable Clause Sets.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2008

Reveal: A Formal Verification Tool for Verilog Designs.

[BibT_eX]

[DOI]

Zaher S. Andraus

Proceedings of the Logic for Programming, 2008

Faster symmetry discovery using sparsity of symmetries.

[BibT_eX]

[DOI]

Paul T. Darga

Proceedings of the 45th Design Automation Conference, 2008

2007

Solution and Optimization of Systems of Pseudo-Boolean Constraints.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 2007

Symmetry breaking for pseudo-Boolean formulas.

[BibT_eX]

[DOI]

ACM J. Exp. Algorithmics, 2007

Report on the SAT 2007 Conference on Theory and Applications of Satisfiability Testing.

[BibT_eX]

[DOI]

Inês Lynce

AI Mag., 2007

Improved Design Debugging Using Maximum Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

2006

Efficient Symmetry Breaking for Boolean Satisfiability.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 2006

Pueblo: A Hybrid Pseudo-Boolean SAT Solver.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2006

Breaking Instance-Independent Symmetries In Exact Graph Coloring.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2006

A Progressive Simplifier for Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2006

From Propositional Satisfiability to Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2006

SMT(CLU): a step toward scalability in system verification.

[BibT_eX]

[DOI]

Proceedings of the 2006 International Conference on Computer-Aided Design, 2006

Ario: A Linear Integer Arithmetic Logic Solver.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

Refinement strategies for verification methods based on datapath abstraction.

[BibT_eX]

[DOI]

Zaher S. Andraus

Proceedings of the 2006 Conference on Asia South Pacific Design Automation: ASP-DAC 2006, 2006

2005

Principles of Sequential-Equivalence Verification.

[BibT_eX]

[DOI]

IEEE Des. Test Comput., 2005

A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2005

A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2005

On Finding All Minimally Unsatisfiable Subformulas.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2005

Identifying Conflicts in Overconstrained Temporal Problems.

[BibT_eX]

[DOI]

Proceedings of the IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30, 2005

Pueblo: A Modern Pseudo-Boolean SAT Solver.

[BibT_eX]

[DOI]

Proceedings of the 2005 Design, 2005

A SAT-Based Decision Procedure for Mixed Logical/Integer Linear Problems.

[BibT_eX]

[DOI]

Proceedings of the Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 2005

On Solving Soft Temporal Constraints Using SAT Techniques.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2005

Dynamic symmetry-breaking for improved Boolean optimization.

[BibT_eX]

[DOI]

Proceedings of the 2005 Conference on Asia South Pacific Design Automation, 2005

2004

A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 2004

MINCE: A Static Global Variable-Ordering Heuristic for SAT Search and BDD Manipulation.

[BibT_eX]

[DOI]

J. Univers. Comput. Sci., 2004

AMUSE: a minimally-unsatisfiable subformula extractor.

[BibT_eX]

[DOI]

Proceedings of the 41th Design Automation Conference, 2004

Exploiting structure in symmetry detection for CNF.

[BibT_eX]

[DOI]

Proceedings of the 41th Design Automation Conference, 2004

Automatic abstraction and verification of verilog models.

[BibT_eX]

[DOI]

Zaher S. Andraus

Proceedings of the 41th Design Automation Conference, 2004

Preserving synchronizing sequences of sequential circuits after retiming.

[BibT_eX]

[DOI]

John Moondanos

Proceedings of the 2004 Conference on Asia South Pacific Design Automation: Electronic Design and Solution Fair 2004, 2004

ShatterPB: symmetry-breaking for pseudo-Boolean formulas.

[BibT_eX]

[DOI]

Proceedings of the 2004 Conference on Asia South Pacific Design Automation: Electronic Design and Solution Fair 2004, 2004

2003

Transistor placement for noncomplementary digital VLSI cell synthesis.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2003

sub-SAT: a formulation for relaxed Boolean satisfiability with applications in routing.

[BibT_eX]

[DOI]

Hui Xu

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2003

Satometer: how much have we searched?

[BibT_eX]

[DOI]

Brian D. Sierawski

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2003

Solving difficult instances of Boolean satisfiability in the presence of symmetry.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2003

Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2003

FORCE: a fast and easy-to-implement variable-ordering heuristic.

[BibT_eX]

[DOI]

Proceedings of the 13th ACM Great Lakes Symposium on VLSI 2003, 2003

Shatter: efficient symmetry-breaking for boolean satisfiability.

[BibT_eX]

[DOI]

Proceedings of the 40th Design Automation Conference, 2003

SAT-based sequential depth computation.

[BibT_eX]

[DOI]

Proceedings of the 2003 Asia and South Pacific Design Automation Conference, 2003

2002

Satisfiability models and algorithms for circuit delay computation.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2002

A new FPGA detailed routing approach via search-based Booleansatisfiability.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2002

Robust SAT-Based Search Algorithm for Leakage Power Reduction.

[BibT_eX]

[DOI]

Proceedings of the Integrated Circuit Design. Power and Timing Modeling, 2002

Majority-Based Decomposition of Carry Logic in Binary Adders.

[BibT_eX]

Leyla Nazhandali

Proceedings of the 11th IEEE/ACM International Workshop on Logic & Synthesis, 2002

Efficient Gate and Input Ordering for Circuit-to-BDD Conversion.

[BibT_eX]

Proceedings of the 11th IEEE/ACM International Workshop on Logic & Synthesis, 2002

ZBDD-Based Backtrack Search SAT Solver.

[BibT_eX]

Proceedings of the 11th IEEE/ACM International Workshop on Logic & Synthesis, 2002

Improving the Efficiency of Circuit-to-BDD Conversion by Gate and Input Ordering.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Computer Design (ICCD 2002), 2002

Resynthesis of multi-level circuits under tight constraints using symbolic optimization.

[BibT_eX]

[DOI]

Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design, 2002

Generic ILP versus specialized 0-1 ILP: an update.

[BibT_eX]

[DOI]

Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design, 2002

Hybrid Routing for FPGAs by Integrating Boolean Satisfiability with Geometric Search.

[BibT_eX]

[DOI]

Proceedings of the Field-Programmable Logic and Applications, 2002

Search-Based SAT Using Zero-Suppressed BDDs.

[BibT_eX]

[DOI]

Proceedings of the 2002 Design, 2002

Solving difficult SAT instances in the presence of symmetry.

[BibT_eX]

[DOI]

Proceedings of the 39th Design Automation Conference, 2002

2001

Fast and accurate timing characterization using functionalinformation.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2001

Faster SAT and Smaller BDDs via Common Function Structure.

[BibT_eX]

[DOI]

Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, 2001

A boolean satisfiability-based incremental rerouting approach with application to FPGAs.

[BibT_eX]

[DOI]

Proceedings of the Conference on Design, Automation and Test in Europe, 2001

An Advanced Timing Characterization Method Using Mode Dependency.

[BibT_eX]

[DOI]

Proceedings of the 38th Design Automation Conference, 2001

SATIRE: A New Incremental Satisfiability Engine.

[BibT_eX]

[DOI]

Proceedings of the 38th Design Automation Conference, 2001

Scalable Hybrid Verification of Complex Microprocessors.

[BibT_eX]

[DOI]

Christopher T. Weaver

Saugata Chatterjee

Todd M. Austin

Proceedings of the 38th Design Automation Conference, 2001

2000

On Solving Stack-Based Incremental Satisfiability Problems.

[BibT_eX]

[DOI]

Proceedings of the IEEE International Conference On Computer Design: VLSI In Computers & Processors, 2000

Generalized Symmetries in Boolean Functions.

[BibT_eX]

[DOI]

Proceedings of the 2000 IEEE/ACM International Conference on Computer-Aided Design, 2000

An Experimental Study of Satisfiability Search Heuristics.

[BibT_eX]

[DOI]

Proceedings of the 2000 Design, 2000

Constructive Library-Aware Synthesis Using Symmetries.

[BibT_eX]

[DOI]

Proceedings of the 2000 Design, 2000

On Applying Incremental Satisfiability to Delay Fault Testing.

[BibT_eX]

[DOI]

Proceedings of the 2000 Design, 2000

Boolean satisfiability in electronic design automation.

[BibT_eX]

[DOI]

Proceedings of the 37th Conference on Design Automation, 2000

Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999

Timing verification of sequential dynamic circuits.

[BibT_eX]

[DOI]

David Van Campenhout

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999

GRASP: A Search Algorithm for Propositional Satisfiability.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 1999

Satisfiability-Based Detailed FPGA Routing.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on VLSI Design (VLSI Design 1999), 1999

Transistor level micro-placement and routing for two-dimensional digital VLSI cell synthesis.

[BibT_eX]

[DOI]

Proceedings of the 1999 International Symposium on Physical Design, 1999

Satisfiability-Based Functional Delay Fault Testing.

[BibT_eX]

Proceedings of the VLSI: Systems on a Chip, 1999

Satisfiability-Based Layout Revisited: Detailed Routing of Complex FPGAs vis Search-Based Boolean SAT.

[BibT_eX]

[DOI]

Proceedings of the 1999 ACM/SIGDA Seventh International Symposium on Field Programmable Gate Arrays, 1999

Functional Timing Analysis for IP Characterization.

[BibT_eX]

[DOI]

Proceedings of the 36th Conference on Design Automation, 1999

1998

Overview of complementary GaAs technology for high-speed VLSI circuits.

[BibT_eX]

[DOI]

IEEE Trans. Very Large Scale Integr. Syst., 1998

The edge-based design rule model revisited.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 1998

Timing analysis using propositional satisfiability.

[BibT_eX]

[DOI]

Luís Guerra e Silva

Luís Miguel Silveira

Proceedings of the 5th IEEE International Conference on Electronics, Circuits and Systems, 1998

AFTA: A Formal Delay Model for Functional Timing Analysis.

[BibT_eX]

[DOI]

V. Chandramouli

Proceedings of the 1998 Design, 1998

Congestion Driven Quadratic Placement.

[BibT_eX]

[DOI]

Phiroze N. Parakh

Richard B. Brown

Proceedings of the 35th Conference on Design Automation, 1998

M32: A Constructive multilevel Logic Synthesis System.

[BibT_eX]

[DOI]

Proceedings of the 35th Conference on Design Automation, 1998

1997

Robust Search Algorithms for Test Pattern Generation.

[BibT_eX]

[DOI]

Proceedings of the Digest of Papers: FTCS-27, 1997

Signal Delay in Coupled, Distributed RC Lines in the Presence of Temporal Proximity.

[BibT_eX]

[DOI]

V. Chandramouli

Proceedings of the 17th Conference on Advanced Research in VLSI (ARVLSI '97), 1997

1996

Ravel-XL: a hardware accelerator for assigned-delay compiled-code logic gate simulation.

[BibT_eX]

[DOI]

Richard B. Brown

IEEE Trans. Very Large Scale Integr. Syst., 1996

Conflict Analysis in Search Algorithms for Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Eigth International Conference on Tools with Artificial Intelligence, 1996

An approximate timing analysis method for datapath circuits.

[BibT_eX]

[DOI]

Hakan Yalcin

John P. Hayes

Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, 1996

GRASP - a new search algorithm for satisfiability.

[BibT_eX]

[DOI]

Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, 1996

Timing verification of sequential domino circuits.

[BibT_eX]

[DOI]

David Van Campenhout

Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, 1996

Modeling the Effects of Temporal Proximity of Input Transitions on Gate Propagation Delay and Transition Time.

[BibT_eX]

[DOI]

V. Chandramouli

Proceedings of the 33st Conference on Design Automation, 1996

1995

Critical paths in circuits with level-sensitive latches.

[BibT_eX]

[DOI]

IEEE Trans. Very Large Scale Integr. Syst., 1995

Timing models for gallium arsenide direct-coupled FET logic circuits.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1995

Maximum rate single-phase clocking of a closed pipeline including wave pipelining, stoppability, and startability.

[BibT_eX]

[DOI]

Chuan-Hua Chang

Edward S. Davidson

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1995

The Aurora RAM Compiler.

[BibT_eX]

[DOI]

Proceedings of the 32st Conference on Design Automation, 1995

1994

Efficient and Robust Test Generation-Based Timing Analysis.

[BibT_eX]

[DOI]

Proceedings of the 1994 IEEE International Symposium on Circuits and Systems, ISCAS 1994, London, England, UK, May 30, 1994

Macromodel Simplification Using Dimensional Analysis.

[BibT_eX]

[DOI]

Proceedings of the 1994 IEEE International Symposium on Circuits and Systems, ISCAS 1994, London, England, UK, May 30, 1994

Optimization of critical paths in circuits with level-sensitive latches.

[BibT_eX]

[DOI]

Proceedings of the 1994 IEEE/ACM International Conference on Computer-Aided Design, 1994

Dynamic Search-Space Pruning Techniques in Path Sensitization.

[BibT_eX]

[DOI]

Proceedings of the 31st Conference on Design Automation, 1994

1993

Synchronization of pipelines.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1993

An Analysis of Path Sensitization Criteria.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1993 International Conference on Computer Design: VLSI in Computers & Processors, 1993

Min-max linear programming and the timing analysis of digital circuits.

[BibT_eX]

[DOI]

Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, 1993

Concurrent path sensitization in timing analysis.

[BibT_eX]

[DOI]

Proceedings of the European Design Automation Conference 1993, 1993

1992

Analysis and design of latch-controlled synchronous digital circuits.

[BibT_eX]

[DOI]

Oyekunle A. Olukotun

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1992

Ravel: assigned-delay compiled-code logic simulation.

[BibT_eX]

[DOI]

Emily J. Shriver

Proceedings of the 1992 IEEE/ACM International Conference on Computer-Aided Design, 1992

Using constraint geometry to determine maximum rate pipeline clocking.

[BibT_eX]

[DOI]

Chuan-Hua Chang

Edward S. Davidson

Proceedings of the 1992 IEEE/ACM International Conference on Computer-Aided Design, 1992

Identification of critical paths in circuits with level-sensitive latches.

[BibT_eX]

[DOI]

Proceedings of the 1992 IEEE/ACM International Conference on Computer-Aided Design, 1992

Delay macromodels for the timing analysis of GaAs DCFL.

[BibT_eX]

[DOI]

Proceedings of the conference on European design automation, 1992

1991

The Design of a Microsupercomputer.

[BibT_eX]

[DOI]

Computer, 1991

Optimal Clocking of Circular Pipelines.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1991 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1991

FPD - An Environment for Exact Timing Analysis.

[BibT_eX]

[DOI]

Luís M. Vidigal

Proceedings of the 1991 IEEE/ACM International Conference on Computer-Aided Design, 1991

1990

A first-order charge conserving MOS capacitance model.

[BibT_eX]

[DOI]

Yao-Tsung Yen

Steve S. Greenberg

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1990

Clock Qualification Algorithm for Timing Analysis of Custom CMOS VLSI Circuits with Overlapped Clocking Disciplines and On-section Clock Derivation.

[BibT_eX]

Somanathan C. Menon

Proceedings of the First International Conference on Systems Integration, 1990

check Tc and min Tc: Timing Verification and Optimal Clocking of Synchronous Digtal Circuits.

[BibT_eX]

[DOI]

Kunle Olukotun

Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, 1990

1985

SAMSON2: An Event Driven VLSI Circuit Simulator.

[BibT_eX]

[DOI]