		Search-engine friendly clone of the ACL2 documentation.

Operational-semantics

Operational-semantics-3__annotated-bibliography

Annotated bibliography for operational-semantics

This topic provides proper bibliographic citations to the work mentioned in the ACL2 documentation topic operational-semantics and its subtopics. Each citation (e.g., bib::bhmy89) is a link, at which you may find additional information about the publication and its relation to operational semantics. When Nqthm or ACL2 files are mentioned you will have to dereference those names following the instructions in operational-semantics-4__how-to-find-things.

Quick Index to Related Topics

operational-semantics
operational-semantics-1__simple-example
operational-semantics-2__other-examples
operational-semantics-3__annotated-bibliography — current topic
operational-semantics-4__how-to-find-things
operational-semantics-5__history-etc

Subtopics

Bib::bhmy89: W.R. Bevier, W.A. Hunt, Jr., J S. Moore, and W.D. Young, Special Issue on System Verification, Journal of Automated Reasoning, 5(4), pp. 409-530, 1989.

Relevance: Computational Logic Inc. (CLI) Verified Stack — a seminal achievement in formal methods and operational semantics
Bib::liu06: H. Liu, Formal Specification and Verification of a JVM and its Bytecode Verifier, University of Texas at Austin, Ph.D. dissertation, 2006

Relevance: most complete ACL2 model of the JVM
Bib::bm96: R. S. Boyer and J S. Moore, “Mechanized Formal Reasoning about Programs and Computing Machines”, in R. Veroff, editor, Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1966.

Relevance: the basic Nqthm/ACL2 style of operational semantics as a book chapter
Bib::plotkin04b: G. D. Plotkin, “ The origins of structural operational semantics”, The Journal of Logic and Algebraic Programming, 60 and 61, pp. 3-15, July and December 2004.

Relevance: an interesting historical account of the most popular (non-ACL2) approach to operational semantics
Bib::bgm90: R. S. Boyer, M. W. Green, and J S. Moore, “The Use of a Formal Simulator to Verify a Simple Real Time Control Program”, in W.H.J. Feijen, A.J.M. van Gasteren, D. Gries, and J. Misra, editors, Beauty is Our Business: A Birthday Salute to Edsger W. Dijkstra, Springer-Verlag Texts and Monographs in Computer Science, pp. 54-66, 1990.

Relevance: operational semantics modeling a hybrid physical/digital system
Bib::hkms17: W. A. Hunt, Jr., M. Kaufmann, J S. Moore, and A. Slobodova, “Industrial hardware and software verification with ACL2” in P. Gardner, P. O'Hearn, M. Gordon, G. Morrisett and F. B. Schneider, editors), Verified Trustworthy Software Systems, Philosophical Transactions A, Royal Society Publishing, 374, DOI 10.1098/rsta.2015.0399, September, 2017.

Relevance: how ACL2 is used in industry, and why
Bib::bkm96: B. Brock, M. Kaufmann, and J S. Moore, “ACL2 Theorems about Commercial Microprocessors”, in M. Srivas and A. Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD'96), Springer-Verlag, LNCS 1166, pp. 275-293, doi 10.1007/BFb0031816, 1996.

Relevance: early (mid-1990s) applications of ACL2 in industry (Motorola CAP DSP via operational semantics and the AMD K5 FDIV via a shallow embedding)
Bib::moore15: J S. Moore, “ Stateman: Using Metafunctions to Manage Large Terms Representing Machine States,” in M. Kaufmann and D. Rager, editors, Proceedings of the 13th International Workshop on the ACL2 Theorem Prover, EPTCS, 192, pp. 93-109, 2015.

Relevance: some ACL2 tools for managing the terms representing states of operational models
Bib::bh99: B. Brock and W. A. Hunt, Jr., “Formal Analysis of the Motorola CAP DSP”, in M. Hinchey and J. Bowen, editors, Industrial-Strength Formal Methods, Springer-Verlag, pp. 81-115, 1999.

Relevance: first industrial application of operational semantics with ACL2 and the first complete formal specification of a commercially designed microprocessor
Bib::wilding93: M. M. Wilding, “A Mechanically Verified Application for a Mechanically Verified Environment, in C. Courcoubetis, editor, Proceedings of Computer-Aided Verification -- CAV '93, Springer-Verlag, LNCS 697, Heidelberg, pp. 268-279, DOI:10.1007/3-540-56922-7_22, 1993.

