Techniques based on formal logic, such as model checking, satisfiability, static analysis, and automated theorem proving, are finding a broad range of applications in modeling, analysis, verification, and synthesis. This school, the tenth in the series, will focus on the principles and practices of formal techniques, with a strong emphasis on the hands-on use and development of these technologies. It primarily targets graduate students and young researchers who are interested in studying and using formal techniques in their research. A prior background in formal methods is helpful but not required. Participants at the school can expect to have a seriously fun time experimenting with the tools and techniques presented in the lectures during laboratory sessions.
Due to the pandemic, the Tenth Summer School on Formal Techniques that was postponed from last year will be virtual this year.
We had an email failure so that some registration emails were not delivered. If you registered but haven't heard back, please drop an email to summerformal2021@gmail.com.
Virtual Machine (VM) with all the tools installed
Many tools (e.g., PVS) only run on Linux of MacOS.
Virtualbox provides a way for Windows
to create a virtual machine running Linux within Windows, without
having to dual-boot. Vagrant
makes it easy to create a VM. Install these as instructed here, get the
Vagrantfile, dated May 23 2021,
put it in a directory, start up a shell, change to that directory,
and run "vagrant up". It will take a couple of hours to set up,
depending on your connection speeds and your computer resources.
Vagrant command summary - note that aside from "up" and "help", all require a running VM
Some of the tools take a very long time to build, which seems to cause problems for vagrant. In particular, the opam installation of z3, ACL2, and Coq all can cause problems. What seems to work is to let it provision as far as it can, taking note of where it died. Then do "vagrant up", but this time instead of provisioning do a "vagrant ssh" and find the corresponding line in the Vagrantfile, and simply copy that line into the command line, along with any other lines for that tool. Alternatively, you could comment out those lines, build the rest of the VM, and do these manually afterwards.
Note: The Vagrantfile may be modified from time to time, the one linked in this page is always the most recent. To check if it changed, see if the fourth line of yours matches the above date. If the date is missing, or is earlier, then replace the old one, and run "vagrant provision" if it is already running, or "vagrant up --provision" to start it and install the modifications. It's a bad idea to provision twice in a row, it's faster the second time, but still slow. If you do this, let it complete, or some tools files may end up corrupted.
Note that even if you are running Linux or MacOS, you might want to install the tools this way, as it saves you the hassle of figuring out how to install them yourself.
More details are in the SSFT21 Vagrant notes.
Videos:
Papers:
Algebraic program analysis:
Abstract: ACL2, which stands for ``A Computational Logic for Applicative Common Lisp,'' is a mechanized logic and functional programming language in which you can model computational artifacts like algorithms, hardware designs, programming languages, and programs. ACL2 supports a robust and efficient subset of the ANSI standard programming language Common Lisp and hence can used not only as a specification language in which to model artifacts but as a prototyping environment in which models can be tested. This has made ACL2 very useful to industrial users, especially in microprocessor design, floating-point analysis, SAT proof checking, real analysis, computational biology, cryptographic algorithms and processors, metamathematics, etc.
While the theorem prover is automatic, the user has a great deal of control over how it approaches any given problem. The most common control mechanisms are the ``appropriate'' formalizations of models and properties and the identification of key lemmas. The ACL2 expert can control proofs in a wide variety of ways, including writing new proof procedures and using ACL2 to verify their soundness. The ACL2 Community Books repository contains thousands of ``books'' of useful lemmas, some of which provide verified proof procedures, like SAT checkers and bit blasting. In these lectures we will introduce ACL2 starting with the simplest proofs about recursive functions and moving up to models of simple hardware designs and programming languages. Lab exercises will emphasize the two main ways users guide ACL2:, appropriate formalization and identification of key lemmas.
Our aim is not to produce expert users but to position students to be able to learn more if they're interested. We assume students are not allergic to Lisp's parenthesis-laden prefix notation and are somewhat familiar with Emacs. We will, however, confine the lectures and labs to relatively small feature subsets of both Lisp and Emacs.
Supplemental Material: The ACL2 home page contains the ACL2 source code, installation instructions, and extensive user-level documentation. Not only should ACL2 be installed, but its regression suite should be recertified and be locally available. A full regression recertification takes about 8 hours and verifies thousands of books containing over a hundred thousand theorems. (It is easier to recertify them all than to recertify the cone of books needed in the lab exercises.) Students wishing to get a head start should buy the book Computer-Aided Reasoning: An Approach, Matt Kaufmann, Panagiotis Manolios, and J Strother Moore, Kluwer Academic Publishers, June, 2000. (ISBN 0-7923-7744-3). The Kluwer price for the hardback edition is excessive but the book can be obtained in paperback form from Lulu by following the Book 1 link.
Slides:
Introduction to ACL2
Notes:
ACL2 Notes
Videos:
Videos:
Abstract: Software bugs are a persistent feature of daily life---crashing web browsers, allowing cyberattacks, and distorting the results of scientific computations. One approach to improving software uses program invariants---mathematical descriptions of program behaviors---to verify code and detect bugs. In this talk, I present DIG, a dynamic analysis framework for discovering useful classes of program invariants that appear in many practical applications. I will also talk about my work on automatic program repair, which automatically generates fixes for buggy programs. Finally, I will discuss how invariant generation and program repair can be applied to solve problems in several emerging domains including configurable systems and AI-generated software.
Bio: ThanhVu Nguyen is an assistant professor in the Department of Computer Science and Engineering at the University of Nebraska-Lincoln. His current research is in the intersection of Software Engineering and Programming Languages. In particular, he focuses on improving software quality through dynamic invariant inference, automatic program repair, and highly-configurable systems analysis.
Dr. Nguyen received his Ph.D. in computer science from the University of New Mexico-Albuquerque in 2014 and completed a 2-year postdoc at the University of Maryland in 2016. He is a recipient of the NSF CISE Career Research Initiation Initiative (CRII) Award, a 10-year Most Influential Paper award (at ICSE 2019), and a 10-year Most Impact Paper Award (at GECCO 2019).
Videos
Information about previous Summer Schools on Formal Techniques can be found at
Jay Bosamiya of CMU has blogged about the 2018 Summer School at https://www.jaybosamiya.com/blog/2018/05/31/ssft/
Those who already registered for the 2020 event need not reregister, and you will be contacted to check if you would like your registration to be processed. Although the summer school is virtual and there is no registration fee, attendance is restricted to registered participants. Attendees who complete the summer school will receive a certificate by mail. Applications should be submitted together with names of two references (preferably advisors, professors, or senior colleagues) using the form below.
Applicants are urged to submit their applications before April 30, 2021, since there are only a limited number of spaces available. We strongly encourage the participation of women and under-represented minorities in the summer school.
†NOTE: Underrepresented minority refers to African Americans, Mexican-Americans, Native Americans (American Indians, Alaska Natives, and Native Hawaiians), Pacific Islanders, and mainland Puerto Ricans.