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

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.


Speaking Logic: Background Course

The main lectures in the summer school will be preceded by a background course on logic

Invited Speakers



Previous Summer Schools on Formal Techniques

Information about previous Summer Schools on Formal Techniques can be found at

Jay Bosamiya of CMU has blogged about the 2018 Summer School at


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 that all fields are required
Male Female
Yes No
Yes No

NOTE: Underrepresented minority refers to African Americans, Mexican-Americans, Native Americans (American Indians, Alaska Natives, and Native Hawaiians), Pacific Islanders, and mainland Puerto Ricans.