Pub-programming-languages
Programming Languages and Software Verification
-
Mechanized
Information Flow Analysis through Inductive Assertions, Warren A. Hunt, Jr., Robert Bellarmine Krug, Sandip Ray, and William
D. Young. In A. Cimatti and R. B. Jones, editors,
Proceedings of the 8th
International Conference on Formal Methods in Computer-aided Design
(FMCAD 2008), Portland, OR, November 2008, pages 227-230. IEEE Computer
Society.
-
Evaluating SFI for a CISC Architecture by Stephen McCamant and Greg
Morrisett. In 15th USENIX Security Symposium, (Vancouver, BC, Canada),
August 2-4, 2006, pp. 209-224. See also the project page.
-
Mechanized Operational
Semantics by J Moore (lectures given at Marktoberdorf Summer
School 2008). These lectures explain how to formalize an
“operational” or “state-transition” semantics of a von Neumann
programming language in a functional programming language.
These lectures illustrate the techniques by formalizing a simple
programming language called “M1,” for “Machine (or Model) 1.” It
is loosely based on the Java Virtual Machine but has been simplified
for pedagogical purposes. They demonstrate the executability of M1
models. Several styles of code proofs are developed, including direct
(symbolic simulation) proofs based on Boyer-Moore “clock functions”
and Floyd-Hoare inductive assertion proofs. Proofs are constructed
only for the simplest of programs, namely an iterative factorial
example. But to illustrate a more realistic use of the model, the
correctness proof for an M1 implementation of the Boyer-Moore fast
string searching algorithm is discussed.
-
A
Mechanical Analysis of Program Verification Strategies, Sandip Ray, Warren
A. Hunt, Jr. John Matthews, and J Strother Moore. Journal of
Automated Reasoning. volume 40(4), May 2008, pages 245-269. Springer.
-
Verification Condition Generation via Theorem Proving, John Matthews, J
S. Moore, Sandip Ray, and Daron Vroon. In M. Hermann and
A. Voronkov, editors, Proceedings of the 13th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning (LPAR 2006), Phnom Penh,
Cambodia, November 2006, volume 4246 of LNCS, pages 362-376. Copyright Springer-Verlag
- A Verifying Core for a Cryptographic Language Compiler, Lee Pike,
Mark Shields, and John Matthews. In P. Manolios and M. Wilding
(eds.), Proceedings of the 6th International
Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006),
Seattle, WA, August 2006, pages 95-98. Proceeding have also been published in the ACM
Digital Library. Copyright ACL2 Steering Committee.
See also the supporting
materials.
-
Proof Styles in Operational Semantics, Sandip Ray and J S. Moore.
In A. J. Hu and A. K. Martin,
editors, Proceedings of the 5th International Conference on Formal Methods in
Computer-aided Design (FMCAD 2004), Austin, TX, November 2004, volume 3312
of LNCS, pages 67-81. Copyright Springer-Verlag.
- Design Verification of a Safety-Critical Embedded Verifier, Piergiorgio
Bertoli and Paolo Traverso, Chapter 14 of Computer-Aided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory 1999/embedded/ in the community-books.)
This article shows the use of ACL2 for the design verification of
a piece of safety-critical software, the Embedded Verifier. The Embedded
Verifier checks online that each execution of a safety-critical translator is
correct. The translator is a component of a software system used by Union
Switch and Signal to build trainborne control systems. The ACL2 scripts
referenced here provide the full details of the results described in the
article along with solutions to all the exercises in the article.
- Compiler Verification Revisited, Wolfgang Goerigk, Chapter 15 of Computer-Aided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory 1999/compiler/ in the community-books.)
This study illustrates a fact observed by Ken Thompson in his
Turing Award Lecture: the machine code of a correct compiler can be altered
to contain a Trojan Horse so that the compiler passes almost every test,
including the so-called “bootstrap test” in which it compiles its own
source code with identical results, and still be capable of generating
“bad” code. The compiler, the object code machine, and the experiments are
formalized in ACL2. The ACL2 scripts referenced here provide the full
details of the results described in the article along with solutions to all
the exercises in the article.
- Proving Theorems about Java-like Byte Code, J
Moore, in E.-R. Olderog and B. Steffen (eds.) Correct System Design ---
Recent Insights and Advances, LNCS: State-of-the-Art-Survey, Volume 1710,
pp. 139--162, 1999). This paper describes a formalization of an abstract
machine very similar to the Java Virtual Machine but far simpler. Techniques
are developed for specifying the properties of classes and methods for this
machine. The paper illustrates two such proofs, that of a static method
implementing the factorial function and of an instance method that
destructively manipulates objects in a way that takes advantage of
inheritance. An ACL2 Script is also available.
- Mechanized
Formal Reasoning about Programs and Computing Machines, Bob Boyer and J
Moore, in R. Veroff (ed.), Automated Reasoning and Its Applications:
Essays in Honor of Larry Wos, MIT Press, 1996. This paper explains a
formalization style that has been extremely successful in enabling
mechanized reasoning about programs and machines, illustrated in ACL2. This
paper presents the so-called “small machine” model, an extremely simple
processor whose state consists of the program counter, a RAM, an execute-only
program space, a control stack and a flag. The paper explains how to prove
theorems about such models. Accompanying the paper is an
ACL2 Script: After fetching this script, use include-book to
load it into your ACL2 and then do (in-package "SMALL-MACHINE").