Relevance: functional correctness and resource utilization of a Nim-playing program on the CLI Verified Stack
Bib::plotkin04a: G. D. Plotkin, “ A Structural Approach to Operational Semantics”, Computer Science Department, Aarhus University, Denmark, DAIMI FN-19, 1981 (reprised in a 2004 submission to the The Journal of Logic and Algebraic Programming).

Relevance: Plotkin's introduction of the term “structural operational semantics”
Bib::moore03b: J S. Moore, “ Inductive Assertions and Operational Semantics”, in D. Geist, editor, CHARME 2003,, Springer Verlag, LNCS 2860, pp. 289-303, 2003.

Relevance:The URL above points to a longer version of the paper presented at CHARME. Using a subset of M5 the paper shows how partial symbolic evaluation of a program can be used to generate and prove verification conditions produced from inductive assertions
Bib::mp02: J S. Moore and G. Porter, “The Apprentice Challenge”, ACM TOPLAS, 24(3), pp. 1-24, May, 2002.

Relevance: M5 and mutual-exclusion via monitors: an unbounded number of JVM threads competing for access to a shared resource
Bib::moore19: J S. Moore, “Milestones from The Pure Lisp Theorem Prover to ACL2”, Formal Aspects of Computing, Springer, DOI https://doi.org/10.1007/s00165-019-00490-3, 2019.

Relevance: how the Edinburgh Pure Lisp Theorem Prover (PLTP) evolved into ACL2
Bib::manolios00: P. Manolios, “Correctness of Pipelined Machines”, in W. A. Hunt, Jr and S. D. Johnson, editors, Formal Methods in Computer-Aided Design (FMCAD 2000), Springer-Verlag LNCS 1954, Heidelberg, pp. 161-178, 2000.

