• Top
    • Documentation
      • Xdoc
      • ACL2-doc
      • Recursion-and-induction
      • Loop$-primer
      • Operational-semantics
        • Operational-semantics-3__annotated-bibliography
          • Bib::bhmy89
          • Bib::liu06
          • Bib::bm96
          • Bib::plotkin04b
          • Bib::bgm90
          • Bib::hkms17
          • Bib::bkm96
          • Bib::moore15
          • Bib::bh99
          • Bib::wilding93
          • Bib::plotkin04a
          • Bib::moore03b
          • Bib::mp02
          • Bib::moore19
          • Bib::manolios00
          • Bib::flatau92
          • Bib::hb92
          • Bib::bm05
          • Bib::goel16
          • Bib::bm73
          • Bib::ghk17
          • Bib::wilding92
          • Bib::moore17
          • Bib::moore96
          • Bib::ghkg14
          • Bib::yu92
          • Bib::hunt85
          • Bib::boh03
          • Bib::mmrv06
          • Bib::bm80
          • Bib::bh97
          • Bib::moore99b
          • Bib::moore14
          • Bib::rm04
          • Bib::by96
          • Bib::sawada00
          • Bib::mccarthy62
          • Bib::bm79
          • Bib::moore99a
          • Bib::sh98
          • Bib::rhmm07
          • Bib::kmm00a
          • Bib::ghk13
          • Bib::moore03a
          • Bib::hk12
          • Bib::mp67
          • Bib::young88
          • Bib::bm97
          • Bib::moore73
          • Bib::kmm00b
            • Bib::bevier87
          • Operational-semantics-1__simple-example
          • Operational-semantics-2__other-examples
          • Operational-semantics-5__history-etc
          • Operational-semantics-4__how-to-find-things
        • Pointers
        • Doc
        • Documentation-copyright
        • Course-materials
        • Publications
        • Args
        • ACL2-doc-summary
        • Finding-documentation
        • Broken-link
        • Doc-terminal-test-2
        • Doc-terminal-test-1
      • Books
      • Boolean-reasoning
      • Projects
      • Debugging
      • Std
      • Community
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Operational-semantics-3__annotated-bibliography

    Bib::kmm00b

    M. Kaufmann, P. Manolios, J S. Moore, Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000.



    Relevance: tutorial examples of ACL2 applications



    ———

    This book is a companion to bib::kmm00a. It contains fourteen articles by ACL2 experts, explaining how they formalized and solved fourteen different problems. It also includes exercises.