Overview
This page provides information on some of the resources available for students in CEN 6075.
This page is organized as follows:
- UCF Library Resources
- General Resources
- Specification Tools
- Theorem Provers (Proof Assistants)
- Static Verification Tools
- Dynamic Testing Tools
- Professional Societies
- Other Resources
UCF Library Resources
The UCF Library has a general guide to the literature in Computer Science, which is found at:
General Resources
Some useful web resources related to this course are:
- An Introduction to the Literature on Semantics.
- FRET: Formal Requirements Elicitation Tool (ARC-18066-1)
- The Wikipedia page on Separation Logic
- Research project from Peter Müller's group at ETH Zürich, including Prusti a verifier for Rust, and Gobra a verifier for Go, and Spec# a "a verification methodology" and "static verifier" for C#.
Specification Tools
The following tools may be useful for formal specification:
- Wikipedia's list of tools for static code analysis.
- Alloy, which is a relational logic based specification language with a model checking tool.
- Lamport's The TLA+ Home Page. TLA+ can be used for specification in general and some theorem proviing.
- Set theory page by Wolfram Research.
- XText a system for building DSLs.
- JastAdd a attribute grammar system with extensions that make it suitable for dataflow analysis.
- The Checker Framework, which enhances Java's type system to allow new pluggable type checkers to be developed.
- Behavioral Interface Specification Languages
- The global home page for Larch and the Larch FAQ.
- The Frama-C framework for engineering systems, especially those written in C. The tools include various dynamic and static analysis tools for C, including a runtime assertion checker for the ANSI/ISO C Specification Language (ACSL).
- Larch/C++
- The Java Modeling Language (JML), which can be used for design by contract (DBC) in Java.
- The VDM Specification Language (VDM-SL) and the Overture tool.
- Equational Specification and Variations
Theorem Provers (Proof Assistants)
- ACL2, which is "a logic and programming language in which you can model computer systems, together with a tool to help you prove properties of those models." The programs are written in Common Lisp.
- PVS, which is "a mechanized environment for formal specification and verification. PVS consists of a specification language, a large number of predefined theories, a type checker, an interactive theorem prover that supports the use of several decision procedures and a symbolic model checker, various utilities including a code generator and a random tester, documentation, formalized libraries, and examples that illustrate different methods of using the system in several application areas." It has been implemented by the Formal Methods in CSL [group] at SRI.
- The HOL Theorem Proving System, which is "an environment for interactive theorem proving in a higher-order logic."
- Isabelle, which is "a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus."
- The Coq Proof Assistant, which is "a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs." For learning Coq, you might be interested in the book Software Foundations by Benjamin Pierce et al. (2007).
- The Verification Infrastructure for Permission-​based Reasoning (VIPER) "language and suite of tools", which provides "an architecture on which new verification tools and prototypes can be developed simply and quickly."
Static Verification Tools
The tools listed below are sometimes combined with programming languages; they may be useful for static verification.
- The Dafny Programming and Verification Language
- The Lean Programming Language and Theorem Prover
- The Whiley Programming Language, which "employs state-of-the-art techniques for ensuring your software is correct. You can specify functions using preconditions and postconditions, and then statically verify your implementation meets its specification."
- Java PathFinder, an "extensible software analysis framework for Java bytecode."
- OpenJML's Extended Static Checker (ESC) tool does Hoare-style static verification of Java code with JML specifications.
- Bandera a model checker and model checking framework for Java programs.
- Bogor "an extensible software model checking framework".
- Static source code analysis tools for C (a listing).
- C Global Surveyor, a tool that finds bugs in C programs using abstract interpretation.
- Findbugs, a tool for finding bugs in Java code.
- The Verified Software Toolchain, which is a toolchain that "includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program."
Dynamic Testing Tools
Bertrand Meyer's Eiffel programming language has several features that support formal methods, as well as a fully-specified library, documentation, and tools. While Eiffel was originally oriented towards dynamic runtime assertion checking, in the design by contract (DbC) methodology, there are now static verification tools for Eiffel.
The following tools may be useful for dynamic testing:
- AFL++ a guided fuzzer for C focused on security.
- JML's runtime assertion checker
- Randoop: Automatic unit test generation for Java
- Kelinci, a guided fuzzer for Java.
- K semantic framework, which is "a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations and rules."
- JML has a runtime assertion checker, which is built into OpenJML.
- TheAspectJML language, which also focuses on runtime assertion checking.
Professional Societies
There are two main professional societies in computing, the Association for Computing Machinery (ACM) and the Institute for Electrical and Electronics Engineers (IEEE). The UCF Library gives access to all publications of these professional societies. Both the ACM and IEEE Computer Society have student memberships and student chapters at UCF.
ACM
The ACM has several resources for members, including a learning center.
The ACM also has various special interest groups (SIGs) that focus on particular areas of computing. Some SIGs that are relevant for this course include:
- SIGACT, which "is an international organization that fosters and promotes the discovery and dissemination of high quality research in theoretical computer science (TCS), the formal analysis of efficient computation and computational processes."
- SIGSOFT, which "seeks to improve our ability to engineer software by stimulating interaction among practitioners, researchers, and educators"
- SIGPLAN, which "explores programming language concepts and tools, focusing on design, implementation, practice, and theory."
IEEE Computer Society
The IEEE contains the Computer Society, which "advances the theory, practice, and application of computer and information-processing science and technology, as well as the professional standing of its members." Its educational resources relevant to this course include:
The IEEE Computer Society also makes Tech News available, which features "Relevant news, analysis, and blogs to keep you best informed, based on world-class research and thought leadership." You can subscribe to the Computing Edge newsletter there.
Other Resources
Conferences
The following are some important academic conferences that often contain papers on formal methods:
- The International Symposia on Formal Methods is a conference devoted to formal methods. There are open access proceedings and often various co-located conferences that are relevant.
- The International Conference on Computer-Aided Verification (CAV) is a conference that contains many interesting results about formal methods.
- International Conference on Tests and Proof (TAP) is a conference that discusses the interplay between dynamic and static techniques.
- The European Symposium on Programming (ESOP) often publishes articles about formal methods.
- The International Conference on Software Engineering (ICSE) sometimes publishes papers on formal methods.
- The ACM International Conference on the Foundations of Software Engineering (FSE), also publishes papers on formal methods.
Journals
The following journals give examples of professional writing in computer science and often contain papers that use formal methods. In most cases access to these is free from the UCF library.
- Formal Aspects of Computing (FAC)
- ACM Transactions on Programming Languages and Systems (TOPLAS)
- Science of Computer Programming (SCP)
Last modified Wednesday, January 15, 2025.
This web page is for CEN 6075 at the University of Central Florida. The details of this course are subject to change as experience dictates. You will be informed of any changes. Please direct any comments or questions to Gary T. Leavens at Leavens@ucf.edu. Some of the policies and web pages for this course are quoted or adapted from other courses I have taught, in partciular, COP 4020.