var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=http://web.eecs.umich.edu/~karem/publications/Sakallah-Publications.bib&jsonp=1&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=http://web.eecs.umich.edu/~karem/publications/Sakallah-Publications.bib&jsonp=1\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=http://web.eecs.umich.edu/~karem/publications/Sakallah-Publications.bib&jsonp=1\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
  2. \n
  3. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
  4. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2023\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Regularity and quantification: a new approach to verify distributed protocols.\n \n \n \n \n\n\n \n Goel, A.; and Sakallah, K. A.\n\n\n \n\n\n\n Innovations in Systems and Software Engineering, 19(4): 359-377. December 2023.\n \n\n\n\n
\n\n\n\n \n \n \"RegularityPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{goel2023regularity,\n   author = {Goel, Aman and Sakallah, Karem A.},\n   title = {{Regularity and quantification: a new approach to verify distributed protocols}},\n   journal = {Innovations in Systems and Software Engineering},\n   volume = {19},\n   number = {4},\n   pages = {359-377},\n   month = {December},\n   abstract = {Proving that an unbounded distributed protocol satisfies a given safety property amounts to finding a quantified inductive invariant that implies the property for all possible instance sizes of the protocol. Existing methods for solving this problem can be described as search procedures for an invariant whose quantification prefix fits a particular template. We propose an alternative constructive approach that does not prescribe, a priori, a specific quantifier prefix. Instead, the required prefix is automatically inferred without any enumerative search by carefully analyzing the spatial and temporal regularity of the protocol. The key insight underlying this approach is that structural regularity and quantification are closely related concepts that express protocol invariance under different re-arrangements of its components and its unbounded evolution over time. We extended the finite-domain IC3/PDR algorithm to use these regularities and boost clause learning to automatically derive the required quantified inductive invariant by exploiting the connection between structural regularities and quantification. We also describe a procedure to automatically find a minimal finite size, the cutoff, that yields a quantified invariant proving safety for any size. Our approach is implemented in IC3PO, a new verifier for distributed protocols that significantly outperforms the state of the art, scales orders of magnitude faster, and robustly derives compact inductive invariants fully automatically.},\n   year = {2023},\n   doi = {10.1007/s11334-022-00460-8},\n   url = {https://doi.org/10.1007/s11334-022-00460-8}\n}\n
\n
\n\n\n
\n Proving that an unbounded distributed protocol satisfies a given safety property amounts to finding a quantified inductive invariant that implies the property for all possible instance sizes of the protocol. Existing methods for solving this problem can be described as search procedures for an invariant whose quantification prefix fits a particular template. We propose an alternative constructive approach that does not prescribe, a priori, a specific quantifier prefix. Instead, the required prefix is automatically inferred without any enumerative search by carefully analyzing the spatial and temporal regularity of the protocol. The key insight underlying this approach is that structural regularity and quantification are closely related concepts that express protocol invariance under different re-arrangements of its components and its unbounded evolution over time. We extended the finite-domain IC3/PDR algorithm to use these regularities and boost clause learning to automatically derive the required quantified inductive invariant by exploiting the connection between structural regularities and quantification. We also describe a procedure to automatically find a minimal finite size, the cutoff, that yields a quantified invariant proving safety for any size. Our approach is implemented in IC3PO, a new verifier for distributed protocols that significantly outperforms the state of the art, scales orders of magnitude faster, and robustly derives compact inductive invariants fully automatically.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols.\n \n \n \n\n\n \n Fazekas, K.; Goel, A.; and Sakallah, K. A.\n\n\n \n\n\n\n In Formal Methods in Computer-Aided Design (FMCAD 2023), pages 152-161, Ames, Iowa, October 2023. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{fazekas2023sat,\n   author = {Fazekas, Katalin and Goel, Aman and Sakallah, Karem A.},\n   title = {{SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols}},\n   booktitle = {Formal Methods in Computer-Aided Design (FMCAD 2023)},\n   address = {Ames, Iowa},\n   pages = {152-161},\n   month = {October},\n   year = {2023},\n   doi = {10.34727/2023/isbn.978-3-85448-060-0_23}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Towards an Automatic Proof of the Bakery Algorithm.\n \n \n \n\n\n \n Goel, A.; Merz, S.; and Sakallah, K. A.\n\n\n \n\n\n\n In 43nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2023), pages 21-28, Lisbon, Portugal, June 2023. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{goel2023towards,\n   author = {Goel, Aman and Merz, Stephan and Sakallah, Karem A.},\n   title = {{Towards an Automatic Proof of the Bakery Algorithm}},\n   booktitle = {43nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2023)},\n   address = {Lisbon, Portugal},\n   pages = {21-28},\n   month = {June},\n   year = {2023},\n   doi = {https://doi.org/10.1007/978-3-031-35355-0_2}\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2022\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2022\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n reTLA: Towards an automatic transpiler from TLA+ to VMT.\n \n \n \n \n\n\n \n Kukovec, J.; Goel, A.; Konnov, I.; Merz, S.; and Sakallah, K.\n\n\n \n\n\n\n In TLA+ Conference, pages 1-3, St. Louis, MO, USA, September 2022. \n \n\n\n\n
\n\n\n\n \n \n \"reTLA:Paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 10 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kukovec2022retla,\n   author = {Kukovec, Jure and Goel, Aman  and Konnov, Igor and Merz, Stephan and Sakallah, Karem},\n   title = {{reTLA: Towards an automatic transpiler from TLA+ to VMT}},\n   booktitle = {TLA+ Conference},\n   address = {St. Louis, MO, USA},\n   pages = {1-3},\n   month = {September},\n   year = {2022},\n   url = {https://conf.tlapl.us/2022/sub7.pdf}\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2021\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Towards an Automatic Proof of Lamport’s Paxos.\n \n \n \n\n\n \n Goel, A.; and Sakallah, K. A.\n\n\n \n\n\n\n In Piskac, R.; and Whalen, M. W, editor(s), Formal Methods in Computer-Aided Design (FMCAD 2021), pages 112-122, New Haven, Connecticut, October 2021. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 23 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{goel2021towards,\n   author = {Goel, Aman and Sakallah, Karem A.},\n   title = {{Towards an Automatic Proof of Lamport’s Paxos}},\n   booktitle = {Formal Methods in Computer-Aided Design (FMCAD 2021)},\n   editor = {Piskac, Ruzica and Whalen, Michael W},\n   address = {New Haven, Connecticut},\n   pages = {112-122},\n   month = {October},\n   year = {2021},\n   doi = {https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_20},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n On Symmetry and Quantification: A New Approach to Verify Distributed Protocols.\n \n \n \n \n\n\n \n Goel, A.; and Sakallah, K. A.\n\n\n \n\n\n\n In 13th Annual NASA Formal Methods Symposium (NFM 2021), pages 131-150, Langley, Virginia, May 2021. \n \n\n\n\n
\n\n\n\n \n \n \"OnPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 50 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{goel2021symmetry,\n   author = {Goel, Aman and Sakallah, Karem A.},\n   title = {{On Symmetry and Quantification: A New Approach to Verify Distributed Protocols}},\n   booktitle = {13th Annual NASA Formal Methods Symposium (NFM 2021)},\n   address = {Langley, Virginia},\n   pages = {131-150},\n   month = {May},\n   year = {2021},\n   url={https://arxiv.org/abs/2103.14831},\n   doi={https://doi.org/10.1007/978-3-030-76384-8_9}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Symmetry and Satisfiability.\n \n \n \n\n\n \n Sakallah, K. A.\n\n\n \n\n\n\n In Biere, A.; Heule, M.; van Maaren, H.; and Walsh, T., editor(s), Handbook of Satisfiability, 2nd Edition, volume 336, of Frontiers in Artificial Intelligence and Applications, 13, pages 509-570. IOS Press, 2021.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 22 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{sakallah2021symmetry,\n   author = {Sakallah, Karem A.},\n   title = {{Symmetry and Satisfiability}},\n   booktitle = {Handbook of Satisfiability, 2nd Edition},\n   editor = {Biere, Armin and Heule, Marijn and van Maaren, Hans and Walsh, Toby},\n   series = {Frontiers in Artificial Intelligence and Applications},\n   publisher = {IOS Press},\n   volume = {336},\n   chapter = {13},\n   pages = {509-570},\n   year = {2021},\n   doi = {https://doi.org/10.3233/FAIA200996},\n\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2020\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n EUFicient Reachability in Software with Arrays.\n \n \n \n\n\n \n Bueno, D.; Cox, A.; and Sakallah, K. A.\n\n\n \n\n\n\n In Formal Methods in Computer-Aided Design (FMCAD), pages 57-66, Haifa, Israel, September 2020. IEEE\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 8 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{bueno2020euficient,\n   author = {Bueno, Denis and Cox, Arlen and Sakallah, Karem A.},\n   title = {{EUFicient Reachability in Software with Arrays}},\n   booktitle = {Formal Methods in Computer-Aided Design (FMCAD)},\n   address = {Haifa, Israel},\n   pages = {57-66},\n   month = {September},\n   year = {2020},\n   organization={IEEE},\n   doi={10.34727/2020/isbn.978-3-85448-042-6_12}}\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n AVR: Abstractly Verifying Reachability.\n \n \n \n\n\n \n Goel, A.; and Sakallah, K. A.\n\n\n \n\n\n\n In 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), volume LNCS 12078, pages 413-422, Dublin, Ireland, April 2020. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 10 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{goel2020avr,\n   author = {Goel, Aman and Sakallah, Karem A.},\n   title = {{AVR: Abstractly Verifying Reachability}},\n   booktitle = {26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020)},\n   address = {Dublin, Ireland},\n   volume = {LNCS 12078},\n   pages = {413-422},\n   month = {April},\n   year = {2020},\n   doi = {https://doi.org/10.1007/978-3-030-45190-5_23}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Horn2VMT: Translating Horn Reachability into Transition Systems.\n \n \n \n \n\n\n \n Bueno, D.; and Sakallah, K. A.\n\n\n \n\n\n\n In 7th Workshop on Horn Clauses for Verification and Synthesis (HCVS), Dublin, Ireland, April 2020. \n \n\n\n\n
\n\n\n\n \n \n \"Horn2VMT:Paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 6 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{bueno2020horn2vmt,\n   author = {Bueno, Denis and Sakallah, Karem A.},\n   title = {{Horn2VMT: Translating Horn Reachability into Transition Systems}},\n   booktitle = {7th Workshop on Horn Clauses for Verification and Synthesis (HCVS)},\n   address = {Dublin, Ireland},\n   month = {April},\n   year = {2020},\n   url = {https://arxiv.org/html/2008.02483v1/#EPTCS320.13}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2019\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2019\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n I4: Incremental Inference of Inductive Invariants forVerification of Distributed Protocols.\n \n \n \n\n\n \n Ma, H.; Goel, A.; Jeannin, J.; Kapritsos, M.; Kasikci, B.; and Sakallah, K. A.\n\n\n \n\n\n\n In The 27th ACM Symposium on Operating Systems Principles (SOSP 2019), pages 370–384, Huntsville, Ontario, Canada, October 2019. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{ma2019i4,\n   author = {Ma, Haojun and Goel, Aman  and Jeannin, Jean-Baptiste and Kapritsos, Manos and Kasikci, Baris and Sakallah, Karem A.},\n   title = {{I4: Incremental Inference of Inductive Invariants forVerification of Distributed Protocols}},\n   booktitle = {The 27th ACM Symposium on Operating Systems Principles (SOSP 2019)},\n   address = {Huntsville, Ontario, Canada},\n   pages = {370--384},\n   month = {October},\n   year = {2019},\n   doi = {https://doi.org/10.1145/3341301.3359651}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Towards Automatic Inference of Inductive Invariants.\n \n \n \n\n\n \n Ma, H.; Goel, A.; Jeannin, J.; Kapritsos, M.; Kasikci, B.; and Sakallah, K. A.\n\n\n \n\n\n\n In The 17th Workshop on Hot Topics in Operating Systems (HotOS XVII), pages 30-36, Bertinoro, Italy, May 2019. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{ma2019towards,\n   author = {Ma, Haojun and Goel, Aman  and Jeannin, Jean-Baptiste and Kapritsos, Manos and Kasikci, Baris and Sakallah, Karem A.},\n   title = {{Towards Automatic Inference of Inductive Invariants}},\n   booktitle = {The 17th Workshop on Hot Topics in Operating Systems (HotOS XVII)},\n   address = {Bertinoro, Italy},\n   pages = {30-36},\n   month = {May},\n   year = {2019},\n   doi = {https://doi.org/10.1145/3317550.3321451}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Model Checking of Verilog RTL using IC3 with Syntax-Guided Abstraction.\n \n \n \n\n\n \n Goel, A.; and Sakallah, K. A.\n\n\n \n\n\n\n In 11th Annual NASA Formal Methods Symposium (NFM 2019), volume LNCS 11460, pages 166–185, Houston, Texas, May 2019. Springer\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 6 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{goel2019model,\n   author = {Goel, Aman and Sakallah, Karem A.},\n   title = {{Model Checking of Verilog RTL using IC3 with Syntax-Guided Abstraction}},\n   booktitle = {11th Annual NASA Formal Methods Symposium (NFM 2019)},\n   address = {Houston, Texas},\n   publisher = {Springer},\n   volume = { LNCS 11460},\n   pages = {166--185},\n   month = {May},\n   year = {2019},\n   doi = {https://doi.org/10.1007/978-3-030-20652-9_11}\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Empirical Evaluation of IC3-Based Model Checking Techniques on Verilog RTL Designs.\n \n \n \n\n\n \n Goel, A.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. of the Design, Automation and Test in Europe Conference (DATE), pages 618-621, Florence, Italy, March 2019. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{goel2019empirical,\n   author = {Goel, Aman and Sakallah, Karem A.},\n   title = {{Empirical Evaluation of IC3-Based Model Checking Techniques on Verilog RTL Designs}},\n   booktitle = {Proc. of the Design, Automation and Test in Europe Conference (DATE)},\n   address = {Florence, Italy},\n   pages = {618-621},\n   month = {March},\n   year = {2019}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n euforia: Complete Software Model Checking with Uninterpreted Functions.\n \n \n \n\n\n \n Bueno, D.; and Sakallah, K. A.\n\n\n \n\n\n\n In 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), volume LNCS 11388, pages 363-385, Cascais, Portugal, January 2019. Springer\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 7 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{bueno2019euforia,\n   author = {Bueno, Denis and Sakallah, Karem A.},\n   title = {{euforia: Complete Software Model Checking with Uninterpreted Functions}},\n   booktitle = {20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)},\n   address = {Cascais, Portugal},\n   publisher = {Springer},\n   volume = {LNCS 11388},\n   pages = {363-385},\n   month = {January},\n   year = {2019},\n   doi = {https://doi.org/10.1007/978-3-030-11245-5_17}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2014\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2014\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction.\n \n \n \n\n\n \n Lee, S.; and Sakallah, K. A.\n\n\n \n\n\n\n In Computer-Aided Verification (CAV), volume LNCS 8559, pages 849–865, Vienna, Austria, July 2014. Springer\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{lee2014unbounded,\n   author = {Lee, Suho and Sakallah, Karem A.},\n   title = {{Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction}},\n   booktitle = {Computer-Aided Verification (CAV)},\n   address = {Vienna, Austria},\n   publisher = {Springer},\n   volume = {LNCS 8559},\n   pages = {849--865},\n   month = {July},\n   year = {2014},\n   doi = {https://doi.org/10.1007/978-3-319-08867-9_56}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2013\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2013\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Conflict Analysis and Branching Heuristics in the Search for Graph Automorphisms.\n \n \n \n\n\n \n Codenotti, P.; Katebi, H.; Sakallah, K. A.; and Markov, I. L.\n\n\n \n\n\n\n In 25th IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pages 907-914, Washington, DC, November 2013. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{codenotti2013conflict,\n   author = {Codenotti, Paolo and Katebi, Hadi and Sakallah, Karem A. and Markov, Igor L.},\n   title = {{Conflict Analysis and Branching Heuristics in the Search for Graph Automorphisms}},\n   booktitle = {25th IEEE International Conference on Tools with Artificial Intelligence (ICTAI)},\n   address = {Washington, DC},\n   pages = {907-914},\n   month = {November},\n   year = {2013},\n   doi = {https://doi.org/10.1109/ICTAI.2013.139}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Generalized Boolean Symmetries Through Nested Partition Refinement.\n \n \n \n \n\n\n \n Katebi, H.; Sakallah, K. A.; and Markov, I. L.\n\n\n \n\n\n\n In International Conference on Computer-Aided Design (ICCAD), pages 763-770, San Jose, California, November 2013. \n \n\n\n\n
\n\n\n\n \n \n \"GeneralizedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{katebi2013generalized,\n   author = {Katebi, Hadi and Sakallah, Karem A. and Markov, Igor L.},\n   title = {{Generalized Boolean Symmetries Through Nested Partition Refinement}},\n   booktitle = {International Conference on Computer-Aided Design (ICCAD)},\n   address = {San Jose, California},\n   pages = {763-770},\n   month = {November},\n   year = {2013},\n   doi = {https://doi.org/10.1109/ICCAD.2013.6691200},\n   url = {https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6691200}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Detecting Traditional Packers, Decisively.\n \n \n \n\n\n \n Bueno, D.; Compton, K. J.; Sakallah, K. A.; and Bailey, M.\n\n\n \n\n\n\n In Research in Attacks, Intrusions and Defenses (RAID'13) Symposium, volume LNCS 8145, pages 184-203, Saint Lucia, October 2013. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{bueno2013detecting,\n   author = {Bueno, Denis and Compton, Kevin J. and Sakallah, Karem A. and Bailey, Michael},\n   title = {{Detecting Traditional Packers, Decisively}},\n   booktitle = {Research in Attacks, Intrusions and Defenses (RAID'13) Symposium},\n   address = {Saint Lucia},\n   publisher = {Springer-Verlag},\n   volume = {LNCS 8145},\n   pages = {184-203},\n   month = {October},\n   year = {2013},\n   doi = {https://doi.org/10.1007/978-3-642-41284-4_10}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2012\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2012\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Conflict Anticipation in the Search for Graph Automorphisms.\n \n \n \n\n\n \n Katebi, H.; Sakallah, K. A.; and Markov, I. L.\n\n\n \n\n\n\n In Bjørner, N.; and Voronkov, A., editor(s), International Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'12), volume LNCS 7180, pages 243-257, Mérida, Venezuela, March 2012. Springer\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{katebi2012conflict,\n   author = {Katebi, Hadi and Sakallah, Karem A. and Markov, Igor L.},\n   title = {{Conflict Anticipation in the Search for Graph Automorphisms}},\n   booktitle = {International Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'12)},\n   editor = {Bj\\o{rner}, Nikolaj and Voronkov, Andrei},\n   address = {M\\'erida, Venezuela},\n   publisher = {Springer},\n   volume = {LNCS 7180},\n   pages = {243-257},\n   month = {March},\n   year = {2012},\n   doi = {https://doi.org/10.1007/978-3-642-28717-6_20}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Graph Symmetry Detection and Canonical Labeling: Differences and Synergies.\n \n \n \n \n\n\n \n Katebi, H.; Sakallah, K. A.; and Markov, I. L.\n\n\n \n\n\n\n In Voronkov, A., editor(s), Turing-100. The Alan Turing Centenary, volume 10, pages 181–195, Manchester, UK, June 2012. EasyChair\n \n\n\n\n
\n\n\n\n \n \n \"GraphPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{katebi2012graph,\n   author = {Katebi, Hadi and Sakallah, Karem A. and Markov, Igor L.},\n   title = {{Graph Symmetry Detection and Canonical Labeling: Differences and Synergies}},\n   booktitle = {Turing-100. The Alan Turing Centenary},\n   editor = {Voronkov, Andrei},\n   address = {Manchester, UK},\n   publisher = {EasyChair},\n   volume = {10},\n   pages = {181--195},\n   month = {June},\n   year = {2012},\n   doi = {{https://doi.org/10.29007/gzc1}},\n   url = {https://easychair.org/publications/paper/2vbW}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2011\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2011\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Empirical Study of the Anatomy of Modern SAT Solvers.\n \n \n \n\n\n \n Katebi, H.; Sakallah, K. A.; and Marques-Silva, J.\n\n\n \n\n\n\n In Sakallah, Karem; and Simon, L., editor(s), Fourteenth International Conference on Theory and Applications of Satisfiability Testing (SAT), volume LNCS 6695, of Lecture Notes in Computer Science, pages 343-356, Ann Arbor, Michigan, June 2011. Springer Berlin / Heidelberg\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{katebi2011empirical,\n   author = {Katebi, Hadi and Sakallah, Karem A. and Marques-Silva, João},\n   title = {{Empirical Study of the Anatomy of Modern SAT Solvers}},\n   booktitle = {Fourteenth International Conference on Theory and Applications of Satisfiability Testing (SAT)},\n   editor = {{Sakallah, Karem and Simon, Laurent}},\n   series = {Lecture Notes in Computer Science},\n   address = {Ann Arbor, Michigan},\n   publisher = {{Springer Berlin / Heidelberg}},\n   volume = {LNCS 6695},\n   pages = {343-356},\n   month = {June},\n   year = {2011},\n   doi = {https://doi.org/10.1007/978-3-642-21581-0_27}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Anatomy and Empirical Evaluation of Modern SAT Solvers.\n \n \n \n \n\n\n \n Sakallah, K. A.; and Marques-Silva, J.\n\n\n \n\n\n\n In Bull. of Euro. Assoc. for Theor. Computer Science, volume 103, pages 96-121, February 2011. \n \n\n\n\n
\n\n\n\n \n \n \"AnatomyPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah2011anatomy,\n   author = {Sakallah, Karem A. and Marques-Silva, {J\\~oao}},\n   title = {{Anatomy and Empirical Evaluation of Modern SAT Solvers}},\n   booktitle = {Bull. of Euro. Assoc. for Theor. Computer Science},\n   volume = {103},\n   pages = {96-121},\n   month = {February},\n   year = {2011},\n   url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.297.7785&rep=rep1&type=pdf}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Distilling Critical Attack Graph Surface iteratively through Minimum-Cost SAT Solving.\n \n \n \n\n\n \n Huang, H.; Zhang, S.; Ou, X.; Prakash, A.; and Sakallah, K.\n\n\n \n\n\n\n In Annual Computer Security Applications Conference (ACSAC'11), pages 31-40, Orlando, Florida, December 2011. ACM\n Best Paper Award\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{huang2011distilling,\n   author = {Huang, Heqing and Zhang, Su and Ou, Xinming and Prakash, Atul and Sakallah, Karem},\n   title = {{Distilling Critical Attack Graph Surface iteratively through Minimum-Cost SAT Solving}},\n   booktitle = {Annual Computer Security Applications Conference (ACSAC'11)},\n   address = {Orlando, Florida},\n   publisher = {ACM},\n   pages = {31-40},\n   month = {December},\n\t note = {Best Paper Award},\n   year = {2011},\n   doi = {https://doi.org/10.1145/2076732.2076738}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Generating Data Race Witnesses by an SMT-Based Analysis.\n \n \n \n\n\n \n Said, M.; Wang, C.; Yang, Z.; and Sakallah, K.\n\n\n \n\n\n\n In 3rd NASA Formal Methods Symposium, volume LNCS 6617, pages 313-327, Pasadena, California, April 2011. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{said2011generating,\n   author = {Said, Mahmoud and Wang, Chao and Yang, Zijiang and Sakallah, Karem},\n   title = {{Generating Data Race Witnesses by an SMT-Based Analysis}},\n   booktitle = {3rd NASA Formal Methods Symposium},\n   address = {Pasadena, California},\n   volume = {LNCS 6617},\n   pages = {313-327},\n   month = {April},\n   year = {2011},\n   doi = {https://doi.org/10.1007/978-3-642-20398-5_23}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Theory and Applications of Satisfiability Testing – SAT 2011.\n \n \n \n \n\n\n \n Sakallah, K. A.; and Simon, L.,\n editors.\n \n\n\n \n\n\n\n Volume LNCS 6695.Springer. Ann Arbor, Michigan, USA, 2011.\n \n\n\n\n
\n\n\n\n \n \n \"TheoryPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@proceedings{sakallah2011theory,\n   editor = {Sakallah, Karem A. and Simon, Laurent},\n   title = {{Theory and Applications of Satisfiability Testing -- SAT 2011}},\n   publisher = {Springer},\n   address = {Ann Arbor, Michigan, USA},\n   volume = {LNCS 6695},\n   year = {2011},\n   url = {https://link.springer.com/content/pdf/10.1007%2F978-3-642-21581-0}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2010\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2010\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Trace-Driven Verification of Multithreaded Programs.\n \n \n \n\n\n \n Yang, Z.; and Sakallah, K.\n\n\n \n\n\n\n In 12th International Conference on Formal Engineering Methods (ICFEM), volume LNCS 6447, pages 404–419, Shanghai, China, November 2010. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{yang2010trace,\n   author = {Yang, Zijiang and Sakallah, Karem},\n   title = {{Trace-Driven Verification of Multithreaded Programs}},\n   booktitle = {{12th International Conference on Formal Engineering Methods (ICFEM)}},\n   address = {Shanghai, China},\n   volume = {LNCS 6447},\n   pages = {{404--419}},\n   month = {November},\n   year = {2010},\n   doi = {https://doi.org/10.1007/978-3-642-16901-4_27}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Incorporating User Control in Automated Interactive Scheduling Systems.\n \n \n \n\n\n \n Huh, J.; Pollack, M.; Katebi, H.; Sakallah, K.; and Kirsch, N.\n\n\n \n\n\n\n In Proceedings of the 8th ACM Conference on Designing Interactive Systems (DIS '10), pages 306–309, Aarhus, Denmark, July 2010. ACM\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{huh2010incorporating,\n   author = {Huh, Jina and Pollack, Martha and Katebi, Hadi and Sakallah, Karem and Kirsch, Ned},\n   title = {{Incorporating User Control in Automated Interactive Scheduling Systems}},\n   booktitle = {{Proceedings of the 8th ACM Conference on Designing Interactive Systems (DIS '10)}},\n   address = {{Aarhus, Denmark}},\n   publisher = {{ACM}},\n   pages = {{306--309}},\n   month = {July},\n   year = {2010},\n   doi = {https://doi.org/10.1145/1858171.1858226}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Symmetry and Satisfiability: An Update.\n \n \n \n \n\n\n \n Katebi, H.; Sakallah, K. A.; and Markov, I. L.\n\n\n \n\n\n\n In Strichman, O.; and Szeider, S., editor(s), Thirteenth International Conference on Theory and Applications of Satisfiability Testing (SAT), volume LNCS 6175, pages 113-127, Edinburgh, July 2010. \n \n\n\n\n
\n\n\n\n \n \n \"SymmetryPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{katebi2010symmetry,\n   author = {Katebi, Hadi and Sakallah, Karem A. and Markov, Igor L.},\n   title = {{Symmetry and Satisfiability: An Update}},\n   booktitle = {Thirteenth International Conference on Theory and Applications of Satisfiability Testing (SAT)},\n   editor = {Strichman, O. and Szeider, S.},\n   address = {Edinburgh},\n   volume = {LNCS 6175},\n   pages = {113-127},\n   month = {July},\n   year = {2010},\n   doi = {https://doi.org/10.1007/978-3-642-14186-7_11},\n   url = {https://link.springer.com/content/pdf/10.1007%2F978-3-642-14186-7_11}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2009\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2009\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Dynamic Symmetry-Breaking for Boolean Satisfiability.\n \n \n \n\n\n \n Aloul, F. A.; Ramani, A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n Annals of Mathematics and Artificial Intelligence, 57(1): 59-73. September 2009.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{aloul2009dynamic,\n   author = {Aloul, Fadi A. and Ramani, Aarathi and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{Dynamic Symmetry-Breaking for Boolean Satisfiability}},\n   journal = {Annals of Mathematics and Artificial Intelligence},\n   volume = {57},\n   number = {1},\n   pages = {59-73},\n   month = {September},\n   year = {2009},\n   doi = {https://doi.org/10.1007/s10472-010-9173-2}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Dynamic Path Reduction for Software Model Checking.\n \n \n \n\n\n \n Yang, Z.; Al-Rawi, B.; Sakallah, K.; Huang, X.; Smolka, S.; and Grosu, R.\n\n\n \n\n\n\n In Wehrheim, M. L.; and H., editor(s), Integrated Formal Methods, volume LNCS 5423, pages 322-336, Duesseldorf, Germany, February 2009. Springer\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{yang2009dynamic,\n   author = {Yang, Zijiang and Al-Rawi, Bashar and Sakallah, Karem and Huang, Xiaowan and Smolka, Scott and Grosu, Radu},\n   title = {{Dynamic Path Reduction for Software Model Checking}},\n   booktitle = {Integrated Formal Methods},\n   editor = {Wehrheim, M. Leuschel and H.},\n   address = {Duesseldorf, Germany},\n   publisher = {Springer},\n   volume = {LNCS 5423},\n   pages = {322-336},\n   month = {February},\n   year = {2009}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Subformulas.\n \n \n \n\n\n \n Liffiton, M.; Mneimneh, M.; Lynce, I.; Andraus, Z.; Marques-Silva, J.; and Sakallah, K.\n\n\n \n\n\n\n Constraints, 14(4): 415-442. December 2009.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{liffiton2009branch,\n   author = {Liffiton, Mark and Mneimneh, Maher and Lynce, {In\\^es} and Andraus, Zaher and Marques-Silva, {J\\~oao} and Sakallah, Karem},\n   title = {{A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Subformulas}},\n   journal = {Constraints},\n   volume = {14},\n   number = {4},\n   pages = {415-442},\n   month = {December},\n   year = {2009},\n   doi = {https://doi.org/10.1007/s10601-008-9058-8}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Generalizing Core-Guided Max-SAT.\n \n \n \n\n\n \n Liffiton, M. H.; and Sakallah, K. A.\n\n\n \n\n\n\n In Twelfth International Conference on Theory and Applications of Satisfiability Testing (SAT 09), volume LNCS 5584, pages 481-494, Swansea, UK , 2009. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{liffiton2009generalizing,\n   author = {Liffiton, Mark H. and Sakallah, Karem A.},\n   title = {{Generalizing Core-Guided Max-SAT}},\n   booktitle = {Twelfth International Conference on Theory and Applications of Satisfiability Testing (SAT 09)},\n   address = {Swansea, UK },\n   volume = {LNCS 5584},\n   pages = {481-494},\n   year = {2009}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Symmetry and Satisfiability.\n \n \n \n\n\n \n Sakallah, K. A.\n\n\n \n\n\n\n In Biere, A.; Heule, M.; van Maaren, H.; and Walsh, T., editor(s), Handbook of Satisfiability, volume 185, of Frontiers in Artificial Intelligence and Applications, 10, pages 289-338. IOS Press, 2009.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{sakallah2009symmetry,\n   author = {Sakallah, Karem A.},\n   title = {{Symmetry and Satisfiability}},\n   booktitle = {Handbook of Satisfiability},\n   editor = {Biere, Armin and Heule, Marijn and van Maaren, Hans and Walsh, Toby},\n   series = {Frontiers in Artificial Intelligence and Applications},\n   publisher = {IOS Press},\n   volume = {185},\n   pages = {289-338},\n   chapter = {10},\n   year = {2009},\n   doi = {https://doi.org/10.3233/978-1-58603-929-5-289}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2008\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2008\n \n \n (8)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints.\n \n \n \n\n\n \n Liffiton, M. H.; and Sakallah, K. A.\n\n\n \n\n\n\n Journal of Automated Reasoning, 40(1): 1-33. January 2008.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{liffiton2008algorithms,\n   author = {Liffiton, Mark H. and Sakallah, Karem A.},\n   title = {{Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints}},\n   journal = {Journal of Automated Reasoning},\n   volume = {40},\n   number = {1},\n   pages = {1-33},\n   month = {January},\n   year = {2008},\n   notes = {(Published online September 2007)},\n   doi = {http://doi.org/10.1007/s10817-007-9084-z}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Subformulas.\n \n \n \n\n\n \n Liffiton, M.; Mneimneh, M.; Lynce, I.; Andraus, Z.; Marques-Silva, J.; and Sakallah, K.\n\n\n \n\n\n\n Constraints,1-28. August 2008.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{liffiton2008branch,\n   author = {Liffiton, Mark and Mneimneh, Maher and Lynce, {In\\^es} and Andraus, Zaher and Marques-Silva, {J\\~oao} and Sakallah, Karem},\n   title = {{A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Subformulas}},\n   journal = {Constraints},\n   pages = {1-28},\n   month = {August},\n   year = {2008},\n   notes = {(Online publication date)}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Faster Symmetry Discovery using Sparsity of Symmetries.\n \n \n \n\n\n \n Sakallah, K. A.\n\n\n \n\n\n\n In the 8th International Workshop on Symmetry and Constraint Satisfaction Problems (SymCon'08), Sydney, Australia, September 2008. \n Invited Talk\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah2008faster,\n   author = {Sakallah, Karem A.},\n   title = {{Faster Symmetry Discovery using Sparsity of Symmetries}},\n   booktitle = {the 8th International Workshop on Symmetry and Constraint Satisfaction Problems (SymCon'08)},\n   address = {Sydney, Australia},\n   month = {September},\n   note = {Invited Talk},\n   year = {2008}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Reveal: A Formal Verification Tool for Verilog Designs.\n \n \n \n\n\n \n Andraus, Z. S.; Liffiton, M. H.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), volume LNCS 5330, pages 343-352, Doha, Qatar, November 2008. Springer\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{andraus2008reveal,\n   author = {Andraus, Zaher S. and Liffiton, Mark H. and Sakallah, Karem A.},\n   title = {{Reveal: A Formal Verification Tool for Verilog Designs}},\n   booktitle = {International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08)},\n   address = {Doha, Qatar},\n   publisher = {Springer},\n   volume = {LNCS 5330},\n   pages = {343-352},\n   month = {November},\n   year = {2008}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Searching for Autarkies to Trim Unsatisfiable Clause Sets.\n \n \n \n\n\n \n Liffiton, M.; and Sakallah, K.\n\n\n \n\n\n\n In Eleventh International Conference on Theory and Applications of Satisfiability Testing (SAT), volume LNCS 4996, pages 182-195, Guangzhou, P. R. China, May 2008. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{liffiton2008searching,\n   author = {Liffiton, Mark and Sakallah, Karem},\n   title = {{Searching for Autarkies to Trim Unsatisfiable Clause Sets}},\n   booktitle = {Eleventh International Conference on Theory and Applications of Satisfiability Testing (SAT)},\n   address = {Guangzhou, P. R. China},\n   volume = {LNCS 4996},\n   pages = {182-195},\n   month = {May},\n   year = {2008}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Symmetry Breaking for Pseudo-Boolean Formulas.\n \n \n \n\n\n \n Aloul, F. A.; Ramani, A.; Sakallah, K. A.; and Markov, I. L.\n\n\n \n\n\n\n ACM Journal of Experimental Algorithms, 12(Article No. 1.3): 1-14. June 2008.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{aloul2008symmetry,\n   author = {Aloul, Fadi A. and Ramani, Arathi and Sakallah, Karem A. and Markov, Igor L.},\n   title = {{Symmetry Breaking for Pseudo-Boolean Formulas}},\n   journal = {ACM Journal of Experimental Algorithms},\n   volume = {12},\n   number = {Article No. 1.3},\n   pages = {1-14},\n   month = {June},\n   year = {2008}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Faster Symmetry Discovery using Sparsity of Symmetries.\n \n \n \n\n\n \n Darga, P. T.; Sakallah, K. A.; and Markov, I. L.\n\n\n \n\n\n\n In Proc. 45th IEEE/ACM Design Automation Conference (DAC), pages 149-154, Anaheim, California, June 2008. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{darga2008faster,\n   author = {Darga, Paul T. and Sakallah, Karem A. and Markov, Igor L.},\n   title = {{Faster Symmetry Discovery using Sparsity of Symmetries}},\n   booktitle = {Proc. 45th IEEE/ACM Design Automation Conference (DAC)},\n   address = {Anaheim, California},\n   pages = {149-154},\n   month = {June},\n   year = {2008}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n SMT-based Symbolic Model Checking for Multi-Threaded Programs.\n \n \n \n\n\n \n Yang, Z.; and Sakallah, K.\n\n\n \n\n\n\n In Exploiting Concurrency Efficiently and Correctly – (EC)$^2$, Princeton, NJ, July 2008. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{yang2008smt,\n   author = {Yang, Zijiang and Sakallah, Karem},\n   title = {{SMT-based Symbolic Model Checking for Multi-Threaded Programs}},\n   booktitle = {Exploiting Concurrency Efficiently and Correctly -- (EC)$^2$},\n   address = {Princeton, NJ},\n   month = {July},\n   year = {2008}\n\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2007\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2007\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Solution and Optimization of Systems of Pseudo-Boolean Constraints.\n \n \n \n\n\n \n Aloul, F. A.; Ramani, A.; Sakallah, K. A.; and Markov, I. L.\n\n\n \n\n\n\n IEEE Transactions on Computers, 56(10): 1415-1424. October 2007.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{aloul2007solution,\n   author = {Aloul, Fadi A. and Ramani, Arathi and Sakallah, Karem A. and Markov, Igor L.},\n   title = {{Solution and Optimization of Systems of Pseudo-Boolean Constraints}},\n   journal = {IEEE Transactions on Computers},\n   volume = {56},\n   number = {10},\n   pages = {1415-1424},\n   month = {October},\n   year = {2007}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Improved Design Debugging using Maximum Satisfiability.\n \n \n \n\n\n \n Safarpour, S.; Mangassarian, H.; Veneris, A.; Liffiton, M. H.; and Sakallah, K. A.\n\n\n \n\n\n\n In Formal Methods in Computer Aided Design (FMCAD07), pages 13-19, Austin, Texas, November 2007. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{safarpour2007improved,\n   author = {Safarpour, Sean and Mangassarian, Hratch and Veneris, Andreas and Liffiton, Mark H. and Sakallah, Karem A.},\n   title = {{Improved Design Debugging using Maximum Satisfiability}},\n   booktitle = {Formal Methods in Computer Aided Design (FMCAD07)},\n   address = {Austin, Texas},\n   pages = {13-19},\n   month = {November},\n   year = {2007}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Theory and Applications of Satisfiability Testing – SAT 2007.\n \n \n \n\n\n \n Marques-Silva, J.; and Sakallah, K. A.,\n editors.\n \n\n\n \n\n\n\n Volume LNCS 4501.Springer. Lisbon, Portugal, 2007.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@proceedings{marquessilva2007theory,\n   editor = {Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{Theory and Applications of Satisfiability Testing -- SAT 2007}},\n   publisher = {Springer},\n   address = {Lisbon, Portugal},\n   volume = {LNCS 4501},\n   pages = {384},\n   year = {2007}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2006\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2006\n \n \n (11)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n From Propositional SAT to SMT.\n \n \n \n\n\n \n Sheini, H. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In Hybrid Methods and Branching Rules in Combinatorial Optimization, pages 1-9, Montréal, Canada, September 2006. \n Invited presentation.\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sheini2006afrom,\n   author = {Sheini, Hossein M. and Sakallah, Karem A.},\n   title = {{From Propositional SAT to SMT}},\n   booktitle = {Hybrid Methods and Branching Rules in Combinatorial Optimization},\n   address = {Montréal, Canada},\n   pages = {1-9},\n   month = {September},\n   note = {Invited presentation.},\n   year = {2006}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n SMT(CLU): A Step toward Scalability in System Verification.\n \n \n \n\n\n \n Sheini, H. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In IEEE International Conference on Computer-Aided Design (ICCAD), pages 844-851, San Jose, California, November 2006. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sheini2006smt,\n   author = {Sheini, Hossein M. and Sakallah, Karem A.},\n   title = {{SMT(CLU): A Step toward Scalability in System Verification}},\n   booktitle = {IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {San Jose, California},\n   pages = {844-851},\n   month = {November},\n   year = {2006}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Ario: A linear Integer Arithmetic Solver.\n \n \n \n\n\n \n Sheini, H. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In Formal Methods in Computer Aided Design (FMCAD06), pages 47-48, San Jose, California, November 2006. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sheini2006ario,\n   author = {Sheini, Hossein M. and Sakallah, Karem A.},\n   title = {{Ario: A linear Integer Arithmetic Solver}},\n   booktitle = {Formal Methods in Computer Aided Design (FMCAD06)},\n   address = {San Jose, California},\n   pages = {47-48},\n   month = {November},\n   year = {2006}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Efficient Symmetry Breaking for Boolean Satisfiability.\n \n \n \n\n\n \n Aloul, F. A.; Sakallah, K. A.; and Markov, I. L.\n\n\n \n\n\n\n IEEE Transactions on Computers, 55(5): 549-558. May 2006.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{aloul2006efficient,\n   author = {Aloul, Fadi A. and Sakallah, Karem A. and Markov, Igor L.},\n   title = {{Efficient Symmetry Breaking for Boolean Satisfiability}},\n   journal = {IEEE Transactions on Computers},\n   volume = {55},\n   number = {5},\n   pages = {549-558},\n   month = {May},\n   year = {2006}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Progressive Approach for Satisfiability Modulo Theories.\n \n \n \n\n\n \n Sheini, H. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In Constraints and Verification, Isaac Newton Institute for Mathematical Sciences, Cambridge, England, May 2006. \n Invited presentation.\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sheini2006progressive,\n   author = {Sheini, Hossein M. and Sakallah, Karem A.},\n   title = {{A Progressive Approach for Satisfiability Modulo Theories}},\n   booktitle = {Constraints and Verification},\n   address = {Isaac Newton Institute for Mathematical Sciences, Cambridge, England},\n   month = {May},\n   note = {Invited presentation.},\n   year = {2006}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Microprocessor Verification Based on Datapath Abstraction and Refinement.\n \n \n \n\n\n \n Andraus, Z. S.; Liffiton, M. H.; and Sakallah, K. A.\n\n\n \n\n\n\n In Designing Correct Circuits (DCC 2006), Vienna, Austria, March 2006. \n Invited Presentation\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{andraus2006microprocessor,\n   author = {Andraus, Zaher S. and Liffiton, Mark H. and Sakallah, Karem A.},\n   title = {{Microprocessor Verification Based on Datapath Abstraction and Refinement}},\n   booktitle = {Designing Correct Circuits (DCC 2006)},\n   address = {Vienna, Austria},\n   month = {March},\n   note = {Invited Presentation},\n   year = {2006}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Pueblo: A Hybrid Pseudo-Boolean SAT Solver.\n \n \n \n\n\n \n Sheini, H. M.; and Sakallah, K. A.\n\n\n \n\n\n\n Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 2: 165-189. March 2006.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{sheini2006pueblo,\n   author = {Sheini, Hossein M. and Sakallah, Karem A.},\n   title = {{Pueblo: A Hybrid Pseudo-Boolean SAT Solver}},\n   journal = {Journal on Satisfiability, Boolean Modeling and Computation (JSAT)},\n   volume = {2},\n   pages = {165-189},\n   month = {March},\n   year = {2006}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Breaking Instance-Independent Symmetries in Exact Graph Coloring.\n \n \n \n\n\n \n Ramani, A.; Aloul, F. A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n Journal of Artificial Intelligence Research, 26: 289-322. July 2006.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{ramani2006breaking,\n   author = {Ramani, Aarathi and Aloul, Fadi A. and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{Breaking Instance-Independent Symmetries in Exact Graph Coloring}},\n   journal = {Journal of Artificial Intelligence Research},\n   volume = {26},\n   pages = {289-322},\n   month = {July},\n   year = {2006}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Refinement Strategies for Verification Methods Based on Datapath Abstraction.\n \n \n \n\n\n \n Andraus, Z. S.; Liffiton, M. H.; and Sakallah, K. A.\n\n\n \n\n\n\n In Asia and South Pacific Design Automation Conference (ASP-DAC), pages 19-24, Yokohama, Japan, January 2006. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{andraus2006refinement,\n   author = {Andraus, Zaher S. and Liffiton, Mark H. and Sakallah, Karem A.},\n   title = {{Refinement Strategies for Verification Methods Based on Datapath Abstraction}},\n   booktitle = {Asia and South Pacific Design Automation Conference (ASP-DAC)},\n   address = {Yokohama, Japan},\n   pages = {19-24},\n   month = {January},\n   year = {2006}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n From Propositional Satisfiability to Satisfiability Modulo Theories.\n \n \n \n\n\n \n Sheini, H. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In 9th International Conference on Theory and Applications of Satisfiability Testing (SAT06), volume LNCS 4121, pages 1-9, Seattle, Washington, August 2006. Springer-Verlag\n Invited paper.\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sheini2006from,\n   author = {Sheini, Hossein M. and Sakallah, Karem A.},\n   title = {{From Propositional Satisfiability to Satisfiability Modulo Theories}},\n   booktitle = {9th International Conference on Theory and Applications of Satisfiability Testing (SAT06)},\n   address = {Seattle, Washington},\n   publisher = {Springer-Verlag},\n   volume = {LNCS 4121},\n   pages = {1-9},\n   month = {August},\n   note = {Invited paper.},\n   year = {2006}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Progressive Simplifier for Satisfiability Modulo Theories.\n \n \n \n\n\n \n Sheini, H. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In 9th International Conference on Theory and Applications of Satisfiability Testing (SAT06), volume LNCS 4121, pages 184-197, Seattle, Washington, August 2006. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sheini2006aprogressive,\n   author = {Sheini, Hossein M. and Sakallah, Karem A.},\n   title = {{A Progressive Simplifier for Satisfiability Modulo Theories}},\n   booktitle = {9th International Conference on Theory and Applications of Satisfiability Testing (SAT06)},\n   address = {Seattle, Washington},\n   publisher = {Springer-Verlag},\n   volume = {LNCS 4121},\n   pages = {184-197},\n   month = {August},\n   year = {2006}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2005\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2005\n \n \n (10)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n On Solving Soft Temporal Constraints Using SAT Techniques.\n \n \n \n\n\n \n Sheini, H. M.; Peintner, B.; Sakallah, K. A.; and Pollack, M. E.\n\n\n \n\n\n\n In 11th International Conference on Principles and Practice of Constraint Programming (CP 2005), volume LNCS 3709, of Lecture Notes in Computer Science, pages 607-621, Sitges (Barcelona), Spain, October 2005. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sheini2005solving,\n   author = {Sheini, Hossein M. and Peintner, Bart and Sakallah, Karem A. and Pollack, Martha E.},\n   title = {{On Solving Soft Temporal Constraints Using SAT Techniques}},\n   booktitle = {11th International Conference on Principles and Practice of Constraint Programming (CP 2005)},\n   series = {Lecture Notes in Computer Science},\n   address = {Sitges (Barcelona), Spain},\n   volume = {LNCS 3709},\n   pages = {607-621},\n   month = {October},\n   year = {2005}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Principles of Sequential-Equivalence Verification.\n \n \n \n\n\n \n Mneimneh, M. N.; and Sakallah, K. A.\n\n\n \n\n\n\n IEEE Design & Test of Computers,248-257. May-June 2005.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{mneimneh2005principles,\n   author = {Mneimneh, Maher N. and Sakallah, Karem A.},\n   title = {{Principles of Sequential-Equivalence Verification}},\n   journal = {IEEE Design \\& Test of Computers},\n   pages = {248-257},\n   month = {May-June},\n   year = {2005}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Pueblo: A Modern Pseudo-Boolean SAT Solver.\n \n \n \n\n\n \n Sheini, H. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. of the Design, Automation and Test in Europe Conference (DATE), pages 684-685, Munich, Germany, March 2005. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sheini2005pueblo,\n   author = {Sheini, Hossein M. and Sakallah, Karem A.},\n   title = {{Pueblo: A Modern Pseudo-Boolean SAT Solver}},\n   booktitle = {Proc. of the Design, Automation and Test in Europe Conference (DATE)},\n   address = {Munich, Germany},\n   pages = {684-685},\n   month = {March},\n   year = {2005}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n On Finding All Minimally Unsatisfiable Subformulas.\n \n \n \n\n\n \n Liffiton, M. H.; and Sakallah, K. A.\n\n\n \n\n\n\n In Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT), volume LNCS 3569, of Lecture Notes in Computer Science, pages 173-186, St. Andrews, Scotland, June 2005. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{liffiton2005finding,\n   author = {Liffiton, Mark H. and Sakallah, Karem A.},\n   title = {{On Finding All Minimally Unsatisfiable Subformulas}},\n   booktitle = {Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT)},\n   series = {Lecture Notes in Computer Science},\n   address = {St. Andrews, Scotland},\n   volume = {LNCS 3569},\n   pages = {173-186},\n   month = {June},\n   year = {2005}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas.\n \n \n \n\n\n \n Mneimneh, M.; Lynce, I.; Andraus, Z.; Marques-Silva, J.; and Sakallah, K.\n\n\n \n\n\n\n In Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT), volume LNCS 3569, pages 467-474, St. Andrews, Scotland, June 2005. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{mneimneh2005branch,\n   author = {Mneimneh, Maher and Lynce, {In\\^es} and Andraus, Zaher and Marques-Silva, {J\\~oao} and Sakallah, Karem },\n   title = {{A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas}},\n   booktitle = {Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT)},\n   address = {St. Andrews, Scotland},\n   volume = {LNCS 3569},\n   pages = {467-474},\n   month = {June},\n   year = {2005}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Constructive Logic and Layout Synthesis Does Not Work.\n \n \n \n\n\n \n Oh, Y.; Ernst, E.; Sakallah, K. A.; and Markov, I. L.\n\n\n \n\n\n\n In International Workshop on Logic & Synthesis (IWLS), pages 367-374, Lake Arrowhead, California, June 2005. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{oh2005constructive,\n   author = {Oh, Yoonna and Ernst, Elizabeth and Sakallah, Karem A. and Markov, Igor L.},\n   title = {{Constructive Logic and Layout Synthesis Does Not Work}},\n   booktitle = {International Workshop on Logic \\& Synthesis (IWLS)},\n   address = {Lake Arrowhead, California},\n   pages = {367-374},\n   month = {June},\n   year = {2005}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic.\n \n \n \n\n\n \n Sheini, H. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In Bacchus, F.; and Walsh, T., editor(s), 8th International Conference on Theory and Applications of Satisfiability Testing, volume LNCS 3569, of Lecture Notes in Computer Science, pages 241-256, St. Andrews, Scotland, June 2005. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sheini2005scalable,\n   author = {Sheini, Hossein M. and Sakallah, Karem A.},\n   title = {{A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic}},\n   booktitle = {8th International Conference on Theory and Applications of Satisfiability Testing},\n   editor = {Bacchus, Fahiem and Walsh, Toby },\n   series = {Lecture Notes in Computer Science},\n   address = {St. Andrews, Scotland},\n   volume = {LNCS 3569},\n   pages = {241-256},\n   month = {June},\n   year = {2005}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A SAT-based Decision Procedure for Mixed Logical/Integer Linear Problems.\n \n \n \n\n\n \n Sheini, H. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CP-AI-OR), volume LNCS 3524, pages 320-335, Prague, Czech Republic, June 2005. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sheini2005sat,\n   author = {Sheini, Hossein M. and Sakallah, Karem A.  },\n   title = {{A SAT-based Decision Procedure for Mixed Logical/Integer Linear Problems}},\n   booktitle = {International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CP-AI-OR)},\n   address = {Prague, Czech Republic},\n   volume = {LNCS 3524},\n   pages = {320-335},\n   month = {June},\n   year = {2005}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Dynamic Symmetry-Breaking for Improved Boolean Optimization.\n \n \n \n\n\n \n Aloul, F. A.; Ramani, A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. of the Asia and South Pacific Design Automation Conference (ASP-DAC), pages 445-450, Shanghai, China, January 2005. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2005dynamic,\n   author = {Aloul, Fadi A. and Ramani, Aarathi and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{Dynamic Symmetry-Breaking for Improved Boolean Optimization}},\n   booktitle = {Proc. of the Asia and South Pacific Design Automation Conference (ASP-DAC)},\n   address = {Shanghai, China},\n   pages = {445-450},\n   month = {January},\n   year = {2005}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Identifying Conflicts in Overconstrained Temporal Problems.\n \n \n \n\n\n \n Liffiton, M. H.; Moffitt, M. D.; Pollack, M. E.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. 19th International Joint Conference on Artificial Intelligence (IJCAI-05), pages 205-211, Edinburgh, Scotland , August 2005. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{liffiton2005identifying,\n   author = {Liffiton, Mark H. and Moffitt, Michael D. and Pollack, Martha E. and Sakallah, Karem A.},\n   title = {{Identifying Conflicts in Overconstrained Temporal Problems}},\n   booktitle = {Proc. 19th International Joint Conference on Artificial Intelligence (IJCAI-05)},\n   address = {Edinburgh, Scotland     },\n   pages = {205-211},\n   month = {August},\n   year = {2005}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2004\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2004\n \n \n (9)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Automatic Abstraction and Verification of Verilog Models.\n \n \n \n\n\n \n Andraus, Z. S.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. 41st IEEE/ACM Design Automation Conference (DAC), pages 218-223, San Diego, California, June 2004. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{andraus2004automatic,\n   author = {Andraus, Zaher S. and Sakallah, Karem A.},\n   title = {{Automatic Abstraction and Verification of Verilog Models}},\n   booktitle = {Proc. 41st IEEE/ACM Design Automation Conference (DAC)},\n   address = {San Diego, California},\n   pages = {218-223},\n   month = {June},\n   year = {2004}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Exploiting Structure in Symmetry Detection for CNF.\n \n \n \n\n\n \n Darga, P. T.; Liffiton, M. H.; Sakallah, K. A.; and Markov, I. L.\n\n\n \n\n\n\n In Proc. 41st IEEE/ACM Design Automation Conference (DAC), pages 530-534, San Diego, California, June 2004. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{darga2004exploiting,\n   author = {Darga, Paul T. and Liffiton, Mark H. and Sakallah, Karem A. and Markov, Igor L.},\n   title = {{Exploiting Structure in Symmetry Detection for CNF}},\n   booktitle = {Proc. 41st IEEE/ACM Design Automation Conference (DAC)},\n   address = {San Diego, California},\n   pages = {530-534},\n   month = {June},\n   year = {2004}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints.\n \n \n \n\n\n \n Nam, G.; Aloul, F.; Sakallah, K. A.; and Rutenbar, R. A.\n\n\n \n\n\n\n IEEE Transactions on Computers, 53(6): 688-696. June 2004.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{nam2004comparative,\n   author = {Nam, Gi-Joon and Aloul, Fadi and Sakallah, Karem A. and Rutenbar, Rob A.},\n   title = {{A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints}},\n   journal = {IEEE Transactions on Computers},\n   volume = {53},\n   number = {6},\n   pages = {688-696},\n   month = {June},\n   year = {2004}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n AMUSE: A Minimally-Unsatisfiable Subformula Extractor.\n \n \n \n\n\n \n Oh, Y.; Mneimneh, M. N.; Andraus, Z. S.; Sakallah, K. A.; and Markov, I. L.\n\n\n \n\n\n\n In Proc. 41st IEEE/ACM Design Automation Conference (DAC), pages 518-523, San Diego, California, June 2004. \n Best Paper Nominee\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{oh2004amuse,\n   author = {Oh, Yoonna and Mneimneh, Maher N. and Andraus, Zaher S. and Sakallah, Karem A. and Markov, Igor L.},\n   title = {{AMUSE: A Minimally-Unsatisfiable Subformula Extractor}},\n   booktitle = {Proc. 41st IEEE/ACM Design Automation Conference (DAC)},\n   address = {San Diego, California},\n   pages = {518-523},\n   month = {June},\n   note = {Best Paper Nominee},\n   year = {2004}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n ShatterPB: Symmetry-Breaking for Pseudo-Boolean Formulas.\n \n \n \n\n\n \n Aloul, F. A.; Ramani, A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n In Asia and South Pacific Design Automation Conference (ASP-DAC 2004), pages 884-887, Yokohama, Japan, January 2004. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2004shatterpb,\n   author = {Aloul, Fadi A. and Ramani, Arathi and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{ShatterPB: Symmetry-Breaking for Pseudo-Boolean Formulas}},\n   booktitle = {Asia and South Pacific Design Automation Conference (ASP-DAC 2004)},\n   address = {Yokohama, Japan},\n   pages = {884-887},\n   month = {January},\n   year = {2004}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Preserving Synchronizing Sequences of Sequential Circuits After Retiming.\n \n \n \n\n\n \n Mneimneh, M. N.; Sakallah, K. A.; and Moondanos, J.\n\n\n \n\n\n\n In Asia and South Pacific Design Automation Conference (ASP-DAC 2004), pages 579-584, Yokohama, Japan, January 2004. \n Best Paper Award\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{mneimneh2004preserving,\n   author = {Mneimneh, Maher N. and Sakallah, Karem A. and Moondanos, John},\n   title = {{Preserving Synchronizing Sequences of Sequential Circuits After Retiming}},\n   booktitle = {Asia and South Pacific Design Automation Conference (ASP-DAC 2004)},\n   address = {Yokohama, Japan},\n   pages = {579-584},\n   month = {January},\n   note = {Best Paper Award},\n   year = {2004}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution.\n \n \n \n\n\n \n Mneimneh, M.; and Sakallah, K.\n\n\n \n\n\n\n Lecture Notes in Computer Science, LNCS 2919: 411-425. February 2004.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{mneimneh2004computing,\n   author = {Mneimneh, Maher and Sakallah, Karem},\n   title = {{Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution}},\n   journal = {Lecture Notes in Computer Science},\n   volume = {LNCS 2919},\n   pages = {411-425},\n   month = {February},\n   year = {2004}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Breaking Instance-Independent Symmetries in Exact Graph Coloring.\n \n \n \n\n\n \n Ramani, A.; Aloul, F. A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. of the Design, Automation and Test in Europe Conference (DATE), pages 324-329, Paris, France, February 2004. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{ramani2004breaking,\n   author = {Ramani, Aarathi and Aloul, Fadi A. and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{Breaking Instance-Independent Symmetries in Exact Graph Coloring}},\n   booktitle = {Proc. of the Design, Automation and Test in Europe Conference (DATE)},\n   address = {Paris, France},\n   pages = {324-329},\n   month = {February},\n   year = {2004}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n MINCE: A Static Global Variable-Ordering Heuristic for SAT Search and BDD Manipulation.\n \n \n \n\n\n \n Aloul, F. A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n Journal of Universal Computer Science, 10(12): 1562-1596. December 2004.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{aloul2004mince,\n   author = {Aloul, Fadi A. and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{MINCE: A Static Global Variable-Ordering Heuristic for SAT Search and BDD Manipulation}},\n   journal = {Journal of Universal Computer Science},\n   volume = {10},\n   number = {12},\n   pages = {1562-1596},\n   month = {December},\n   year = {2004}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2003\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2003\n \n \n (14)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Symmetry-Breaking for Pseudo-Boolean Formulas.\n \n \n \n\n\n \n Aloul, F. A.; Ramani, A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n In Third International Workshop on Symmetry in Constraint Satisfaction Problems, Held in conjunction with Ninth International Conference on Principles and Practice of Constraint Programming, CP'03, pages 1-12, County Cork, Ireland, September 29 2003. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2003symmetry,\n   author = {Aloul, Fadi A. and Ramani, Arathi and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{Symmetry-Breaking for Pseudo-Boolean Formulas}},\n   booktitle = {Third International Workshop on Symmetry in Constraint Satisfaction Problems, Held in conjunction with Ninth International Conference on Principles and Practice of Constraint Programming, CP'03},\n   address = {County Cork, Ireland},\n   pages = {1-12},\n   month = {September 29},\n   year = {2003}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution.\n \n \n \n\n\n \n Mneimneh, M.; and Sakallah, K.\n\n\n \n\n\n\n In Sixth International Conference on Theory and Applications of Satisfiability Testing, pages 356-369, Portofino, Italy, May 2003. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{mneimneh2003computing,\n   author = {Mneimneh, Maher and Sakallah, Karem},\n   title = {{Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution}},\n   booktitle = {Sixth International Conference on Theory and Applications of Satisfiability Testing},\n   address = {Portofino, Italy},\n   pages = {356-369},\n   month = {May},\n   year = {2003}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n REVERSE: Efficient Sequential Verification for Retiming.\n \n \n \n\n\n \n Mneimneh, M.; and Sakallah, K.\n\n\n \n\n\n\n In Twelfth International Workshop on Logic and Synthesis, pages 133-139, Laguna Beach, California, May 2003. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{mneimneh2003reverse,\n   author = {Mneimneh, Maher and Sakallah, Karem},\n   title = {{REVERSE: Efficient Sequential Verification for Retiming}},\n   booktitle = {Twelfth International Workshop on Logic and Synthesis},\n   address = {Laguna Beach, California},\n   pages = {133-139},\n   month = {May},\n   year = {2003}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Shatter: Efficient Symmetry-Breaking for Boolean Satisfiability.\n \n \n \n\n\n \n Aloul, F. A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. 40th IEEE/ACM Design Automation Conference (DAC), pages 836-839, Anaheim, California, June 2003. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2003shatter,\n   author = {Aloul, Fadi A. and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{Shatter: Efficient Symmetry-Breaking for Boolean Satisfiability}},\n   booktitle = {Proc. 40th IEEE/ACM Design Automation Conference (DAC)},\n   address = {Anaheim, California},\n   pages = {836-839},\n   month = {June},\n   year = {2003}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n sub-SAT: A Formulation for Relaxed Boolean Satisfiability with Applications in Routing.\n \n \n \n\n\n \n Xu, H.; Rutenbar, R. A.; and Sakallah, K. A.\n\n\n \n\n\n\n IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 22(6): 814-820. June 2003.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{xu2003subsat,\n   author = {Xu, Hui and Rutenbar, Rob A. and Sakallah, Karem A.},\n   title = {{sub-SAT: A Formulation for Relaxed Boolean Satisfiability with Applications in Routing}},\n   journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n   volume = {22},\n   number = {6},\n   pages = {814-820},\n   month = {June},\n   year = {2003}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n SAT-based Sequential Depth Computation.\n \n \n \n\n\n \n Mneimneh, M.; and Sakallah, K.\n\n\n \n\n\n\n In Asia and South Pacific Design Automation Conference (ASP-DAC 2003), pages 87-92, Kitakyushu, Japan, January 2003. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{mneimneh2003sat,\n   author = {Mneimneh, Maher and Sakallah, Karem},\n   title = {{SAT-based Sequential Depth Computation}},\n   booktitle = {Asia and South Pacific Design Automation Conference (ASP-DAC 2003)},\n   address = {Kitakyushu, Japan},\n   pages = {87-92},\n   month = {January},\n   year = {2003}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Transistor Placement for Non-Complementary Digital VLSI Cell Synthesis.\n \n \n \n\n\n \n Riepe, M. A.; and Sakallah, K. A.\n\n\n \n\n\n\n ACM Transactions on Design Automation of Electronic Systems (TODAES), 8(1): 81-107. January 2003.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{riepe2003transistor,\n   author = {Riepe, Michael A. and Sakallah, Karem A.},\n   title = {{Transistor Placement for Non-Complementary Digital VLSI Cell Synthesis}},\n   journal = {ACM Transactions on Design Automation of Electronic Systems (TODAES)},\n   volume = {8},\n   number = {1},\n   pages = {81-107},\n   month = {January},\n   year = {2003}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Efficient Symmetry Breaking for Boolean Satisfiability.\n \n \n \n\n\n \n Aloul, F. A.; Sakallah, K. A.; and Markov, I. L.\n\n\n \n\n\n\n In Proc. 18th International Joint Conference on Artificial Intelligence (IJCAI-03), pages 271-282, Acapulco, Mexico, August 2003. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2003efficient,\n   author = {Aloul, Fadi A. and Sakallah, Karem A. and Markov, Igor L.},\n   title = {{Efficient Symmetry Breaking for Boolean Satisfiability}},\n   booktitle = {Proc. 18th International Joint Conference on Artificial Intelligence (IJCAI-03)},\n   address = {Acapulco, Mexico},\n   pages = {271-282},\n   month = {August},\n   year = {2003}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n REVERSE: Efficient Sequential Verification for Retiming.\n \n \n \n\n\n \n Mneimneh, M. N.; and Sakallah, K. A.\n\n\n \n\n\n\n In TECHCON, Dallas, Texas, August 2003. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{mneimneh2003areverse,\n   author = {Mneimneh, Maher N. and Sakallah, Karem A.},\n   title = {{REVERSE: Efficient Sequential Verification for Retiming}},\n   booktitle = {TECHCON},\n   address = {Dallas, Texas},\n   month = {August},\n   year = {2003}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n FORCE: A Fast and Easy-to-Implement Variable-Ordering Heuristic.\n \n \n \n\n\n \n Aloul, F. A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n In Great Lakes Symposium on VLSI (GLSVLSI 2003), pages 116-119, Washington, D.C., April 2003. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2003force,\n   author = {Aloul, Fadi A. and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{FORCE: A Fast and Easy-to-Implement Variable-Ordering Heuristic}},\n   booktitle = {Great Lakes Symposium on VLSI (GLSVLSI 2003)},\n   address = {Washington, D.C.},\n   pages = {116-119},\n   month = {April},\n   year = {2003}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Solving Difficult Instances of Boolean Satisfiability in the Presence of Symmetry.\n \n \n \n\n\n \n Aloul, F. A.; Ramani, A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 22(9): 1117-1137. 2003.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{aloul2003solving,\n   author = {Aloul, Fadi A. and Ramani, Arathi and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{Solving Difficult Instances of Boolean Satisfiability in the Presence of Symmetry}},\n   journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n   volume = {22},\n   number = {9},\n   pages = {1117-1137},\n   year = {2003}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Satometer: How Much Have We Searched?.\n \n \n \n\n\n \n Aloul, F. A.; Sierawski, B.; and Sakallah, K. A.\n\n\n \n\n\n\n IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 22(8): 995-1004. 2003.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{aloul2003satometer,\n   author = {Aloul, Fadi A. and Sierawski, Brian and Sakallah, Karem A.},\n   title = {{Satometer: How Much Have We Searched?}},\n   journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n   volume = {22},\n   number = {8},\n   pages = {995-1004},\n   year = {2003}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n GRASP-A New Search Algorithm for Satisfiability.\n \n \n \n\n\n \n Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Kuehlmann, A., editor(s), The Best of ICCAD: 20 Years of Excellence in Computer-Aided Design, pages 73-89. Kluwer Academic Publishers, 2003.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{marquessilva2003grasp,\n   author = {Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{GRASP-A New Search Algorithm for Satisfiability}},\n   booktitle = {The Best of ICCAD: 20 Years of Excellence in Computer-Aided Design},\n   editor = {Kuehlmann, Andreas},\n   publisher = {Kluwer Academic Publishers},\n   pages = {73-89},\n   year = {2003}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Timing, Test and Manufacturing Overview.\n \n \n \n\n\n \n Sakallah, K. A.; Walker, D. M. (.; and Nassif, S. R.\n\n\n \n\n\n\n In Kuehlmann, A., editor(s), The Best of ICCAD: 20 Years of Excellence in Computer-Aided Design, pages 551-562. Kluwer Academic Publishers, 2003.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{sakallah2003timing,\n   author = {Sakallah, Karem A. and Walker, Duncan M. (Hank) and Nassif, Sani R.},\n   title = {{Timing, Test and Manufacturing Overview}},\n   booktitle = {The Best of ICCAD: 20 Years of Excellence in Computer-Aided Design},\n   editor = {Kuehlmann, Andreas},\n   publisher = {Kluwer Academic Publishers},\n   pages = {551-562},\n   year = {2003}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2002\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2002\n \n \n (20)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Improving the Efficiency of Circuit-to-BDD Conversion by Gate and Input Ordering.\n \n \n \n\n\n \n Aloul, F. A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Conference on Computer Design (ICCD), pages 64-69, Freiburg, Germany, September 16-18 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2002improving,\n   author = {Aloul, Fadi A. and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{Improving the Efficiency of  Circuit-to-BDD Conversion by  Gate and Input Ordering}},\n   booktitle = {International Conference on Computer Design (ICCD)},\n   address = {Freiburg, Germany},\n   pages = {64-69},\n   month = {September 16-18},\n   year = {2002}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Robust SAT-Based Search Algorithm for Leakage Power Reduction.\n \n \n \n\n\n \n Aloul, F. A.; Hassoun, S.; Sakallah, K. A.; and Blaauw, D.\n\n\n \n\n\n\n In 12th International Workshop on Power and Timing Modeling, Optimization and Simulation (PATMOS '02), pages 167-177, Sevilla, Spain, September 11-13 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2002robust,\n   author = {Aloul, Fadi A. and Hassoun, Soha and Sakallah, Karem A. and Blaauw, David},\n   title = {{Robust SAT-Based Search Algorithm for Leakage Power Reduction}},\n   booktitle = {12th International Workshop on Power and Timing Modeling, Optimization and Simulation (PATMOS '02)},\n   address = {Sevilla, Spain},\n   pages = {167-177},\n   month = {September 11-13},\n   year = {2002}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Symmetry Breaking for Boolean Satisfiability: The Mysteries of Logic Minimization.\n \n \n \n\n\n \n Aloul, F. A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n In Second International Workshop on Symmetry in Constraint Satisfaction Problems, Held in conjunction with Eighth International Conference on Principles and Practice of Constraint Programming, CP2002, pages 37-46, Ithaca, New York, September 8 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2002symmetry,\n   author = {Aloul, Fadi A. and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{Symmetry Breaking for Boolean Satisfiability: The Mysteries of Logic Minimization}},\n   booktitle = {Second International Workshop on Symmetry in Constraint Satisfaction Problems, Held in conjunction with Eighth International Conference on Principles and Practice of Constraint Programming, CP2002},\n   address = {Ithaca, New York},\n   pages = {37-46},\n   month = {September 8},\n   year = {2002}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n SAT-based Sequential Depth Computation.\n \n \n \n\n\n \n Mneimneh, M.; and Sakallah, K.\n\n\n \n\n\n\n In First International Workshop on Constraints in Formal Verification, Held in conjunction with Eight International Conference on Principles and Practice of Constraint Programming, CP2002, Ithaca, New York, September 8 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{mneimneh2002sat,\n   author = {Mneimneh, Maher and Sakallah, Karem},\n   title = {{SAT-based Sequential Depth Computation}},\n   booktitle = {First International Workshop on Constraints in Formal Verification, Held in conjunction with Eight International Conference on Principles and Practice of Constraint Programming, CP2002},\n   address = {Ithaca, New York},\n   month = {September 8},\n   year = {2002}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Hybrid Routing for FPGAs by Integrating Boolean Satisfiability with Geometric Search.\n \n \n \n\n\n \n Nam, G.; Sakallah, K.; and Rutenbar, R.\n\n\n \n\n\n\n In Glesner, M.; Zipf, P.; and Renovell, M., editor(s), 12th International Conference on Field Programmable Logic and Application (FPL 2002), volume LNCS 2438, pages 360-369, Montpellier, France, September 2-4 2002. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{nam2002hybrid,\n   author = {Nam, Gi-Joon and Sakallah, Karem and Rutenbar, Rob},\n   title = {{Hybrid Routing for FPGAs by Integrating Boolean Satisfiability with Geometric Search}},\n   booktitle = {12th International Conference on Field Programmable Logic and Application (FPL 2002)},\n   editor = {Glesner, M. and Zipf, P. and Renovell, M.},\n   address = {Montpellier, France},\n   publisher = {Springer-Verlag},\n   volume = {LNCS 2438},\n   pages = {360-369},\n   month = {September 2-4},\n   year = {2002}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Generic ILP versus Specialized 0-1 ILP: an Update.\n \n \n \n\n\n \n Aloul, F. A.; Ramani, A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 450-457, San Jose, California, November 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2002generic,\n   author = {Aloul, Fadi A. and Ramani, Arathi and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{Generic ILP versus Specialized 0-1 ILP: an Update}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {San Jose, California},\n   pages = {450-457},\n   month = {November},\n   year = {2002}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Resynthesis of Multi-level Circuits Under Tight Constraints Using Symbolic Optimization.\n \n \n \n\n\n \n Kravets, V. N.; and Sakallah, K. A.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 687-693, San Jose, California, November 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kravets2002resynthesis,\n   author = {Kravets, Victor N. and Sakallah, Karem A.},\n   title = {{Resynthesis of Multi-level Circuits Under Tight Constraints Using Symbolic Optimization}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {San Jose, California},\n   pages = {687-693},\n   month = {November},\n   year = {2002}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Solving Difficult SAT Instances in the Presence of Symmetry.\n \n \n \n\n\n \n Aloul, F. A.; Ramani, A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n In Fifth International Symposium on Theory and Applications of Satisfiability Testing, pages 338-345, Cincinnati, Ohio, May 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2002solving,\n   author = {Aloul, Fadi A. and Ramani, Arathi and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{Solving Difficult SAT Instances in the Presence of Symmetry}},\n   booktitle = {Fifth International Symposium on Theory and Applications of Satisfiability Testing},\n   address = {Cincinnati, Ohio},\n   pages = {338-345},\n   month = {May},\n   year = {2002}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n PBS: A Backtrack-Search Pseudo-Boolean Solver and Optimizer.\n \n \n \n\n\n \n Aloul, F. A.; Ramani, A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n In Fifth International Symposium on Theory and Applications of Satisfiability Testing, pages 346-353, Cincinnati, Ohio, May 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2002pbs,\n   author = {Aloul, Fadi A. and Ramani, Arathi and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{PBS: A Backtrack-Search Pseudo-Boolean Solver and Optimizer}},\n   booktitle = {Fifth International Symposium on Theory and Applications of Satisfiability Testing},\n   address = {Cincinnati, Ohio},\n   pages = {346-353},\n   month = {May},\n   year = {2002}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Tool for Measuring Progress of Backtrack-Search Solvers.\n \n \n \n\n\n \n Aloul, F. A.; Sierawski, B. D.; and Sakallah, K. A.\n\n\n \n\n\n\n In Fifth International Symposium on Theory and Applications of Satisfiability Testing, pages 98-105, Cincinnati, Ohio, May 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2002tool,\n   author = {Aloul, Fadi A. and Sierawski, Brian D. and Sakallah, Karem A.},\n   title = {{A Tool for Measuring Progress of Backtrack-Search Solvers}},\n   booktitle = {Fifth International Symposium on Theory and Applications of Satisfiability Testing},\n   address = {Cincinnati, Ohio},\n   pages = {98-105},\n   month = {May},\n   year = {2002}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Search-Based SAT Using Zero-Suppressed BDDs.\n \n \n \n\n\n \n Aloul, F. A.; Mneimneh, M. N.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proceedings of the Design, Automation and Test in Europe Conference (DATE 2002), pages 1082, Paris, France, March 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2002search,\n   author = {Aloul, Fadi A. and Mneimneh, Maher N. and Sakallah, Karem A.},\n   title = {{Search-Based SAT Using Zero-Suppressed BDDs}},\n   booktitle = {Proceedings of the Design, Automation and Test in Europe Conference (DATE 2002)},\n   address = {Paris, France},\n   pages = {1082},\n   month = {March},\n   year = {2002}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Solving Difficult SAT Instances in the Presence of Symmetry.\n \n \n \n\n\n \n Aloul, F. A.; Arathi, R.; Markov, I.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. 39th IEEE/ACM Design Automation Conference (DAC), pages 731-736, New Orlean, Louisiana, June 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2002asolving,\n   author = {Aloul, Fadi A. and Arathi, Raman and Markov, Igor and Sakallah, Karem A.},\n   title = {{Solving Difficult SAT Instances in the Presence of Symmetry}},\n   booktitle = {Proc. 39th IEEE/ACM Design Automation Conference (DAC)},\n   address = {New Orlean, Louisiana},\n   pages = {731-736},\n   month = {June},\n   year = {2002}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Efficient Gate and Input Ordering for Circuit-to-BDD Conversion.\n \n \n \n\n\n \n Aloul, F. A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Workshop on Logic & Synthesis (IWLS), pages 137-142, New Orleans, Louisiana, June 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2002efficient,\n   author = {Aloul, Fadi A. and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{Efficient Gate and Input Ordering for Circuit-to-BDD Conversion}},\n   booktitle = {International Workshop on Logic \\& Synthesis (IWLS)},\n   address = {New Orleans, Louisiana},\n   pages = {137-142},\n   month = {June},\n   year = {2002}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n ZBDD-Based Backtrack Search SAT Solver.\n \n \n \n\n\n \n Aloul, F. A.; Mneimneh, M. N.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Workshop on Logic & Synthesis (IWLS), pages 131-136, New Orleans, Louisiana, June 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2002zbdd,\n   author = {Aloul, Fadi A. and Mneimneh, Maher N. and Sakallah, Karem A.},\n   title = {{ZBDD-Based Backtrack Search SAT Solver}},\n   booktitle = {International Workshop on Logic \\& Synthesis (IWLS)},\n   address = {New Orleans, Louisiana},\n   pages = {131-136},\n   month = {June},\n   year = {2002}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Satometer: How Much Have We Searched?.\n \n \n \n\n\n \n Aloul, F. A.; Sierawski, B.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. 39th IEEE/ACM Design Automation Conference (DAC), pages 737-742, New Orleans, Louisiana, June 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2002satometer,\n   author = {Aloul, Fadi A. and Sierawski, Brian and Sakallah, Karem A.},\n   title = {{Satometer: How Much Have We Searched?}},\n   booktitle = {Proc. 39th IEEE/ACM Design Automation Conference (DAC)},\n   address = {New Orleans, Louisiana},\n   pages = {737-742},\n   month = {June},\n   year = {2002}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A New FPGA Detailed Routing Approach via Search-Based Boolean Satisfiability.\n \n \n \n\n\n \n Nam, G.; Sakallah, K. A.; and Rutenbar, R.\n\n\n \n\n\n\n IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 21(6): 674-684. June 2002.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{nam2002new,\n   author = {Nam, Gi-Joon and Sakallah, Karem A. and Rutenbar, Rob},\n   title = {{A New FPGA Detailed Routing Approach via Search-Based Boolean Satisfiability}},\n   journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n   volume = {21},\n   number = {6},\n   pages = {674-684},\n   month = {June},\n   year = {2002}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Majority-Based Decomposition of Carry Logic in Binary Adders.\n \n \n \n\n\n \n Nazhandali, L.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Workshop on Logic & Synthesis (IWLS), pages 179-184, New Orleans, Louisiana, June 2002. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{nazhandali2002majority,\n   author = {Nazhandali, Leyla and Sakallah, Karem A.},\n   title = {{Majority-Based Decomposition of Carry Logic in Binary Adders}},\n   booktitle = {International Workshop on Logic \\& Synthesis (IWLS)},\n   address = {New Orleans, Louisiana},\n   pages = {179-184},\n   month = {June},\n   year = {2002}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Satisfiability Models and Algorithms for Circuit Delay Computation.\n \n \n \n\n\n \n e Silva, L. G.; Marques-Silva, J.; Silveira, L. M.; and Sakallah, K. A.\n\n\n \n\n\n\n ACM Transactions on Design Automation of Electronic Systems (TODAES), 7(1): 137-158. January 2002.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{esilva2002satisfiability,\n   author = {e Silva, Luis Guerra and Marques-Silva, {J\\~oao} and Silveira, L. Miguel and Sakallah, Karem A.},\n   title = {{Satisfiability Models and Algorithms for Circuit Delay Computation}},\n   journal = {ACM Transactions on Design Automation of Electronic Systems (TODAES)},\n   volume = {7},\n   number = {1},\n   pages = {137-158},\n   month = {January},\n   year = {2002}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n sub-SAT: A Formulation for Relaxed Boolean Satisfiability with Applications in Routing.\n \n \n \n\n\n \n Xu, H.; Rutenbar, R. A.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. of 2002 International Symposium on Physical Design, pages 182-187, Del Mar, California, April 2002. ACM Press\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{xu2002subsat,\n   author = {Xu, Hui and Rutenbar, Rob A. and Sakallah, Karem A.},\n   title = {{sub-SAT: A Formulation for Relaxed Boolean Satisfiability with Applications in Routing}},\n   booktitle = {Proc. of 2002 International Symposium  on Physical Design},\n   address = {Del Mar, California},\n   publisher = {ACM Press},\n   pages = {182-187},\n   month = {April},\n   year = {2002}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Static Timing Analysis.\n \n \n \n\n\n \n Kukimoto, Y.; Berkelaar, M.; and Sakallah, K.\n\n\n \n\n\n\n In Hassoun, S.; and Sasao, T., editor(s), Logic Synthesis and Verification, of The Kluwer International Series in Engineering and Computer Science, pages 373-401. Kluwer Academic Publishers, 2002.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{kukimoto2002static,\n   author = {Kukimoto, Yuji and Berkelaar, Michel and Sakallah, Karem},\n   title = {{Static Timing Analysis}},\n   booktitle = {Logic Synthesis and Verification},\n   editor = {Hassoun, Soha and Sasao, Tsutomu},\n   series = {The Kluwer International Series in Engineering and Computer Science},\n   publisher = {Kluwer Academic Publishers},\n   pages = {373-401},\n   year = {2002}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2001\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2001\n \n \n (9)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Faster SAT and Smaller BDDs via Common Function Structure.\n \n \n \n\n\n \n Aloul, F.; Markov, I.; and Sakallah, K. A.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 443-448, San Jose, California, November 2001. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2001faster,\n   author = {Aloul, Fadi and Markov, Igor and Sakallah, Karem A.},\n   title = {{Faster SAT and Smaller BDDs via Common Function Structure}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {San Jose, California},\n   pages = {443-448},\n   month = {November},\n   year = {2001}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Boolean Satisfiability-Based Incremental Rerouting Approach with Application to FPGAs.\n \n \n \n\n\n \n Nam, G.; Sakallah, K.; and Rutenbar, R.\n\n\n \n\n\n\n In Proceedings of the Design, Automation and Test in Europe Conference (DATE 2001), pages 560-564, Munich, Germany, March 2001. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{nam2001boolean,\n   author = {Nam, Gi-Joon and Sakallah, Karem and Rutenbar, Rob},\n   title = {{A Boolean Satisfiability-Based Incremental Rerouting Approach with Application to FPGAs}},\n   booktitle = {Proceedings of the Design, Automation and Test in Europe Conference (DATE 2001)},\n   address = {Munich, Germany},\n   pages = {560-564},\n   month = {March},\n   year = {2001}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n MINCE: A Static Global Variable-Ordering for SAT and BDD.\n \n \n \n\n\n \n Aloul, F. A.; Markov, I. L.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Workshop on Logic Synthesis (IWLS), pages 281-286, Granlibakken, California, June 2001. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2001mince,\n   author = {Aloul, Fadi A. and Markov, Igor L. and Sakallah, Karem A.},\n   title = {{MINCE: A Static Global Variable-Ordering for SAT and BDD}},\n   booktitle = {International Workshop on Logic Synthesis (IWLS)},\n   address = {Granlibakken, California},\n   pages = {281-286},\n   month = {June},\n   year = {2001}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Backtrack Search Using ZBDDs.\n \n \n \n\n\n \n Aloul, F. A.; Mneimneh, M. N.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Workshop on Logic Synthesis (IWLS), pages 293-297, Granlibakken, California, June 2001. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2001backtrack,\n   author = {Aloul, Fadi A. and Mneimneh, Maher N. and Sakallah, Karem A.},\n   title = {{Backtrack Search Using ZBDDs}},\n   booktitle = {International Workshop on Logic Synthesis (IWLS)},\n   address = {Granlibakken, California},\n   pages = {293-297},\n   month = {June},\n   year = {2001}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Scalable Hybrid Verification of Complex Microprocessors.\n \n \n \n\n\n \n Mneimneh, M.; Aloul, F.; Weaver, C.; Chatterjee, S.; Sakallah, K.; and Austin, T.\n\n\n \n\n\n\n In Proc. 38th IEEE/ACM Design Automation Conference (DAC), pages 41-46, Las Vegas, Nevada, June 2001. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{mneimneh2001scalable,\n   author = {Mneimneh, Maher and Aloul, Fadi and Weaver, Christopher and Chatterjee, Saugata and Sakallah, Karem and Austin, Todd},\n   title = {{Scalable Hybrid Verification of Complex Microprocessors}},\n   booktitle = {Proc. 38th IEEE/ACM Design Automation Conference (DAC)},\n   address = {Las Vegas, Nevada},\n   pages = {41-46},\n   month = {June},\n   year = {2001}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n SATIRE: A New Incremental Satisfiability Engine.\n \n \n \n\n\n \n Whittemore, J.; Kim, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. 38th IEEE/ACM Design Automation Conference (DAC), pages 542-545, Las Vegas, Nevada, June 2001. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{whittemore2001satire,\n   author = {Whittemore, Jesse and Kim, Joonyoung and Sakallah, Karem A.},\n   title = {{SATIRE: A New Incremental Satisfiability Engine}},\n   booktitle = {Proc. 38th IEEE/ACM Design Automation Conference (DAC)},\n   address = {Las Vegas, Nevada},\n   pages = {542-545},\n   month = {June},\n   year = {2001}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An Advanced Timing Characterization Method Using Mode Dependency.\n \n \n \n\n\n \n Yalcin, H.; Palermo, R.; Mortazavi, M. S.; Bamji, C.; Sakallah, K. A.; and Hayes, J. P.\n\n\n \n\n\n\n In Proc. 38th IEEE/ACM Design Automation Conference (DAC), pages 657-660, Las Vegas, Nevada, June 2001. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{yalcin2001advanced,\n   author = {Yalcin, Hakan and Palermo, Robert and Mortazavi, Mohammad S. and Bamji, Cyrus and Sakallah, Karem A. and Hayes, John P.},\n   title = {{An Advanced Timing Characterization Method Using Mode Dependency}},\n   booktitle = {Proc. 38th IEEE/ACM Design Automation Conference (DAC)},\n   address = {Las Vegas, Nevada},\n   pages = {657-660},\n   month = {June},\n   year = {2001}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Fast and Accurate Timing Characterization Using Functional Information.\n \n \n \n\n\n \n Yalcin, H.; Mortazavi, M.; Palermo, R.; Bamji, C.; Sakallah, K. A.; and Hayes, J. P.\n\n\n \n\n\n\n IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 20(2): 315-331. February 2001.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{yalcin2001fast,\n   author = {Yalcin, Hakan and Mortazavi, Mohammad and Palermo, Robert and Bamji, Cyrus and Sakallah, Karem A. and Hayes, John P.},\n   title = {{Fast and Accurate Timing Characterization Using Functional Information}},\n   journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n   volume = {20},\n   number = {2},\n   pages = {315-331},\n   month = {February},\n   year = {2001}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints.\n \n \n \n\n\n \n Nam, G.; Aloul, F.; Sakallah, K. A.; and Rutenbar, R.\n\n\n \n\n\n\n In International Sympoisum on Physical Design (ISPD '01), pages 222-227, Sonoma, California, April 2001. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{nam2001comparative,\n   author = {Nam, Gi-Joon and Aloul, Fadi and Sakallah, Karem A. and Rutenbar, Rob},\n   title = {{A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints}},\n   booktitle = {International Sympoisum on Physical Design (ISPD '01)},\n   address = {Sonoma, California},\n   pages = {222-227},\n   month = {April},\n   year = {2001}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 2000\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2000\n \n \n (12)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n On Solving Stack-Based Incremental Satisfiability Problems.\n \n \n \n\n\n \n Kim, J.; Whittemore, J. P.; Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. of IEEE International Conference on Computer Design (ICCD), pages 379-382, Austin, Texas, September 2000. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kim2000solving,\n   author = {Kim, Joonyoung and Whittemore, Jesse P. and Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{On Solving Stack-Based Incremental Satisfiability Problems}},\n   booktitle = {Proc. of IEEE International Conference on Computer Design (ICCD)},\n   address = {Austin, Texas},\n   pages = {379-382},\n   month = {September},\n   year = {2000}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Structure-Aware Functional Decomposition in Logic Synthesis.\n \n \n \n\n\n \n Kravets, V. N.; and Sakallah, K. A.\n\n\n \n\n\n\n In TECHCON, Phoenix, Arizona, September 2000. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kravets2000structure,\n   author = {Kravets, Victor N. and Sakallah, Karem A.},\n   title = {{Structure-Aware Functional Decomposition in Logic Synthesis}},\n   booktitle = {TECHCON},\n   address = {Phoenix, Arizona},\n   month = {September},\n   year = {2000}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Generalized Symmetries in Boolean Functions.\n \n \n \n\n\n \n Kravets, V. N.; and Sakallah, K. A.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 526-532, San Jose, California, November 2000. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kravets2000generalized,\n   author = {Kravets, Victor N. and Sakallah, Karem A.},\n   title = {{Generalized Symmetries in Boolean Functions}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {San Jose, California},\n   pages = {526-532},\n   month = {November},\n   year = {2000}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An Experimental Study of Satisfiability Search Heuristics.\n \n \n \n\n\n \n Aloul, F.; Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proceedings of the Design, Automation and Test in Europe Conference (DATE 2000), pages 745, Paris, France, March 2000. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2000experimental,\n   author = {Aloul, Fadi and Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{An Experimental Study of Satisfiability Search Heuristics}},\n   booktitle = {Proceedings of the Design, Automation and Test in Europe Conference (DATE 2000)},\n   address = {Paris, France},\n   pages = {745},\n   month = {March},\n   year = {2000}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n On Applying Incremental Satisfiability to Delay Fault Testing.\n \n \n \n\n\n \n Kim, J.; Whittemore, J. P.; Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proceedings of the Design, Automation and Test in Europe Conference (DATE 2000), pages 380-384, Paris, France, March 2000. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kim2000applying,\n   author = {Kim, Joonyoung and Whittemore, J. P. and Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{On Applying Incremental Satisfiability to Delay Fault Testing}},\n   booktitle = {Proceedings of the Design, Automation and Test in Europe Conference (DATE 2000)},\n   address = {Paris, France},\n   pages = {380-384},\n   month = {March},\n   year = {2000}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Constructive Library-Aware Synthesis Using Symmetries.\n \n \n \n\n\n \n Kravets, V. N.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proceedings of the Design, Automation and Test in Europe Conference (DATE 2000), pages 208-213, Paris, France, March 2000. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kravets2000constructive,\n   author = {Kravets, Victor N. and Sakallah, Karem A.},\n   title = {{Constructive Library-Aware Synthesis Using Symmetries}},\n   booktitle = {Proceedings of the Design, Automation and Test in Europe Conference (DATE 2000)},\n   address = {Paris, France},\n   pages = {208-213},\n   month = {March},\n   year = {2000}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Efficient Verification of the PCI Local Bus using Boolean Satisfiability.\n \n \n \n\n\n \n Aloul, F. A.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Workshop on Logic Synthesis (IWLS), pages 131-135, Dana Point, California, June 2000. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2000efficient,\n   author = {Aloul, Fadi A. and Sakallah, Karem A.},\n   title = {{Efficient Verification of the PCI Local Bus using Boolean Satisfiability}},\n   booktitle = {International Workshop on Logic Synthesis (IWLS)},\n   address = {Dana Point, California},\n   pages = {131-135},\n   month = {June},\n   year = {2000}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An Experimental Evaluation of Conflict Diagnosis and Recursive Learning in Boolean Satisfiability.\n \n \n \n\n\n \n Aloul, F. A.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Workshop on Logic Synthesis (IWLS), pages 117-121, Dana Point, California, June 2000. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{aloul2000aexperimental,\n   author = {Aloul, Fadi A. and Sakallah, Karem A.},\n   title = {{An Experimental Evaluation of Conflict Diagnosis and Recursive Learning in Boolean Satisfiability}},\n   booktitle = {International Workshop on Logic Synthesis (IWLS)},\n   address = {Dana Point, California},\n   pages = {117-121},\n   month = {June},\n   year = {2000}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Improving SAT: Stack-based Incremental Satisfiability.\n \n \n \n\n\n \n Kim, J.; Whittemore, J.; Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Workshop on Logic Synthesis (IWLS), pages 181-184, Dana Point, California, June 2000. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kim2000improving,\n   author = {Kim, Joonyoung and Whittemore, Jesse and Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{Improving SAT: Stack-based Incremental Satisfiability}},\n   booktitle = {International Workshop on Logic Synthesis (IWLS)},\n   address = {Dana Point, California},\n   pages = {181-184},\n   month = {June},\n   year = {2000}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Structure-Aware Functional Decomposition in Logic Synthesis.\n \n \n \n\n\n \n Kravets, V. N.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Workshop on Logic Synthesis (IWLS), pages 81-90, Dana Point, California, June 2000. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kravets2000astructure,\n   author = {Kravets, Victor N. and Sakallah, Karem A.},\n   title = {{Structure-Aware Functional Decomposition in Logic Synthesis}},\n   booktitle = {International Workshop on Logic Synthesis (IWLS)},\n   address = {Dana Point, California},\n   pages = {81-90},\n   month = {June},\n   year = {2000}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Boolean Satisfiability in Electronic Design Automation.\n \n \n \n\n\n \n Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. 37th IEEE/ACM Design Automation Conference (DAC), pages 675-680, Los Angeles, California, June 2000. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{marquessilva2000boolean,\n   author = {Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{Boolean Satisfiability in Electronic Design Automation}},\n   booktitle = {Proc. 37th IEEE/ACM Design Automation Conference (DAC)},\n   address = {Los Angeles, California},\n   pages = {675-680},\n   month = {June},\n   year = {2000}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Functional Timing Analysis—False Path elimination in Timing Verification.\n \n \n \n\n\n \n Sakallah, K. A.\n\n\n \n\n\n\n In TAU '00—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, pages 82-83, Austin, Texas, December 2000. \n Invited Talk\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah2000functional,\n   author = {Sakallah, K. A.},\n   title = {{Functional Timing Analysis—False Path elimination in Timing Verification}},\n   booktitle = {TAU '00—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems},\n   address = {Austin, Texas},\n   pages = {82-83},\n   month = {December},\n   note = {Invited Talk},\n   year = {2000}\n\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1999\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1999\n \n \n (9)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n GRASP: A Search Algorithm for Propositional Satisfiability.\n \n \n \n\n\n \n Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n IEEE Transactions on Computers, 48(5): 506-521. May 1999.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{marquessilva1999grasp,\n   author = {Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{GRASP: A Search Algorithm for Propositional Satisfiability}},\n   journal = {IEEE Transactions on Computers},\n   volume = {48},\n   number = {5},\n   pages = {506-521},\n   month = {May},\n   year = {1999}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Timing Verification of Sequential Dynamic Circuits.\n \n \n \n\n\n \n Van Campenhout, D.; Mudge, T.; and Sakallah, K. A.\n\n\n \n\n\n\n IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 18(5): 645-658. May 1999.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{vancampenhout1999timing,\n   author = {Van Campenhout, David and Mudge, Trevor and Sakallah, Karem A.},\n   title = {{Timing Verification of Sequential Dynamic Circuits}},\n   journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n   volume = {18},\n   number = {5},\n   pages = {645-658},\n   month = {May},\n   year = {1999}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Functional Timing Analysis for IP Characterization.\n \n \n \n\n\n \n Yalcin, H.; Mortazavi, M.; Palermo, R.; Bamji, C.; and Sakallah, K.\n\n\n \n\n\n\n In TAU99—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, pages 59-64, Monterey, California, March 1999. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{yalcin1999functional,\n   author = {Yalcin, H. and Mortazavi, M. and Palermo, R. and Bamji, C. and Sakallah, K.},\n   title = {{Functional Timing Analysis for IP Characterization}},\n   booktitle = {TAU99—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems},\n   address = {Monterey, California},\n   pages = {59-64},\n   month = {March},\n   year = {1999}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Incremental Satisfiability and Its Application to Delay Fault Testing.\n \n \n \n\n\n \n Kim, J.; Whittemore, J.; Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Workshop on Logic Synthesis (IWLS), pages 242-245, Granlibakken, California, June 1999. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kim1999incremental,\n   author = {Kim, Joonyoung and Whittemore, Jesse and Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{Incremental Satisfiability and Its Application to Delay Fault Testing}},\n   booktitle = {International Workshop on Logic Synthesis (IWLS)},\n   address = {Granlibakken, California},\n   pages = {242-245},\n   month = {June},\n   year = {1999}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Functional Timing Analysis for IP Characterization.\n \n \n \n\n\n \n Yalcin, H.; Mortazavi, M.; Palermo, R.; Bamji, C.; and Sakallah, K.\n\n\n \n\n\n\n In Proc. IEEE/ACM Design Automation Conference, pages 731-736, New Orleans, Louisiana, June 1999. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{yalcin1999afunctional,\n   author = {Yalcin, Hakan and Mortazavi, Mohammad and Palermo, Robert and Bamji, Cyrus and Sakallah, Karem},\n   title = {{Functional Timing Analysis for IP Characterization}},\n   booktitle = {Proc. IEEE/ACM Design Automation Conference},\n   address = {New Orleans, Louisiana},\n   pages = {731-736},\n   month = {June},\n   year = {1999}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Satisfiability-Based Detailed FPGA Routing.\n \n \n \n\n\n \n Nam, G.; Sakallah, K. A.; and Rutenbar, R. A\n\n\n \n\n\n\n In Twelfth International Conference on VLSI Design, pages 574-577, Goa, India, January 7-10 1999. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{nam1999satisfiability,\n   author = {Nam, Gi-Joon and Sakallah, Karem A. and Rutenbar, Rob A},\n   title = {{Satisfiability-Based Detailed FPGA Routing}},\n   booktitle = {Twelfth International Conference on VLSI Design},\n   address = {Goa, India},\n   pages = {574-577},\n   month = {January 7-10},\n   year = {1999}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Satisfiability-Based Layout Revisited: Detailed Routing of Complex FPGAs Via Search-Based Boolean SAT.\n \n \n \n\n\n \n Nam, G.; Sakallah, K. A.; and Rutenbar, R. A.\n\n\n \n\n\n\n In Proc. ACM/SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA'99), pages 167-175, Monterey, California, February 21-23, 1999 1999. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{nam1999asatisfiability,\n   author = {Nam, Gi-Joon and Sakallah, Karem A. and Rutenbar, Rob A.},\n   title = {{Satisfiability-Based Layout Revisited: Detailed Routing of Complex FPGAs Via Search-Based Boolean SAT}},\n   booktitle = {Proc. ACM/SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA'99)},\n   address = {Monterey, California},\n   pages = {167-175},\n   month = {February 21-23, 1999},\n   year = {1999}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Satisfiability-Based Functional Delay Fault Testing.\n \n \n \n\n\n \n Kim, J.; Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. IFIP TC10 WG10.5 Tenth International Conference on Very Large Scale Integration (VLSI '99), pages 362-372, Lisbon, Portugal, December 1999. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kim1999satisfiability,\n   author = {Kim, Joonyoung and Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{Satisfiability-Based Functional Delay Fault Testing}},\n   booktitle = {Proc. IFIP TC10 WG10.5 Tenth International Conference on Very Large Scale Integration (VLSI '99)},\n   address = {Lisbon, Portugal},\n   pages = {362-372},\n   month = {December},\n   year = {1999}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Transistor Level Micro-Placement and Routing for Two-Dimensional Digital VLSI Cell Synthesis.\n \n \n \n\n\n \n Riepe, M. A.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Symposium on Physical Design (ISPD-99), pages 74-81, Monterey, California, April 12-14 1999. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{riepe1999transistor,\n   author = {Riepe, Michael A. and Sakallah, Karem A.},\n   title = {{Transistor Level Micro-Placement and Routing for Two-Dimensional Digital VLSI Cell Synthesis}},\n   booktitle = {International Symposium on Physical Design (ISPD-99)},\n   address = {Monterey, California},\n   pages = {74-81},\n   month = {April 12-14},\n   year = {1999}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1998\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1998\n \n \n (10)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Timing Analysis Using Propositional Satisfiability.\n \n \n \n\n\n \n e Silva, L. G.; Marques-Silva, J.; Silveira, L. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In 5th International Conference on Electronics, Circuits, and Systems (ICECS98), pages 95-98, Lisbon, Portugal, September 1998. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{esilva1998timing,\n   author = {e Silva, Luis Guerra and Marques-Silva, {J\\~oao} and Silveira, Luis Miguel and Sakallah, Karem A.},\n   title = {{Timing Analysis Using Propositional Satisfiability}},\n   booktitle = {5th International Conference on Electronics, Circuits, and Systems (ICECS98)},\n   address = {Lisbon, Portugal},\n   pages = {95-98},\n   month = {September},\n   year = {1998}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n False Path Analysis in Sequential Circuits.\n \n \n \n\n\n \n Bell, J. L.; Sakallah, K. A.; and Whittemore, J. P.\n\n\n \n\n\n\n In 8th International Workshop on Power and Timing Modeling, Optimization and Simulation (PATMOS98), pages 245-254, Lyngby, Denmark, October 1998. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{bell1998false,\n   author = {Bell, Jeffery L. and Sakallah, Karem A. and Whittemore, Jesse P.},\n   title = {{False Path Analysis in Sequential Circuits}},\n   booktitle = {8th International Workshop on Power and Timing Modeling, Optimization and Simulation (PATMOS98)},\n   address = {Lyngby, Denmark},\n   pages = {245-254},\n   month = {October},\n   year = {1998}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Satisfiability-Based Algorithms for 0-1 Integer Programming.\n \n \n \n\n\n \n Manquinho, V.; Marques-Silva, J.; Oliveira, A.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. of the International Workshop on Logic Synthesis (IWLS), pages 25-34, Lake Tahoe, California, May 1998. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{manquinho1998satisfiability,\n   author = {Manquinho, V. and Marques-Silva, {J\\~oao} and Oliveira, A. and Sakallah, K. A.},\n   title = {{Satisfiability-Based Algorithms for 0-1 Integer Programming}},\n   booktitle = {Proc. of the International Workshop on Logic Synthesis (IWLS)},\n   address = {Lake Tahoe, California},\n   pages = {25-34},\n   month = {May},\n   year = {1998}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Functional Timing Analysis for IP Characterization.\n \n \n \n\n\n \n Yalcin, H.; Mortazavi, M.; Palermo, R.; Bamji, C.; and Sakallah, K.\n\n\n \n\n\n\n In Cadence Technical Conference, pages 544-549, San Antonio, Texas, May 1998. \n Best Paper Award\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{yalcin1998functional,\n   author = {Yalcin, H. and Mortazavi, M. and Palermo, R. and Bamji, C. and Sakallah, K.},\n   title = {{Functional Timing Analysis for IP Characterization}},\n   booktitle = {Cadence Technical Conference},\n   address = {San Antonio, Texas},\n   pages = {544-549},\n   month = {May},\n   note = {Best Paper Award},\n   year = {1998}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Overview of Complementary GaAs Technology for High-Speed VLSI Circuits.\n \n \n \n\n\n \n Brown, R. B.; Bernhardt, B.; LaMacchia, M.; Abrokwah, J.; Parakh, P. N.; Basso, T. D.; Gold, S. M.; Stetson, S.; Gauthier, C. R.; Foster, D.; Crawforth, B.; McQuire, T.; Sakallah, K. A.; Lomax, R. J.; and Mudge, T. N.\n\n\n \n\n\n\n IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 6(1): 47-51. March 1998.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{brown1998overview,\n   author = {Brown, Richard B. and Bernhardt, Bruce and LaMacchia, Mike and Abrokwah, Jon and Parakh, Phiroze N. and Basso, Todd D. and Gold, Spencer M. and Stetson, Sean and Gauthier, Claude R. and Foster, David and Crawforth, Brian and McQuire, Timothy and Sakallah, Karem A. and Lomax, Ronald J. and Mudge, Trevor N.},\n   title = {{Overview of Complementary GaAs Technology for High-Speed VLSI Circuits}},\n   journal = {IEEE Transactions on Very Large Scale Integration (VLSI) Systems},\n   volume = {6},\n   number = {1},\n   pages = {47-51},\n   month = {March},\n   year = {1998}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Realistic Delay Modeling in Satisfiability-Based Timing Analysis.\n \n \n \n\n\n \n e Silva, L. G.; Marques-Silva, J.; Silveira, L. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Symposium on Circuits and Systems (ISCAS98), pages 215-218, Monterey, California, June 1998. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{esilva1998realistic,\n   author = {e Silva, Luis Guerra and Marques-Silva, {J\\~oao} and Silveira, Luis Miguel and Sakallah, Karem A.},\n   title = {{Realistic Delay Modeling in Satisfiability-Based Timing Analysis}},\n   booktitle = {International Symposium on Circuits and Systems (ISCAS98)},\n   address = {Monterey, California},\n   pages = {215-218},\n   month = {June},\n   year = {1998}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n M32: A Constructive Multilevel Logic Synthesis System.\n \n \n \n\n\n \n Kravets, V. N.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. 35th IEEE/ACM Design Automation Conference (DAC), pages 336-341, San Francisco, California, June 1998. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kravets1998m32,\n   author = {Kravets, Victor N. and Sakallah, Karem A.},\n   title = {{M32: A Constructive Multilevel Logic Synthesis System}},\n   booktitle = {Proc. 35th IEEE/ACM Design Automation Conference (DAC)},\n   address = {San Francisco, California},\n   pages = {336-341},\n   month = {June},\n   year = {1998}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Congestion Driven Quadratic Placement.\n \n \n \n\n\n \n Parakh, P. N.; Brown, R. B.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. 35th IEEE/ACM Design Automation Conference (DAC), pages 275-278, San Francisco, California, June 1998. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{parakh1998congestion,\n   author = {Parakh, Phiroze N. and Brown, Richard B. and Sakallah, Karem A.},\n   title = {{Congestion Driven Quadratic Placement}},\n   booktitle = {Proc. 35th IEEE/ACM Design Automation Conference (DAC)},\n   address = {San Francisco, California},\n   pages = {275-278},\n   month = {June},\n   year = {1998}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The Edge-Based Design Rule Model Revisited.\n \n \n \n\n\n \n Riepe, M. A.; and Sakallah, K. A.\n\n\n \n\n\n\n ACM Transactions on Design Automation of Electronic Systems (TODAES), 3(3): 463-486. July 1998.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{riepe1998edge,\n   author = {Riepe, Michael A. and Sakallah, Karem A.},\n   title = {{The Edge-Based Design Rule Model Revisited}},\n   journal = {ACM Transactions on Design Automation of Electronic Systems (TODAES)},\n   volume = {3},\n   number = {3},\n   pages = {463-486},\n   month = {July},\n   year = {1998}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n AFTA: A Formal Delay Model for Functional Timing Analysis.\n \n \n \n\n\n \n Chandramouli, V.; Whittemore, J. P.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proceedings of the Design, Automation and Test in Europe Conference (DATE98), pages 350-355, Paris, France, February 1998. \n Best Paper Nominee\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{chandramouli1998afta,\n   author = {Chandramouli, V. and Whittemore, Jesse Paul and Sakallah, Karem A.},\n   title = {{AFTA: A Formal Delay Model for Functional Timing Analysis}},\n   booktitle = {Proceedings of the Design, Automation and Test in Europe Conference (DATE98)},\n   address = {Paris, France},\n   pages = {350-355},\n   month = {February},\n   note = {Best Paper Nominee},\n   year = {1998}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1997\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1997\n \n \n (14)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Signal Delay in Coupled, Distributed RC Lines in the Presence of Temporal Proximity.\n \n \n \n\n\n \n Chandramouli, V.; Kayssi, A.; and Sakallah, K. A.\n\n\n \n\n\n\n In Brown, R. B.; and Ishii, A. T., editor(s), Proc. 17th Advanced Research in VLSI (ARVLSI), pages 32-46, Ann Arbor, Michigan, September 1997. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{chandramouli1997signal,\n   author = {Chandramouli, V. and Kayssi, Ayman and Sakallah, Karem A.},\n   title = {{Signal Delay in Coupled,  Distributed RC Lines in the Presence of Temporal Proximity}},\n   booktitle = {Proc. 17th Advanced Research in VLSI (ARVLSI)},\n   editor = {Brown, Richard B. and Ishii, Alexander T.},\n   address = {Ann Arbor, Michigan},\n   pages = {32-46},\n   month = {September},\n   year = {1997}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Design Verification: How Do We Know That These 100-Million Transistor Chips Will Work?.\n \n \n \n\n\n \n Sakallah, K. A.\n\n\n \n\n\n\n In Proc. Second LAAS International Conference on Computer Simulation, pages 1-3, Beirut, Lebanon, September 1997. \n Invited talk\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah1997design,\n   author = {Sakallah, Karem A.},\n   title = {{Design Verification: How Do We Know That These 100-Million Transistor Chips Will Work?}},\n   booktitle = {Proc. Second LAAS International Conference on Computer Simulation},\n   address = {Beirut, Lebanon},\n   pages = {1-3},\n   month = {September},\n   note = {Invited talk},\n   year = {1997}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Waveform Calculus for Timing Analysis of Digital Circuits.\n \n \n \n\n\n \n Whittemore, J. P.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. Second LAAS International Conference on Computer Simulation, pages 231-235, Beirut, Lebanon, September 1997. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{whittemore1997waveform,\n   author = {Whittemore, Jesse Paul and Sakallah, Karem A.},\n   title = {{Waveform Calculus for Timing Analysis of Digital Circuits}},\n   booktitle = {Proc. Second LAAS International Conference on Computer Simulation},\n   address = {Beirut, Lebanon},\n   pages = {231-235},\n   month = {September},\n   year = {1997}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Synchronizers and Clocking Schemes in Digital Systems.\n \n \n \n\n\n \n Chandramouli, V.; and Sakallah, K. A.\n\n\n \n\n\n\n In International Workshop on Clock Distribution Networks-Design, Synthesis, and Analysis, Atlanta, Georgia, October 1997. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{chandramouli1997synchronizers,\n   author = {Chandramouli, V. and Sakallah, Karem A.},\n   title = {{Synchronizers and Clocking Schemes in Digital Systems}},\n   booktitle = {International Workshop on Clock Distribution Networks-Design, Synthesis, and Analysis},\n   address = {Atlanta, Georgia},\n   month = {October},\n   year = {1997}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Application of System-Level EM Modeling to High-Speed Digital IC Packages and PCB's.\n \n \n \n\n\n \n Yook, J.; Katehi, L. P. B.; Sakallah, K. A.; Martin, R. S.; Huang, L.; and Schreyer, T. A.\n\n\n \n\n\n\n IEEE Transactions on Microwave Theory and Techniques, 45(10): 1847-1856. October 1997.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{yook1997application,\n   author = {Yook, Jong-Gwan and Katehi, Linda P. B. and Sakallah, Karem A. and Martin, Ray S. and Huang, Lilly and Schreyer, Tim A.},\n   title = {{Application of System-Level EM Modeling to High-Speed Digital IC Packages and PCB's}},\n   journal = {IEEE Transactions on Microwave Theory and Techniques},\n   volume = {45},\n   number = {10},\n   pages = {1847-1856},\n   month = {October},\n   year = {1997}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n RID-GRASP: Redundancy Identification and Removal Using GRASP.\n \n \n \n\n\n \n Kim, J.; Marques-Silva, J.; Savoj, H.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. of the International Workshop on Logic Synthesis (IWLS), Lake Tahoe, California, May 1997. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kim1997rid,\n   author = {Kim, Joonyoung and Marques-Silva, {J\\~oao} and Savoj, Hamid and Sakallah, Karem A.},\n   title = {{RID-GRASP: Redundancy Identification and Removal Using GRASP}},\n   booktitle = {Proc. of the International Workshop on Logic Synthesis (IWLS)},\n   address = {Lake Tahoe, California},\n   month = {May},\n   year = {1997}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n RID-GRASP: Redundancy Identification and Removal Using GRASP.\n \n \n \n\n\n \n Kim, J.; Marques-Silva, J.; Savoj, H.; and Sakallah, K. A.\n\n\n \n\n\n\n In Cadence Technical Conference, pages 131-134, Keystone, Colorado, May 1997. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kim1997arid,\n   author = {Kim, Joonyoung and Marques-Silva, {J\\~oao} and Savoj, Hamid and Sakallah, Karem A.},\n   title = {{RID-GRASP: Redundancy Identification and Removal Using GRASP}},\n   booktitle = {Cadence Technical Conference},\n   address = {Keystone, Colorado},\n   pages = {131-134},\n   month = {May},\n   year = {1997}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Test Pattern Generation for Circuits Using Power Management Techniques.\n \n \n \n\n\n \n Marques-Silva, J.; Monteiro, J. C.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. European Test Workshop (ETW), Cagliari, Italy, May 1997. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{marquessilva1997test,\n   author = {Marques-Silva, {J\\~oao} and Monteiro, Jose C. and Sakallah, Karem A.},\n   title = {{Test Pattern Generation for Circuits Using Power Management Techniques}},\n   booktitle = {Proc. European Test Workshop (ETW)},\n   address = {Cagliari, Italy},\n   month = {May},\n   year = {1997}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Timing Abstraction of Intellectual Property Blocks.\n \n \n \n\n\n \n Venkatesh, S. V.; Palermo, R.; Mortazavi, M.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. Custom Integrated Circuits Conference (CICC), pages 99-102, Santa Clara, California, May 1997. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{venkatesh1997timing,\n   author = {Venkatesh, S. V. and Palermo, Robert and Mortazavi, Mohammad and Sakallah, Karem A.},\n   title = {{Timing Abstraction of Intellectual Property Blocks}},\n   booktitle = {Proc. Custom Integrated Circuits Conference (CICC)},\n   address = {Santa Clara, California},\n   pages = {99-102},\n   month = {May},\n   year = {1997}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Computation of Switching Noise in Printed Circuit Boards.\n \n \n \n\n\n \n Yook, J.; Chandramouli, V.; Katehi, L. P. B.; Sakallah, K. A.; Arabi, T. R.; and Schreyer, T. A.\n\n\n \n\n\n\n IEEE Transactions on Components, Packaging, and Manufacturing Technology—Part A, 20(1): 64-75. March 1997.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{yook1997computation,\n   author = {Yook, Jong-Gwan and Chandramouli, V. and Katehi, Linda P. B. and Sakallah, Karem A. and Arabi, Tawfik R. and Schreyer, Tim A.},\n   title = {{Computation of Switching Noise in Printed Circuit Boards}},\n   journal = {IEEE Transactions on Components, Packaging, and Manufacturing Technology—Part A},\n   volume = {20},\n   number = {1},\n   pages = {64-75},\n   month = {March},\n   year = {1997}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Robust Search Algorithms for Test Pattern Generation.\n \n \n \n\n\n \n Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. Fault-Tolerant Computing Symposium (FTCS), pages 152-161, Seattle, Washington, June 1997. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{marquessilva1997robust,\n   author = {Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{Robust Search Algorithms for Test Pattern Generation}},\n   booktitle = {Proc. Fault-Tolerant Computing Symposium (FTCS)},\n   address = {Seattle, Washington},\n   pages = {152-161},\n   month = {June},\n   year = {1997}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n AFTA: A Delay Model for Functional Timing Analysis.\n \n \n \n\n\n \n Chandramouli, V.; Whittemore, J. P.; and Sakallah, K. A.\n\n\n \n\n\n\n In TAU97-ACM/IEEE International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, pages 5-14, Austin, Texas, December 1997. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{chandramouli1997afta,\n   author = {Chandramouli, V. and Whittemore, Jesse Paul and Sakallah, Karem A.},\n   title = {{AFTA: A Delay Model for Functional Timing Analysis}},\n   booktitle = {TAU97-ACM/IEEE International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems},\n   address = {Austin, Texas},\n   pages = {5-14},\n   month = {December},\n   year = {1997}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Satisfiability Models and Algorithms for Circuit Delay Computation.\n \n \n \n\n\n \n e Silva, L. G.; Marques-Silva, J.; Silveira, L. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In TAU97-ACM/IEEE International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, pages 57-62, Austin, Texas, December 1997. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{esilva1997satisfiability,\n   author = {e Silva, Luis Guerra and Marques-Silva, {J\\~oao} and Silveira, Luis Miguel and Sakallah, Karem A.},\n   title = {{Satisfiability Models and Algorithms for Circuit Delay Computation}},\n   booktitle = {TAU97-ACM/IEEE International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems},\n   address = {Austin, Texas},\n   pages = {57-62},\n   month = {December},\n   year = {1997}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Selection of Voltage Thresholds for Delay Measurement.\n \n \n \n\n\n \n Chandramouli, V.; and Sakallah, K. A.\n\n\n \n\n\n\n Special issue on Analog Design Issues in Digital VLSI Circuits and Systems, Journal of Analog Integrated Circuits and Signal Processing (AICSP), 14(1/2): 9-28. 1997.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{chandramouli1997selection,\n   author = {Chandramouli, V. and Sakallah, Karem A.},\n   title = {{Selection of Voltage Thresholds for Delay Measurement}},\n   journal = {Special issue on Analog Design Issues in Digital VLSI Circuits and Systems, Journal of Analog Integrated Circuits and Signal Processing (AICSP)},\n   volume = {14},\n   number = {1/2},\n   pages = {9-28},\n   year = {1997}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1996\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1996\n \n \n (10)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Static Timing Analysis of Sequential Domino Circuits.\n \n \n \n\n\n \n Van Campenhout, D.; Mudge, T.; and Sakallah, K. A.\n\n\n \n\n\n\n In TECHCON, Phoenix, Arizona, September 1996. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{vancampenhout1996static,\n   author = {Van Campenhout, David and Mudge, Trevor and Sakallah, Karem A.},\n   title = {{Static Timing Analysis of Sequential Domino Circuits}},\n   booktitle = {TECHCON},\n   address = {Phoenix, Arizona},\n   month = {September},\n   year = {1996}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Symbolic Calculus for Timing Analysis of Digital Circuits.\n \n \n \n\n\n \n Whittemore, J. P.; and Sakallah, K. A.\n\n\n \n\n\n\n In TECHCON, Phoenix, Arizona, September 1996. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{whittemore1996symbolic,\n   author = {Whittemore, Jesse Paul and Sakallah, Karem A.},\n   title = {{A Symbolic Calculus for Timing Analysis of Digital Circuits}},\n   booktitle = {TECHCON},\n   address = {Phoenix, Arizona},\n   month = {September},\n   year = {1996}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n System Level EM Modeling of Digital IC Packages and PC Boards.\n \n \n \n\n\n \n Yook, J.; Arabi, T.; Schreyer, T.; Katehi, L. P.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. 5th Topical Meeting on Electrical Performance of Electronic Packaging (EPEP'96), pages 238-240, Napa, California, October 1996. IEEE\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{yook1996system,\n   author = {Yook, Jong-Gwan and Arabi, Tawfik and Schreyer, Tim and Katehi, Linda P. and Sakallah, Karem A.},\n   title = {{System Level EM Modeling of Digital IC Packages and PC Boards}},\n   booktitle = {Proc. 5th Topical Meeting on Electrical Performance of Electronic Packaging (EPEP'96)},\n   address = {Napa, California},\n   publisher = {IEEE},\n   pages = {238-240},\n   month = {October},\n   year = {1996}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n GRASP-A New Search Algorithm for Satisfiability.\n \n \n \n\n\n \n Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 220-227, San Jose, California, November 1996. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{marquessilva1996grasp,\n   author = {Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{GRASP-A New Search Algorithm for Satisfiability}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {San Jose, California},\n   pages = {220-227},\n   month = {November},\n   year = {1996}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Conflict Analysis in Search Algorithms for Propositional Satisfiability.\n \n \n \n\n\n \n Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. 8th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'96), pages 467-469, Toulouse, France, November 1996. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{marquessilva1996conflict,\n   author = {Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{Conflict Analysis in Search Algorithms for Propositional Satisfiability}},\n   booktitle = {Proc. 8th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'96)},\n   address = {Toulouse, France},\n   pages = {467-469},\n   month = {November},\n   year = {1996}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Timing Verification of Sequential Domino Circuits.\n \n \n \n\n\n \n Van Campenhout, D.; Mudge, T.; and Sakallah, K. A.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 127-132, San Jose, California, November 1996. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{vancampenhout1996timing,\n   author = {Van Campenhout, David and Mudge, Trevor and Sakallah, Karem A.},\n   title = {{Timing Verification of Sequential Domino Circuits}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {San Jose, California},\n   pages = {127-132},\n   month = {November},\n   year = {1996}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An Approximate Timing Analysis Method for Datapath Circuits.\n \n \n \n\n\n \n Yalcin, H.; Hayes, J. P.; and Sakallah, K. A.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 114-118, San Jose, California, November 1996. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{yalcin1996approximate,\n   author = {Yalcin, Hakan and Hayes, John P. and Sakallah, Karem A.},\n   title = {{An Approximate Timing Analysis Method for Datapath Circuits}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {San Jose, California},\n   pages = {114-118},\n   month = {November},\n   year = {1996}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Block Characterization: Timing Abstraction of Megacells.\n \n \n \n\n\n \n Venkatesh, S. V.; Mortazavi, M.; Palermo, R.; and Sakallah, K.\n\n\n \n\n\n\n In Cadence Technical Conference, pages 184-191, Napa, California, May 1996. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{venkatesh1996block,\n   author = {Venkatesh, S. V. and Mortazavi, Mohammad and Palermo, Robert and Sakallah, Karem},\n   title = {{Block Characterization: Timing Abstraction of Megacells}},\n   booktitle = {Cadence Technical Conference},\n   address = {Napa, California},\n   pages = {184-191},\n   month = {May},\n   year = {1996}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Ravel-XL: A Hardware Accelerator for Assigned-Delay Compiled-Code Logic Gate Simulation.\n \n \n \n\n\n \n Riepe, M. A.; Marques-Silva, J.; Sakallah, K. A.; and Brown, R. B.\n\n\n \n\n\n\n IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 4(1): 113-129. March 1996.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{riepe1996ravel,\n   author = {Riepe, Michael A. and Marques-Silva, {J\\~oao} and Sakallah, Karem A. and Brown, Richard B.},\n   title = {{Ravel-XL: A Hardware Accelerator for Assigned-Delay Compiled-Code Logic Gate Simulation}},\n   journal = {IEEE Transactions on Very Large Scale Integration (VLSI) Systems},\n   volume = {4},\n   number = {1},\n   pages = {113-129},\n   month = {March},\n   year = {1996}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Modeling the Effects of Temporal Proximity of Input Transitions on Output Delay and Transition Times.\n \n \n \n\n\n \n Chandramouli, V.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. IEEE/ACM Design Automation Conference (DAC), pages 617-622, Las Vegas, Nevada, June 1996. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{chandramouli1996modeling,\n   author = {Chandramouli, V. and Sakallah, Karem A.},\n   title = {{Modeling the Effects of Temporal Proximity of Input Transitions on Output Delay and Transition Times}},\n   booktitle = {Proc. IEEE/ACM Design Automation Conference (DAC)},\n   address = {Las Vegas, Nevada},\n   pages = {617-622},\n   month = {June},\n   year = {1996}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1995\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1995\n \n \n (8)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Macromodeling and Simulation of RC Interconnection Circuits.\n \n \n \n\n\n \n Kayssi, A. I.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. First LAAS International Conference on Computer Simulation (ICCS'95), pages 207-212, American University of Beirut, Lebanon, September 1995. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kayssi1995macromodeling,\n   author = {Kayssi, Ayman I. and Sakallah, Karem A.},\n   title = {{Macromodeling and Simulation of RC Interconnection Circuits}},\n   booktitle = {Proc. First LAAS International Conference on Computer Simulation (ICCS'95)},\n   address = {American University of Beirut, Lebanon},\n   pages = {207-212},\n   month = {September},\n   year = {1995}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Computation of Switching Noise in PCBs for Digital Packages.\n \n \n \n\n\n \n Yook, J.; Chandramouli, V.; Katehi, L. P.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. 4th Topical Meeting on Electrical Performance of Electronic Packaging (EPEP'95), pages 37-39, Portland, Oregon, October 1995. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{yook1995acomputation,\n   author = {Yook, Jong-Gwan and Chandramouli, V. and Katehi, Linda P. and Sakallah, Karem A.},\n   title = {{Computation of Switching Noise in PCBs for Digital Packages}},\n   booktitle = {Proc. 4th Topical Meeting on Electrical Performance of Electronic Packaging (EPEP'95)},\n   address = {Portland, Oregon},\n   pages = {37-39},\n   month = {October},\n   year = {1995}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Dynamic Modeling of Logic Gate Circuits.\n \n \n \n\n\n \n Sakallah, K. A.\n\n\n \n\n\n\n In TAU'95: ACM/SIGDA International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, pages 103-120, Seattle, Washington, November 1995. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah1995dynamic,\n   author = {Sakallah, Karem A.},\n   title = {{Dynamic Modeling of Logic Gate Circuits}},\n   booktitle = {TAU'95: ACM/SIGDA International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems},\n   address = {Seattle, Washington},\n   pages = {103-120},\n   month = {November},\n   year = {1995}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Timing Models for Gallium Arsenide Direct-Coupled FET Logic Circuits.\n \n \n \n\n\n \n Kayssi, A. I.; and Sakallah, K. A.\n\n\n \n\n\n\n IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 14(3): 384-393. March 1995.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{kayssi1995timing,\n   author = {Kayssi, Ayman I. and Sakallah, Karem A.},\n   title = {{Timing Models for Gallium Arsenide Direct-Coupled FET Logic Circuits}},\n   journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n   volume = {14},\n   number = {3},\n   pages = {384-393},\n   month = {March},\n   year = {1995}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Critical Paths in Circuits with Level-Sensitive Latches.\n \n \n \n\n\n \n Burks, T. M.; Sakallah, K. A.; and Mudge, T. N.\n\n\n \n\n\n\n IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 3(2): 273-291. June 1995.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{burks1995critical,\n   author = {Burks, Timothy M. and Sakallah, Karem A. and Mudge, Trevor N.},\n   title = {{Critical Paths in Circuits with Level-Sensitive Latches}},\n   journal = {IEEE Transactions on Very Large Scale Integration (VLSI) Systems},\n   volume = {3},\n   number = {2},\n   pages = {273-291},\n   month = {June},\n   year = {1995}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The Aurora RAM Compiler.\n \n \n \n\n\n \n Chandna, A.; Kibler, C. D.; Brown, R. B.; Roberts, M.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. IEEE/ACM Design Automation Conference (DAC), pages 261-266, San Francisco, California, June 1995. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{chandna1995aurora,\n   author = {Chandna, Ajay and Kibler, C. David and Brown, Richard B. and Roberts, Mark and Sakallah, Karem A.},\n   title = {{The Aurora RAM Compiler}},\n   booktitle = {Proc. IEEE/ACM Design Automation Conference (DAC)},\n   address = {San Francisco, California},\n   pages = {261-266},\n   month = {June},\n   year = {1995}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Computation of Switching Noise in Printed Circuit Boards.\n \n \n \n\n\n \n Yook, J.; Chandramouli, V.; Katehi, L.; and Sakallah, K. A.\n\n\n \n\n\n\n In Progress in Electromagnetics Research Symposium, Seattle, Washington, July 1995. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{yook1995computation,\n   author = {Yook, J. and Chandramouli, V. and Katehi, L. and Sakallah, K. A.},\n   title = {{Computation of Switching Noise in Printed Circuit Boards}},\n   booktitle = {Progress in Electromagnetics Research Symposium},\n   address = {Seattle, Washington},\n   month = {July},\n   year = {1995}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Maximum Rate Single-Phase Clocking of a Closed Pipeline including Wave Pipelining, Stoppability, and Startability.\n \n \n \n\n\n \n Chang, C.; Davidson, E. S.; and Sakallah, K. A.\n\n\n \n\n\n\n IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 14(12): 1526-1545. December 1995.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{chang1995maximum,\n   author = {Chang, Chuan-Hua and Davidson, Edward S. and Sakallah, Karem A.},\n   title = {{Maximum Rate Single-Phase Clocking of a Closed Pipeline including Wave Pipelining, Stoppability, and Startability}},\n   journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n   volume = {14},\n   number = {12},\n   pages = {1526-1545},\n   month = {December},\n   year = {1995}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1994\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1994\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Optimization of Critical Paths in Circuits with Level-Sensitive Latches.\n \n \n \n\n\n \n Burks, T. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 468-473, San Jose, California, November 1994. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{burks1994optimization,\n   author = {Burks, Timothy M. and Sakallah, Karem A.},\n   title = {{Optimization of Critical Paths in Circuits with Level-Sensitive Latches}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {San Jose, California},\n   pages = {468-473},\n   month = {November},\n   year = {1994}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Delay Macromodels for Point-to-Point MCM Interconnections.\n \n \n \n\n\n \n Kayssi, A. I.; and Sakallah, K. A.\n\n\n \n\n\n\n IEEE Transactions on Components, Packaging and Manufacturing Technology—Part B, 17(2): 147-152. May 1994.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{kayssi1994delay,\n   author = {Kayssi, Ayman I. and Sakallah, Karem A.},\n   title = {{Delay Macromodels for Point-to-Point MCM Interconnections}},\n   journal = {IEEE Transactions on Components, Packaging and Manufacturing Technology—Part B},\n   volume = {17},\n   number = {2},\n   pages = {147-152},\n   month = {May},\n   year = {1994}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Macromodel Simplification Using Dimensional Analysis.\n \n \n \n\n\n \n Kayssi, A. I.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. IEEE International Symposium on Circuits and Systems (ISCAS), volume 1, pages 335-338, London, England, June 1994. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kayssi1994macromodel,\n   author = {Kayssi, Ayman I. and Sakallah, Karem A.},\n   title = {{Macromodel Simplification Using Dimensional Analysis}},\n   booktitle = {Proc. IEEE International Symposium on Circuits and Systems (ISCAS)},\n   address = {London, England},\n   volume = {1},\n   pages = {335-338},\n   month = {June},\n   year = {1994}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Efficient and Robust Test Generation-Based Timing Analysis.\n \n \n \n\n\n \n Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. IEEE International Symposium on Circuits and Systems (ISCAS), volume 1, pages 303-306, London, England, June 1994. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{marquessilva1994efficient,\n   author = {Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{Efficient and Robust Test Generation-Based Timing Analysis}},\n   booktitle = {Proc. IEEE International Symposium on Circuits and Systems (ISCAS)},\n   address = {London, England},\n   volume = {1},\n   pages = {303-306},\n   month = {June},\n   year = {1994}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Dynamic Search-Space Pruning Techniques in Path Sensitization.\n \n \n \n\n\n \n Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. IEEE/ACM Design Automation Conference (DAC), pages 705-711, San Diego, California, June 1994. \n Best Paper Nominee\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{marquessilva1994dynamic,\n   author = {Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{Dynamic Search-Space Pruning Techniques in Path Sensitization}},\n   booktitle = {Proc. IEEE/ACM Design Automation Conference (DAC)},\n   address = {San Diego, California},\n   pages = {705-711},\n   month = {June},\n   note = {Best Paper Nominee},\n   year = {1994}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1993\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1993\n \n \n (13)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Min-Max Linear Programming and the Timing Analysis of Digital Circuits.\n \n \n \n\n\n \n Burks, T. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In TAU93—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Malente, Germany, September 1993. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{burks1993minmax,\n   author = {Burks, Timothy M. and Sakallah, Karem A.},\n   title = {{Min-Max Linear Programming and the Timing Analysis of Digital Circuits}},\n   booktitle = {TAU93—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems},\n   address = {Malente, Germany},\n   month = {September},\n   year = {1993}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Comparison of Path Sensitization Criteria for Timing Analysis.\n \n \n \n\n\n \n Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In TAU93—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Malente, Germany, September 1993. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{marquessilva1993comparison,\n   author = {Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{A Comparison of Path Sensitization Criteria for Timing Analysis}},\n   booktitle = {TAU93—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems},\n   address = {Malente, Germany},\n   month = {September},\n   year = {1993}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Sensitization Networks for Accurate Timing Analysis.\n \n \n \n\n\n \n Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In TAU93—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Malente, Germany, September 1993. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{marquessilva1993sensitization,\n   author = {Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{Sensitization Networks for Accurate Timing Analysis}},\n   booktitle = {TAU93—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems},\n   address = {Malente, Germany},\n   month = {September},\n   year = {1993}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Concurrent Path Sensitization in Timing Analysis.\n \n \n \n\n\n \n Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In European Design Automation Conference (EuroDAC), pages 196-199, Hamburg, Germany, September 1993. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{marquessilva1993concurrent,\n   author = {Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{Concurrent Path Sensitization in Timing Analysis}},\n   booktitle = {European Design Automation Conference (EuroDAC)},\n   address = {Hamburg, Germany},\n   pages = {196-199},\n   month = {September},\n   year = {1993}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Delay Modeling for GaAs DCFL Circuits.\n \n \n \n\n\n \n Kayssi, A. I.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. IEEE GaAs IC Symposium, pages 67-70, San Jose, California, October 1993. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kayssi1993delay,\n   author = {Kayssi, Ayman I. and Sakallah, Karem A.},\n   title = {{Delay Modeling for GaAs DCFL Circuits}},\n   booktitle = {Proc. IEEE GaAs IC Symposium},\n   address = {San Jose, California},\n   pages = {67-70},\n   month = {October},\n   year = {1993}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An Analysis of Path Sensitization Criteria.\n \n \n \n\n\n \n Marques-Silva, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. IEEE International Conference on Computer Design (ICCD), pages 68-72, Boston, Massachusetts, October 1993. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{marquessilva1993analysis,\n   author = {Marques-Silva, {J\\~oao} and Sakallah, Karem A.},\n   title = {{An Analysis of Path Sensitization Criteria}},\n   booktitle = {Proc. IEEE International Conference on Computer Design (ICCD)},\n   address = {Boston, Massachusetts},\n   pages = {68-72},\n   month = {October},\n   year = {1993}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Ravel-XL: A Hardware Accelerator for Assigned-Delay Compiled-Code Logic Gate Simulation.\n \n \n \n\n\n \n Riepe, M. A.; Marques-Silva, J.; Sakallah, K. A.; and Brown, R. B.\n\n\n \n\n\n\n In Proc. IEEE International Conference on Computer Design (ICCD), pages 361-364, Boston, Massachusetts, October 1993. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{riepe1993ravel,\n   author = {Riepe, Michael A. and Marques-Silva, {J\\~oao} and Sakallah, Karem A. and Brown, Richard B.},\n   title = {{Ravel-XL: A Hardware Accelerator for Assigned-Delay Compiled-Code Logic Gate Simulation}},\n   booktitle = {Proc. IEEE International Conference on Computer Design (ICCD)},\n   address = {Boston, Massachusetts},\n   pages = {361-364},\n   month = {October},\n   year = {1993}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Min-Max Linear Programming and the Timing Analysis of Synchronous Circuits.\n \n \n \n\n\n \n Burks, T. M.; and Sakallah, K. A.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 152-155, Santa Clara, California, November 1993. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{burks1993aminmax,\n   author = {Burks, Timothy M. and Sakallah, Karem A.},\n   title = {{Min-Max Linear Programming and the Timing Analysis of Synchronous Circuits}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {Santa Clara, California},\n   pages = {152-155},\n   month = {November},\n   year = {1993}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The Impact of Signal Transition Time on Path Delay Computation.\n \n \n \n\n\n \n Kayssi, A. I.; Sakallah, K. A.; and Mudge, T. N.\n\n\n \n\n\n\n IEEE Transactions on Circuits and Systems II: Analog and Digital Signal Processing, 40(5): 302-309. May 1993.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{kayssi1993impact,\n   author = {Kayssi, Ayman I. and Sakallah, Karem A. and Mudge, Trevor N.},\n   title = {{The Impact of Signal Transition Time on Path Delay Computation}},\n   journal = {IEEE Transactions on Circuits and Systems II: Analog and Digital Signal Processing},\n   volume = {40},\n   number = {5},\n   pages = {302-309},\n   month = {May},\n   year = {1993}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A High Performance GaAs Microprocessor.\n \n \n \n\n\n \n Huff, T. R.; Upton, M.; Sherhart, P.; Barker, P.; McVay, R.; Stanley, T.; Brown, R.; Lomax, R.; Mudge, T.; and Sakallah, K.\n\n\n \n\n\n\n In Sarnoff Symposium, 1993 IEEE Princeton Section, pages 166–172, Princeton, New Jersey, March 1993. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{huff1993high,\n   author = {Huff, T. R. and Upton, M. and Sherhart, P. and Barker, P. and McVay, R. and Stanley, T. and Brown, R. and Lomax, R. and Mudge, T. and Sakallah, K.},\n   title = {{A High Performance GaAs Microprocessor}},\n   booktitle = {Sarnoff Symposium, 1993 IEEE Princeton Section},\n   address = {Princeton, New Jersey},\n   pages = {166--172},\n   month = {March},\n   year = {1993}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Delay-Accurate Compiled-Code Synchronous Gate-Level Verilog Simulation.\n \n \n \n\n\n \n Riepe, M. A.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. International Verilog HDL Conference, pages 121-127, Santa Clara, California, March 1993. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{riepe1993delay,\n   author = {Riepe, Michael A. and Sakallah, Karem A.},\n   title = {{Delay-Accurate Compiled-Code Synchronous Gate-Level Verilog Simulation}},\n   booktitle = {Proc. International Verilog HDL Conference},\n   address = {Santa Clara, California},\n   pages = {121-127},\n   month = {March},\n   year = {1993}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A 160,000 Transistor GaAs Microprocessor.\n \n \n \n\n\n \n Upton, M.; Huff, T.; Sherhart, P.; Barker, P.; Brown, R.; Lomax, R.; Mudge, T.; and Sakallah, K.\n\n\n \n\n\n\n In International Solid-State Circuits Conference (ISSCC), pages 92-93, San Francisco, California, February 1993. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{upton1993transistor,\n   author = {Upton, Michael and Huff, Thomas and Sherhart, Patrick and Barker, Phillip and Brown, Richard and Lomax, Ronald and Mudge, Trevor and Sakallah, Karem},\n   title = {{A 160,000 Transistor GaAs Microprocessor}},\n   booktitle = {International Solid-State Circuits Conference (ISSCC)},\n   address = {San Francisco, California},\n   pages = {92-93},\n   month = {February},\n   year = {1993}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Synchronization of Pipelines.\n \n \n \n\n\n \n Sakallah, K. A.; Mudge, T. N.; Burks, T. M.; and Davidson, E. S.\n\n\n \n\n\n\n IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 12(8): 1132-1146. August 1993.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{sakallah1993synchronization,\n   author = {Sakallah, Karem A. and Mudge, Trevor N. and Burks, Timothy M. and Davidson, Edward S.},\n   title = {{Synchronization of Pipelines}},\n   journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n   volume = {12},\n   number = {8},\n   pages = {1132-1146},\n   month = {August},\n   year = {1993}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1992\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1992\n \n \n (11)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Delay Macromodels for the Timing Analysis of GaAs DCFL.\n \n \n \n\n\n \n Kayssi, A. I.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. European Design Automation Conference (EuroDAC), pages 142-145, Hamburg, Germany, September 1992. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kayssi1992delay,\n   author = {Kayssi, Ayman I. and Sakallah, Karem A.},\n   title = {{Delay Macromodels for the Timing Analysis of GaAs DCFL}},\n   booktitle = {Proc. European Design Automation Conference (EuroDAC)},\n   address = {Hamburg, Germany},\n   pages = {142-145},\n   month = {September},\n   year = {1992}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n GaAs RISC Processors.\n \n \n \n\n\n \n Brown, R. B.; Barker, P.; Chandna, A.; Huff, T. R.; Kayssi, A. I.; Lomax, R. J.; Mudge, T. N.; Nagle, D.; Sakallah, K. A.; Sherhart, P. J.; Uhlig, R.; and Upton, M.\n\n\n \n\n\n\n In Proc. IEEE GaAs IC Symposium, pages 81-84, Miami Beach, Florida, October 1992. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{brown1992gaas,\n   author = {Brown, Richard B. and Barker, Phillip and Chandna, Ajay and Huff, Thomas R. and Kayssi, Ayman I. and Lomax, Ronald J. and Mudge, Trevor N. and Nagle, David and Sakallah, Karem A. and Sherhart, P. J. and Uhlig, Richard and Upton, Michael},\n   title = {{GaAs RISC Processors}},\n   booktitle = {Proc. IEEE GaAs IC Symposium},\n   address = {Miami Beach, Florida},\n   pages = {81-84},\n   month = {October},\n   year = {1992}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Identification of Critical Paths in Circuits with Level-Sensitive Latches.\n \n \n \n\n\n \n Burks, T. M.; Sakallah, K. A.; and Mudge, T. N.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 137-141, Santa Clara, California, November 1992. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{burks1992identification,\n   author = {Burks, Timothy M. and Sakallah, Karem A. and Mudge, Trevor N.},\n   title = {{Identification of Critical Paths in Circuits with Level-Sensitive Latches}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {Santa Clara, California},\n   pages = {137-141},\n   month = {November},\n   year = {1992}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Using Constraint Geometry to Determine Maximum Rate Pipeline Clocking.\n \n \n \n\n\n \n Chang, C.; Davidson, E. S.; and Sakallah, K. A.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 142-148, Santa Clara, California, November 1992. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{chang1992using,\n   author = {Chang, Chuan-Hua and Davidson, Edward S. and Sakallah, Karem A.},\n   title = {{Using Constraint Geometry to Determine Maximum Rate Pipeline Clocking}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {Santa Clara, California},\n   pages = {142-148},\n   month = {November},\n   year = {1992}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Ravel: Assigned-Delay Compiled-Code Logic Simulation.\n \n \n \n\n\n \n Shriver, E. J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 364-368, Santa Clara, California, November 1992. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{shriver1992ravel,\n   author = {Shriver, Emily J. and Sakallah, Karem A.},\n   title = {{Ravel: Assigned-Delay Compiled-Code Logic Simulation}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {Santa Clara, California},\n   pages = {364-368},\n   month = {November},\n   year = {1992}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Impact of MCMs on System Performance Optimization.\n \n \n \n\n\n \n Kayssi, A. I.; Sakallah, K. A.; Brown, R. B.; Lomax, R. J.; Mudge, T. N.; and Huff, T. R.\n\n\n \n\n\n\n In Proc. IEEE International Symposium on Circuits and Systems (ISCAS), pages 919-922, San Diego, California, May 1992. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kayssi1992impact,\n   author = {Kayssi, Ayman I. and Sakallah, Karem A. and Brown, Richard B. and Lomax, Ronald J. and Mudge, Trevor N. and Huff, Thomas R.},\n   title = {{Impact of MCMs on System Performance Optimization}},\n   booktitle = {Proc. IEEE International Symposium on Circuits and Systems (ISCAS)},\n   address = {San Diego, California},\n   pages = {919-922},\n   month = {May},\n   year = {1992}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Synthesis and Verification of a GaAs Microprocessor from a Verilog Hardware Description.\n \n \n \n\n\n \n Brown, R.; Chandna, A.; Hoy, T.; Huff, T.; Lomax, R.; Mudge, T.; Nagle, D.; Sakallah, K.; Uhlig, R.; Upton, M.; Olukotun, O.; and Johnson, D.\n\n\n \n\n\n\n In Proc. International Verilog HDL Conference, pages 85-92, Santa Clara, California, March 1992. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{brown1992synthesis,\n   author = {Brown, Richard and Chandna, Ajay and Hoy, Thomas and Huff, Thomas and Lomax, Ronald and Mudge, Trevor and Nagle, David and Sakallah, Karem and Uhlig, Richard and Upton, Michael and Olukotun, Oyekunle and Johnson, David},\n   title = {{Synthesis and Verification of a GaAs Microprocessor from a Verilog Hardware Description}},\n   booktitle = {Proc. International Verilog HDL Conference},\n   address = {Santa Clara, California},\n   pages = {85-92},\n   month = {March},\n   year = {1992}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Multiphase Retiming Using minTc.\n \n \n \n\n\n \n Burks, T. M.; Sakallah, K. A.; and Mudge, T. N.\n\n\n \n\n\n\n In TAU92—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Princeton University, March 1992. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{burks1992multiphase,\n   author = {Burks, Timothy M. and Sakallah, Karem A. and Mudge, Trevor N.},\n   title = {{Multiphase Retiming Using minTc}},\n   booktitle = {TAU92—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems},\n   address = {Princeton University},\n   month = {March},\n   year = {1992}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Delay Macromodels for Point-to-Point MCM Interconnections.\n \n \n \n\n\n \n Kayssi, A. I.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. IEEE Multi-Chip Module Conference (MCMC), pages 79-82, Santa Cruz, California, March 1992. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kayssi1992adelay,\n   author = {Kayssi, Ayman I. and Sakallah, Karem A.},\n   title = {{Delay Macromodels for Point-to-Point MCM Interconnections}},\n   booktitle = {Proc. IEEE Multi-Chip Module Conference (MCMC)},\n   address = {Santa Cruz, California},\n   pages = {79-82},\n   month = {March},\n   year = {1992}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Analysis and Design of Latch-Controlled Synchronous Digital Circuits.\n \n \n \n\n\n \n Sakallah, K. A.; Mudge, T. N.; and Olukotun, O. A.\n\n\n \n\n\n\n IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 11(3): 322-333. March 1992.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{sakallah1992analysis,\n   author = {Sakallah, Karem A. and Mudge, Trevor N. and Olukotun, Oyekunle A.},\n   title = {{Analysis and Design of Latch-Controlled Synchronous Digital Circuits}},\n   journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n   volume = {11},\n   number = {3},\n   pages = {322-333},\n   month = {March},\n   year = {1992}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Analytical Transient Response of CMOS Inverters.\n \n \n \n\n\n \n Kayssi, A. I.; Sakallah, K. A.; and Burks, T. M.\n\n\n \n\n\n\n IEEE Transactions on Circuits and Systems, 39(1): 42-45. January 1992.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{kayssi1992analytical,\n   author = {Kayssi, Ayman I. and Sakallah, Karem A. and Burks, Timothy M.},\n   title = {{Analytical Transient Response of CMOS Inverters}},\n   journal = {IEEE Transactions on Circuits and Systems},\n   volume = {39},\n   number = {1},\n   pages = {42-45},\n   month = {January},\n   year = {1992}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1991\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1991\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Optimal Clocking of Circular Pipelines.\n \n \n \n\n\n \n Sakallah, K. A.; Mudge, T. N.; Burks, T. M.; and Davidson, E. S.\n\n\n \n\n\n\n In Proc. IEEE International Conference on Computer Design (ICCD), pages 642-646, Boston, Massachusetts, October 1991. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah1991optimal,\n   author = {Sakallah, Karem A. and Mudge, Trevor N. and Burks, Timothy M. and Davidson, Edward S.},\n   title = {{Optimal Clocking of Circular Pipelines}},\n   booktitle = {Proc. IEEE International Conference on Computer Design (ICCD)},\n   address = {Boston, Massachusetts},\n   pages = {642-646},\n   month = {October},\n   year = {1991}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n FPD—An Environment for Exact Timing Analysis.\n \n \n \n\n\n \n Marques-Silva, J.; Sakallah, K. A.; and Vidigal, L. M.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 212-215, Santa Clara, California, November 1991. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{marquessilva1991fpd,\n   author = {Marques-Silva, {J\\~oao} and Sakallah, Karem A. and Vidigal, Luis M.},\n   title = {{FPD—An Environment for Exact Timing Analysis}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {Santa Clara, California},\n   pages = {212-215},\n   month = {November},\n   year = {1991}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Performance Improvement through Optimal Clocking and Retiming.\n \n \n \n\n\n \n Burks, T. M.; Sakallah, K. A.; Bartlett, K. A.; and Borriello, G.\n\n\n \n\n\n\n In Proc. of the International Workshop on Logic Synthesis (IWLS), Research Triangle Park, North Carolina, May 1991. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{burks1991performance,\n   author = {Burks, Timothy M. and Sakallah, Karem A. and Bartlett, Karen A. and Borriello, Gaetano},\n   title = {{Performance Improvement through Optimal Clocking and Retiming}},\n   booktitle = {Proc. of the International Workshop on Logic Synthesis (IWLS)},\n   address = {Research Triangle Park, North Carolina},\n   month = {May},\n   year = {1991}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Multilevel Optimization in the Design of a High-Performance GaAs Microcomputer.\n \n \n \n\n\n \n Olukotun, O. A.; Brown, R. B.; Lomax, R. J.; Mudge, T. N.; and Sakallah, K. A.\n\n\n \n\n\n\n IEEE Journal on Solid State Circuits, 26(5): 763-767. May 1991.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{olukotun1991multilevel,\n   author = {Olukotun, O. A. and Brown, R. B. and Lomax, R. J. and Mudge, T. N. and Sakallah, K. A.},\n   title = {{Multilevel Optimization in the Design of a High-Performance GaAs Microcomputer}},\n   journal = {IEEE Journal on Solid State Circuits},\n   volume = {26},\n   number = {5},\n   pages = {763-767},\n   month = {May},\n   year = {1991}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Impact of MCM's on System Performance.\n \n \n \n\n\n \n Kayssi, A. I.; Sakallah, K. A.; Brown, R. B.; Lomax, R. J.; Mudge, T. N.; and Huff, T. R.\n\n\n \n\n\n\n In Proc. MCM Workshop, pages 58-65, University of California, Santa Cruz, March 1991. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{kayssi1991impact,\n   author = {Kayssi, Ayman I. and Sakallah, Karem A. and Brown, Richard B. and Lomax, Ronald J. and Mudge, Trevor N. and Huff, Thomas R.},\n   title = {{Impact of MCM's on System Performance}},\n   booktitle = {Proc. MCM Workshop},\n   address = {University of California, Santa Cruz},\n   pages = {58-65},\n   month = {March},\n   year = {1991}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The Design of a Microsupercomputer.\n \n \n \n\n\n \n Mudge, T. N.; Birmingham, W. P.; Brown, R. B.; Dykstra, J. A.; Kayssi, A. I.; Lomax, R. J.; Olukotun, O. A.; Sakallah, K. A.; and Milano, R. A.\n\n\n \n\n\n\n IEEE Computer, 24(1): 57-64. January 1991.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{mudge1991design,\n   author = {Mudge, Trevor N. and Birmingham, William P. and Brown, Richard B. and Dykstra, Jeffery A. and Kayssi, Ayman I. and Lomax, Ronald J. and Olukotun, Oyekunle A. and Sakallah, Karem A. and Milano, Raymond A.},\n   title = {{The Design of a Microsupercomputer}},\n   journal = {IEEE Computer},\n   volume = {24},\n   number = {1},\n   pages = {57-64},\n   month = {January},\n   year = {1991}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The Design of a GaAs Micro-Supercomputer.\n \n \n \n\n\n \n Mudge, T. N.; Brown, R.; Birmingham, W. P.; Dykstra, J.; Kayssi, A.; Lomax, R.; Olukotun, O. A.; Sakallah, K. A.; and Milano, R.\n\n\n \n\n\n\n In Proc. Hawaii International Conference on Systems Sciences (HICSS), pages 421-432, Honolulu, Hawaii, January 1991. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{mudge1991adesign,\n   author = {Mudge, T. N. and Brown, R. and Birmingham, W. P. and Dykstra, J. and Kayssi, A. and Lomax, R. and Olukotun, O. A. and Sakallah, K. A. and Milano, R.},\n   title = {{The Design of a GaAs Micro-Supercomputer}},\n   booktitle = {Proc. Hawaii International Conference on Systems Sciences (HICSS)},\n   address = {Honolulu, Hawaii},\n   pages = {421-432},\n   month = {January},\n   year = {1991}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1990\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1990\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n checkTc and minTc: Timing Verification and Optimal Clocking of Synchronous Digital Circuits.\n \n \n \n\n\n \n Sakallah, K. A.; Mudge, T. N.; and Olukotun, O. A.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 552-555, Santa Clara, California, November 1990. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah1990checktc,\n   author = {Sakallah, Karem A. and Mudge, Trevor N. and Olukotun, Oyekunle A.},\n   title = {{checkTc and minTc: Timing Verification and Optimal Clocking of Synchronous Digital Circuits}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {Santa Clara, California},\n   pages = {552-555},\n   month = {November},\n   year = {1990}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Analysis and Design of Latch-Controlled Synchronous Digital Circuits.\n \n \n \n\n\n \n Sakallah, K. A.; Mudge, T. N.; and Olukotun, O. A.\n\n\n \n\n\n\n In Proc. IEEE/ACM Design Automation Conference (DAC), pages 111-117, Orlando, Florida, June 1990. \n Best Paper Nominee\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah1990analysis,\n   author = {Sakallah, Karem A. and Mudge, Trevor N. and Olukotun, Oyekunle A.},\n   title = {{Analysis and Design of Latch-Controlled Synchronous Digital Circuits}},\n   booktitle = {Proc. IEEE/ACM Design Automation Conference (DAC)},\n   address = {Orlando, Florida},\n   pages = {111-117},\n   month = {June},\n   note = {Best Paper Nominee},\n   year = {1990}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A First-Order Charge-Conserving MOS Capacitance Model.\n \n \n \n\n\n \n Sakallah, K. A.; Yen, Y.; and Greenberg, S. S.\n\n\n \n\n\n\n IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 9(1): 99-108. January 1990.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{sakallah1990first,\n   author = {Sakallah, Karem A. and Yen, Yao-Tsung and Greenberg, Steve S.},\n   title = {{A First-Order Charge-Conserving MOS Capacitance Model}},\n   journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n   volume = {9},\n   number = {1},\n   pages = {99-108},\n   month = {January},\n   year = {1990}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Optimal Clocking of Synchronous Systems.\n \n \n \n\n\n \n Sakallah, K. A.; Mudge, T. N.; and Olukotun, O. A.\n\n\n \n\n\n\n In TAU90—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, University of British Columbia, Vancouver, August 1990. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah1990optimal,\n   author = {Sakallah, K. A. and Mudge, T. N. and Olukotun, O. A.},\n   title = {{Optimal Clocking of Synchronous Systems}},\n   booktitle = {TAU90—ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems},\n   address = {University of British Columbia, Vancouver},\n   month = {August},\n   year = {1990}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Clock Qualification Algorithm for Timing Analysis of Custom CMOS VLSI Circuits with Overlapped Clocking Disciplines and On-Section Clock Derivation.\n \n \n \n\n\n \n Menon, S. C.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. International Conference on Systems Integration, pages 550-558, Boston, Massachusetts, April 1990. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{menon1990clock,\n   author = {Menon, Somanathan C. and Sakallah, Karem A.},\n   title = {{Clock Qualification Algorithm for Timing Analysis of Custom CMOS VLSI Circuits with Overlapped Clocking Disciplines and On-Section Clock Derivation}},\n   booktitle = {Proc. International Conference on Systems Integration},\n   address = {Boston, Massachusetts},\n   pages = {550-558},\n   month = {April},\n   year = {1990}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1988\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1988\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Mixed Analog-Digital Simulation.\n \n \n \n\n\n \n Greenberg, S. S.; Grodstein, J.; and Sakallah, K. A.\n\n\n \n\n\n\n In Electro/88 Professional Program Session Record 43/2, pages 1-8, Boston, Massachusetts, May 1988. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{greenberg1988mixed,\n   author = {Greenberg, Steve S. and Grodstein, Joel and Sakallah, Karem A.},\n   title = {{Mixed Analog-Digital Simulation}},\n   booktitle = {Electro/88 Professional Program Session Record 43/2},\n   address = {Boston,  Massachusetts},\n   pages = {1-8},\n   month = {May},\n   year = {1988}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1987\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1987\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n The Meyer Model Revisited: Explaining and Correcting the Charge Non-Conservation Problem.\n \n \n \n\n\n \n Sakallah, K. A.; Yen, Y.; and Greenberg, S. S.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 204-207, Santa Clara, California, November 1987. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah1987meyer,\n   author = {Sakallah, Karem A. and Yen, Yao-Tsung and Greenberg, Steve S.},\n   title = {{The Meyer Model Revisited: Explaining and Correcting the Charge Non-Conservation Problem}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {Santa Clara, California},\n   pages = {204-207},\n   month = {November},\n   year = {1987}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n SAM0: An Automatic MOS Circuit Partitioner.\n \n \n \n\n\n \n Yen, Y.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. IEEE Custom Integrated Circuits Conference (CICC), pages 129-132, Portland, Oregon, May 1987. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{yen1987sam0,\n   author = {Yen, Yao-Tsung and Sakallah, Karem A.},\n   title = {{SAM0: An Automatic MOS Circuit Partitioner}},\n   booktitle = {Proc. IEEE Custom Integrated Circuits Conference (CICC)},\n   address = {Portland, Oregon},\n   pages = {129-132},\n   month = {May},\n   year = {1987}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1985\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1985\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n SAMSON2: An Event Driven VLSI Circuit Simulator.\n \n \n \n \n\n\n \n Sakallah, K. A.; and Director, S. W.\n\n\n \n\n\n\n IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, CAD-4(4): 668-684. October 1985.\n \n\n\n\n
\n\n\n\n \n \n \"SAMSON2:Paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{sakallah1985samson2,\n   author = {Sakallah, Karem A. and Director, Stephen W.},\n   title = {{SAMSON2: An Event Driven VLSI Circuit Simulator}},\n   journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n   volume = {CAD-4},\n   number = {4},\n   pages = {668-684},\n   month = {October},\n   year = {1985},\n   doi = {https://doi.org/10.1109/TCAD.1985.1270167},\n   url = {https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=1270167}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Polynomial Terminal Equivalent Circuits as Dormant Models in Event Driven Circuit Simulation.\n \n \n \n\n\n \n Sakallah, K. A.\n\n\n \n\n\n\n In Digest of IEEE International Conference on Computer-Aided Design (ICCAD), pages 179-181, Santa Clara, California, November 1985. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah1985polynomial,\n   author = {Sakallah, Karem A.},\n   title = {{Polynomial Terminal Equivalent Circuits as Dormant Models in Event Driven Circuit Simulation}},\n   booktitle = {Digest of IEEE International Conference on Computer-Aided Design (ICCAD)},\n   address = {Santa Clara, California},\n   pages = {179-181},\n   month = {November},\n   year = {1985}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n PRIMO: A VLSI Circuit Partitioner for Simulation Applications.\n \n \n \n\n\n \n Vasquez, A. V.; Director, S. W.; and Sakallah, K. A.\n\n\n \n\n\n\n In Proc. IEEE International Symposium on Circuits and Systems (ISCAS), pages 1075-1078, Kyoto, Japan, June 1985. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{vasquez1985primo,\n   author = {Vasquez, A. Vincent and Director, Stephen W. and Sakallah, Karem A.},\n   title = {{PRIMO: A VLSI Circuit Partitioner for Simulation Applications}},\n   booktitle = {Proc. IEEE International Symposium on Circuits and Systems (ISCAS)},\n   address = {Kyoto, Japan},\n   pages = {1075-1078},\n   month = {June},\n   year = {1985}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n SAMSON: A Mixed Circuit- Logic-Level Simulator.\n \n \n \n\n\n \n Sakallah, K. A.; and Director, S. W.\n\n\n \n\n\n\n In Sangiovanni-Vincentelli, A., editor(s), Computer-Aided Design of VLSI Circuits and Systems, volume 1, of Advances in Computer-Aided Engineering Design, pages 149-223. JAI Press Inc., 36 Sherwood Place, Greenwich, Connecticut 06830, 1985.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{sakallah1985samson,\n   author = {Sakallah, Karem A. and Director, Stephen W.},\n   title = {{SAMSON: A Mixed Circuit- Logic-Level Simulator}},\n   booktitle = {Computer-Aided Design of VLSI Circuits and Systems},\n   editor = {Sangiovanni-Vincentelli, Alberto},\n   series = {Advances in Computer-Aided Engineering Design},\n   publisher = {JAI Press Inc.},\n   address = {36 Sherwood Place, Greenwich, Connecticut 06830},\n   volume = {1},\n   pages = {149-223},\n   year = {1985}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1984\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1984\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n SAMSON: An Event Driven VLSI Circuit Simulator.\n \n \n \n\n\n \n Sakallah, K. A.; and Director, S. W.\n\n\n \n\n\n\n In Proc. IEEE Custom Integrated Circuits Conference (CICC), pages 226-231, Rochester, New York, May 1984. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah1984samson,\n   author = {Sakallah, Karem A. and Director, Stephen W.},\n   title = {{SAMSON: An Event Driven VLSI Circuit Simulator}},\n   booktitle = {Proc. IEEE Custom Integrated Circuits Conference (CICC)},\n   address = {Rochester, New York},\n   pages = {226-231},\n   month = {May},\n   year = {1984}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1982\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1982\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n An Event Driven Approach for Mixed Gate and Circuit Level Simulation.\n \n \n \n\n\n \n Sakallah, K. A.; and Director, S. W.\n\n\n \n\n\n\n In Proc. IEEE International Symposium on Circuits and Systems (ISCAS), pages 1194-1197, Rome, Italy, May 1982. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah1982event,\n   author = {Sakallah, Karem A. and Director, Stephen W.},\n   title = {{An Event Driven Approach for Mixed Gate and Circuit Level Simulation}},\n   booktitle = {Proc. IEEE International Symposium on Circuits and Systems (ISCAS)},\n   address = {Rome, Italy},\n   pages = {1194-1197},\n   month = {May},\n   year = {1982}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1981\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1981\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n An Algorithm for Activity-Directed Mixed-Level Simulation of VLSI Circuits.\n \n \n \n\n\n \n Sakallah, K. A.; and Director, S. W.\n\n\n \n\n\n\n In Tenth Computer-Aided Network Design (CANDE) Workshop, Gravenhurst, Ontario, Canada, September 1981. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah1981algorithm,\n   author = {Sakallah, Karem A. and Director, Stephen W.},\n   title = {{An Algorithm for Activity-Directed Mixed-Level Simulation of VLSI Circuits}},\n   booktitle = {Tenth Computer-Aided Network Design (CANDE) Workshop},\n   address = {Gravenhurst, Ontario, Canada},\n   month = {September},\n   year = {1981}\n\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Mixed Simulation of Electronic Integrated Circuits.\n \n \n \n\n\n \n Sakallah, K. A.\n\n\n \n\n\n\n Ph.D. Thesis, Carnegie Mellon University, 1981.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@phdthesis{sakallah1981mixed,\n   author = {Sakallah, Karem A.},\n   title = {{Mixed Simulation of Electronic Integrated Circuits}},\n   school = {Carnegie Mellon University},\n   type = {Ph.D. Thesis},\n   year = {1981}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1980\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1980\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n An Activity-Directed Circuit Simulation Algorithm.\n \n \n \n\n\n \n Sakallah, K. A.; and Director, S. W.\n\n\n \n\n\n\n In Proc. IEEE International Conference on Circuits and Computers (ICCC), pages 1032-1035, Rye, New York, October 1980. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{sakallah1980activity,\n   author = {Sakallah, Karem A. and Director, Stephen W.},\n   title = {{An Activity-Directed Circuit Simulation Algorithm}},\n   booktitle = {Proc. IEEE International Conference on Circuits and Computers (ICCC)},\n   address = {Rye, New York},\n   pages = {1032-1035},\n   month = {October},\n   year = {1980}\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n% 1977\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1977\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n The Simulation of Class I Traffic in an Integrated Communications Network.\n \n \n \n\n\n \n Sakallah, K. A.\n\n\n \n\n\n\n Master's Thesis, Carnegie Mellon University, 1977.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@mastersthesis{sakallah1977simulation,\n   author = {Sakallah, Karem A.},\n   title = {{The Simulation of Class I Traffic in an Integrated Communications Network}},\n   school = {Carnegie Mellon University},\n   type = {Master's Thesis},\n   year = {1977}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);