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
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, edsitors,
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::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 ACL2
books).
Relevance: operational model of a pipelined machine
and its verification - 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::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