The SCEAS System
Navigation Menu
Introduction
Collection Based
Clustering
Ranking
Paper Based
Journals
Conferences
DB Status
Statistics
Search

Search the dblp DataBase

Title:
Author:
Mark Aagaard: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

Publications of Author

  1. Mark Aagaard, Miriam Leeser
    Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification. [Citation Graph (0, 0)][DBLP]
    CAV, 1992, pp:69-81 [Conf]
  2. Mark Aagaard
    A Hazards-Based Correctness Statement for Pipelined Circuits. [Citation Graph (0, 0)][DBLP]
    CHARME, 2003, pp:66-80 [Conf]
  3. Mark Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones
    A Framework for Microprocessor Correctness Statements. [Citation Graph (0, 0)][DBLP]
    CHARME, 2001, pp:433-448 [Conf]
  4. Mark Aagaard, Thomas F. Melham, John W. O'Leary
    Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. [Citation Graph (0, 0)][DBLP]
    CHARME, 1999, pp:202-218 [Conf]
  5. Robert Beers, Rajnish Ghughal, Mark Aagaard
    Applications of Hierarchical Verification in Model Checking. [Citation Graph (0, 0)][DBLP]
    CHARME, 2001, pp:40-57 [Conf]
  6. John W. O'Leary, Mark H. Linderman, Miriam Leeser, Mark Aagaard
    HML: A Hardware Description Language Based on Standard ML. [Citation Graph (0, 0)][DBLP]
    CHDL, 1993, pp:327-334 [Conf]
  7. Mark Aagaard, Robert B. Jones, Roope Kaivola, Katherine R. Kohatsu, Carl-Johan H. Seger
    Formal verification of iterative algorithms in microprocessors. [Citation Graph (0, 0)][DBLP]
    DAC, 2000, pp:201-206 [Conf]
  8. Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger
    Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment. [Citation Graph (0, 0)][DBLP]
    DAC, 1998, pp:538-541 [Conf]
  9. Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger
    Parametric Representations of Boolean Constraints. [Citation Graph (0, 0)][DBLP]
    DAC, 1999, pp:402-407 [Conf]
  10. Hazem I. Shehata, Mark Aagaard
    A general decomposition strategy for verifying register renaming. [Citation Graph (0, 0)][DBLP]
    DAC, 2004, pp:234-237 [Conf]
  11. Mark Aagaard, Vlad C. Ciubotariu, Jason T. Higgins, Farzad Khalvati
    Combining Equivalence Verification and Completion Functions. [Citation Graph (0, 0)][DBLP]
    FMCAD, 2004, pp:98-112 [Conf]
  12. Mark Aagaard, Nancy A. Day, Robert B. Jones
    Synchronization-at-Retirement for Pipeline Verification. [Citation Graph (0, 0)][DBLP]
    FMCAD, 2004, pp:113-127 [Conf]
  13. Mark Aagaard, Nancy A. Day, Meng Lou
    Relating Multi-step and Single-Step Microprocessor Correctness Statements. [Citation Graph (0, 0)][DBLP]
    FMCAD, 2002, pp:123-141 [Conf]
  14. Mark Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, Carl-Johan H. Seger
    A Methodology for Large-Scale Hardware Verification. [Citation Graph (0, 0)][DBLP]
    FMCAD, 2000, pp:263-282 [Conf]
  15. Robert Beers, Rajnish Ghughal, Mark Aagaard
    Applications of Hierarchical Verification in Model Checking. [Citation Graph (0, 0)][DBLP]
    FMCAD, 2000, pp:- [Conf]
  16. Nancy A. Day, Mark Aagaard, Byron Cook
    Combining Stream-Based and State-Based Verification Techniques. [Citation Graph (0, 0)][DBLP]
    FMCAD, 2000, pp:126-142 [Conf]
  17. Mark Aagaard, Carl-Johan H. Seger
    The formal verification of a pipelined double-precision IEEE floating-point multiplier. [Citation Graph (0, 0)][DBLP]
    ICCAD, 1995, pp:7-10 [Conf]
  18. Mark Aagaard, Miriam Leeser
    A Formally Verified System for Logic Synthesis. [Citation Graph (0, 0)][DBLP]
    ICCD, 1991, pp:346-350 [Conf]
  19. Mark Aagaard, Miriam Leeser
    A Framework for Specifying and Designing Pipelines. [Citation Graph (0, 0)][DBLP]
    ICCD, 1993, pp:548-551 [Conf]
  20. Mark Aagaard, Miriam Leeser
    Reasoning About Pipelines with Structural Hazards. [Citation Graph (0, 0)][DBLP]
    TPCD, 1994, pp:13-32 [Conf]
  21. John W. O'Leary, Miriam Leeser, Jason Hickey, Mark Aagaard
    Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization. [Citation Graph (0, 0)][DBLP]
    TPCD, 1994, pp:52-71 [Conf]
  22. Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger
    Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 1999, pp:323-340 [Conf]
  23. Mark Aagaard, Miriam Leeser
    A Methodology for Reusable Hardware Proofs. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 1992, pp:177-196 [Conf]
  24. Mark Aagaard, Miriam Leeser, Phillip J. Windley
    Toward a Super Duper Hardware Tactic. [Citation Graph (0, 0)][DBLP]
    HUG, 1993, pp:399-412 [Conf]
  25. Roope Kaivola, Mark Aagaard
    Divider Circuit Verification with Model Checking and Theorem Proving. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:338-355 [Conf]
  26. Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, Mark Aagaard, Thomas F. Melham
    Practical Formal Verification in Microprocessor Design. [Citation Graph (0, 0)][DBLP]
    IEEE Design & Test of Computers, 2001, v:18, n:4, pp:16-25 [Journal]
  27. Mark Aagaard, Miriam Leeser
    A Methodology for Efficient Hardware Verification. [Citation Graph (0, 0)][DBLP]
    Formal Methods in System Design, 1994, v:5, n:1/2, pp:95-117 [Journal]
  28. Mark Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones
    A framework for superscalar microprocessor correctness statements. [Citation Graph (0, 0)][DBLP]
    STTT, 2003, v:4, n:3, pp:298-312 [Journal]
  29. Mark Aagaard, Miriam Leeser
    PBS: proven Boolean simplification. [Citation Graph (0, 0)][DBLP]
    IEEE Trans. on CAD of Integrated Circuits and Systems, 1994, v:13, n:4, pp:459-470 [Journal]
  30. Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Thomas F. Melham, Mark Aagaard, Clark Barrett, Don Syme
    An industrially effective environment for formal hardware verification. [Citation Graph (0, 0)][DBLP]
    IEEE Trans. on CAD of Integrated Circuits and Systems, 2005, v:24, n:9, pp:1381-1405 [Journal]
  31. Jason T. Higgins, Mark Aagaard
    Simplifying the design and automating the verification of pipelines with structural hazards. [Citation Graph (0, 0)][DBLP]
    ACM Trans. Design Autom. Electr. Syst., 2005, v:10, n:4, pp:651-672 [Journal]
  32. Mark Aagaard, Miriam Leeser
    Verifying a Logic-Synthesis Algorithm and Implementation: A Case Study in Software Verification. [Citation Graph (0, 0)][DBLP]
    IEEE Trans. Software Eng., 1995, v:21, n:10, pp:822-833 [Journal]
  33. Eunsuk Kang, Mark Aagaard
    Improving the Usability of HOL Through Controlled Automation Tactics. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2007, pp:157-172 [Conf]

Search in 0.066secs, Finished in 0.068secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
Introduction Collection Based Clustering Ranking Paper Based Journals Conferences DB Status Statistics Search
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002