Relevance: an alternative approach to verifying operational models of a pipelined machine
Bib::flatau92: A. D. Flatau A verified implementation of an applicative language with dynamic storage allocation (ftp://ftp.cs.utexas.edu/pub/boyer/diss/flatau.pdf), University of Texas at Austin, Ph.D. dissertation, 1992 (minus some appendices).

Relevance: a second verified compiler hosted on the CLI Verified Stack
Bib::hb92: W. A. Hunt, Jr. and B. Brock, “A Formal HDL and its use in the FM9001 Verification”, Proceedings of the Royal Society, North Holland, April, 1992.

Relevance: a formalized hardware description language and the verification of a fabricated microprocessor described with it; this describes three foundational achievements in formal methods
Bib::bm05: B. Brock and J S. Moore, “A Mechanically Checked Proof of a Comparator Sort Algorithm”, in M. Broy, J. Gruenbauer, D. Harel, and C. A. R. Hoare, editors, Engineering Theories of Software Intensive Systems, Springer NATO Science Series II, 195, pp. 141-175, 2005.

Relevance: an example of proving that the state transformation effected by running a CAP model on commercial microcode implements the high level specification
Bib::goel16: S. Goel, Formal Verification of Application and System Programs Based on a Validated x86 ISA Model, University of Texas at Austin, Ph.D. dissertation, 2016.

Relevance: details of the x86 model
Bib::bm73: R. S. Boyer and J S. Moore, “Proving Theorems about LISP Functions”, in Proceedings of the Third International Joint Conference on Artificial Intelligence (IJCAI), Stanford University, pp. 486-493, 1973.

Relevance: journal article about the Edinburgh Pure Lisp Theorem Prover (PLTP)
Bib::ghk17: S. Goel, W. A. Hunt, Jr., and M. Kaufmann, “Engineering a Formal, Executable x86 ISA Simulator for Software Verification”, in M. Hinchey, J. P. Bowen, and E.-R. Olderog, editors, Provably Correct Systems Springer, pp. 173-209, 2017.

Relevance: operational model of the x86 at both the user- and system-level and code proofs
Bib::wilding92: M. M. Wilding, Machine-checked real-time system verification (ftp://ftp.cs.utexas.edu/pub/boyer/diss/wilding.pdf), University of Texas at Austin, Ph.D. dissertation, 1996.

Relevance: a non-trivial applications program on the CLI Verified Stack
Bib::moore17: J S. Moore, “ Computing Verified Machine Address Bounds during Symbolic Exploration of Code,” in J. Bowen, H. Langmaack and E.-R. Olderog, editors, Provably Correct Systems, Springer, pp. 151-172, 2017.

Relevance: an ACL2 tool for determining whether two symbolic machine addresses may be equal
Bib::moore96: J S. Moore, Piton: A Mechanically Verified Assembly-Level Language, J S. Moore, Automated Reasoning Series, Kluwer Academic Publishers, 1996.

Relevance: verified assembler/linker/loader and a component of the CLI Verified Stack
Bib::ghkg14: S. Goel, W. A. Hunt, Jr., M. Kaufmann, and S. Ghosh, “Simulation and Formal Verification of x86 Machine-Code Programs that Make System Calls”, in Proceedings of Formal Methods in Computer-Aided Design (FMCAD'14), pp. 91-98, 2014.

Relevance: modeling and verifying machine-code programs that exhibit non-determinism
Bib::yu92: Y. Yu, Automated proofs of object code for a widely used microprocessor (ftp://ftp.cs.utexas.edu/pub/boyer/diss/yu.pdf), University of Texas at Austin, Ph.D. dissertation, 1992.

Relevance: details of the operational model of the Motorola 68020
Bib::hunt85: W. A. Hunt, Jr., FM8501: A Verified Microprocessor, University of Texas at Austin, Ph.D. dissertation, 1985 (also published as a book of the same title, Springer-Verlag LNAI 795, Heidelberg, 1994.

Relevance: first microprocessor verified at the gate level and the bottommost component of the CLI stack
Bib::boh03: R. E. Bryant and D. R. O'Hallaron, Computer Systems: A Programmer's Perspective, Prentice-Hall. First edition 2003, second edition 2011, third edition 2015.

Relevance:one of the most popular and influential textbooks on modern computer systems; its relevance here is that the book introduced the y86.
Bib::mmrv06: J. Matthews, J S. Moore, S. Ray and D. Vroon, “ Verification Condition Generation via Theorem Proving”, in Proceedings of 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006), LNCS 4246, pp. 362-376, 2006.

Relevance: how to conduct inductive assertion-style proofs from an operational semantics without a verification condition generator
Bib::bm80: R. S. Boyer and J S. Moore, “On Why It Is Impossible to Prove that the BDX930 Dispatcher Implements a Time-Sharing System”, in Sections 14 and 15 of P.M. Melliar-Smith, K. Levitt, R. Schwartz, R. Boyer, J Moore, D. Hare, R. Shostak, M. Moriconi, M. Green, and W.D. Elliot, Investigation, Development, and Evaluation of Performance Proving for Fault-Tolerant Computer Final Report, covering the period September 1978 to June 1982, SRI, July 1982.

Relevance: operational semantic model of (a fragment) of a 1970s flight control computer
Bib::bh97: B. Brock and W. A. Hunt, Jr., “Formally Specifying and Mechanically Verifying Programs for the Motorola Complex Arithmetic Processor DSP”, in 1997 IEEE International Conference on Computer Design, IEEE Computer Society, pp. 31-36, October, 1997.

Relevance: first public announcement of the CAP DSP formalization (this short article was superseded by bib::bh99)
Bib::moore99b: J S. Moore, “A Mechanically Checked Proof of a Multiprocessor Result via a Uniprocessor View”, J S. Moore, Formal Methods in System Design, 14(2), pp. 213-228, March, 1999.

Relevance: proving a relationship between two state machines
Bib::moore14: J S. Moore, “ Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete” in G. Klein and R. Gamboa, editors, Interactive Theorem Proving, ITP 2014, Springer LNCS 8558, doi.org/10.1007/978-3-319-08970-6_26, 2014.

Relevance:M1 can compute anything a Turing machine can. (The paper ought to be re-titled “Proving M1 Turing Equivalent.”)
Bib::rm04: S. Ray and J S. Moore, “Proof Styles in Operational Semantics,” in A. J. Hu and A. K. Martin, editors, Formal Methods in Computer-Aided Design (FMCAD-2004), Springer, LNCS 3312, pp. 67-81, 2004.

Relevance: ACL2 tools for transforming inductive assertion-style proofs to clock function style and vice versa
Bib::by96: R. S. Boyer and Y. Yu, “Automated Proofs of Object Code for a Widely Used Microprocessor”, Journal of the ACM 43(1), pp. 166-192, January, 1996.

Relevance: operational model of the Motorola 68020 and verification of object code generated by commercial compilers
Bib::mccarthy62: J. McCarthy, “Towards a mathematical science of computation,” Proceedings of the Information Processing Cong. 62, North-Holland, Munich, West Germany, pp. 21-28, August, 1962.

Relevance: a seminal paper in the history of formal operational semantics
Bib::bm79: R. S. Boyer and J S. Moore, A Computational Logic, Academic Press, 1979.

Relevance: implementation details of the prover that became Nqthm
Bib::sawada00: J. Sawada, “Verification of a Simple Pipelined Machine Model,” in M. Kaufmann, P. Manolios, J S. Moore, editors, Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, Chapter 9, pp. 137-150, 2000. (See also pubs::pubs-books.)

Relevance: operational model of a pipelined machine and its verification
Bib::moore99a: J S. Moore, “Proving Theorems about Java-like Byte Code,” in E.-R. Olderog and B. Steffen, editors, Correct System Design -- Recent Insights and Advances, LNCS 1710, pp. 139-162, 1999.

Relevance: M2: a JVM model similar to M1 but with method invocation (i.e., subroutine call)
Bib::sh98: J. Sawada and W. A. Hunt, Jr, “Processor Verification with Precise Exceptions and Speculative Execution”, in A. J. Hu and M. Y. Vardi, editors, Computer Aided Verification, (CAV '98), Springer-Verlag LNCS 1427, Heidelberg, pp. 135-146, 1998.

Relevance: proof method for dealing with exceptions and speculative execution
Bib::rhmm07: S. Ray, W. A. Hunt, Jr., J. Matthews, and J S. Moore, `A Mechanical Analysis of Program Verification Strategies,” Journal of Automated Reasoning, 40(4), pp. 245-269, May, 2008.

Relevance: stepwise invariants, clock functions, and inductive assertion proof styles are all equivalent
Bib::kmm00a: M. Kaufmann, P. Manolios, J S. Moore, Computer-Aided Reasoning: An Approach, Kluwer Academic Publishers, 2000.

Relevance: introduction to ACL2
Bib::ghk13: S. Goel, W. A. Hunt, Jr., and M. Kaufmann, “Abstract Stobjs and Their Application to ISA Modeling”, in R. Gamboa and J. Davis, editors, Proceedings of ACL2 Workshop 2013, Electronic Proceedings in Theoretical Computer Science, Volume 114, pp. 54-69, 2013.

Relevance: an ACL2 feature introduced to support operational semantic models
Bib::moore03a: J S. Moore, “Proving Theorems about Java and the JVM with ACL2”, in M. Broy and M. Pizka, editors, Models, Algebras and Logic of Engineering Software, IOS Press, Amsterdam, pp. 227-290, 2003.

Relevance: M5: a JVM model with method invocation, classes, and threads, with some example proofs including about mutual-exclusion
Bib::hk12: W. A. Hunt, Jr. and M. Kaufmann, “Towards a Formal Model of the x86 ISA”, University of Texas at Austin, Computer Science Department Technical Report TR-12-07, May, 2012.

Relevance: a “toy model” of the x86, built as a warm up exercise
Bib::mp67: J. McCarthy and J. Painter, “Correctness of a Compiler for Arithmetic Expressions”, Proceedings of Symposia in Applied Mathematics, 19, American Mathematical Society, 1967.

Relevance: an early (perhaps the first) compiler proof
Bib::young88: W. D. Young, A Verified Code Generator for a Subset of Gypsy (ftp://ftp.cs.utexas.edu/pub/boyer/diss/young.pdf), University of Texas at Austin, Ph.D. dissertation, 1988.

Relevance: a verified compiler (from a small Pascal-like subset to an assembly language) and a component of the CLI Verified Stack
Bib::bm97: R. S. Boyer and J S. Moore, A Computational Logic Handbook, Second Edition, Academic Press, New York, 1997.

Relevance: Nqthm user's manual
Bib::moore73: J S. Moore, “Computational Logic: Structure Sharing and Proof of Program Properties, University of Edinburgh, Ph.D. dissertation, 1973.

Relevance: details of the Edinburgh Pure Lisp Theorem Prover (PLTP)
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
Bib::bevier87: W. R. Bevier, Verified Operating System Kernel (ftp://ftp.cs.utexas.edu/pub/boyer/diss/bevier.pdf), University of Texas at Austin, Ph.D. dissertation, 1987.

Relevance: first verified operating system and a component of the CLI stack