Tenth Summer School on Formal Techniques
May 22-28, 2021
Due to the pandemic, the Tenth Summer School on Formal
Techniques that was postponed from last year will be virtual this year.
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.
Algebraic Program Analysis:
Automating Abstract Interpretation
Thomas Reps (University of Wisconsin)
(see Supplemental Material below)
Abstract: I will lecture about two topics, which constitute
the major parts of -- and the latest chapters of -- a
twenty-five-year quest to raise the level of automation in
abstract interpretation. They concern two parts of the creation
of correct-by-construction static analyzers.
The first talk, "Algebraic program analysis," describes recent
work on fixed-point-finding methods for solving the kinds of
equation systems that arise in abstract interpretation. The second
talk, "Automating abstract interpretation," covers three
approaches that my collaborators and I developed to automate the
construction of the abstract transformers used (on the right-hand
sides) in such equation systems. In particular, the talk tries to
characterize how they stack up on 4 issues:
- What formalism is used to express concrete semantics?
- What formalism is used to specify the abstract domain?
- What is the "engine" at work that applies/constructs abstract transformers
(and, in particular, whether it provides a way to
- merely apply an abstract transformer, or to
- compile/synthesize a representation of an abstract
transformer that can be manipulated as an explicit artifact)?
- How is the inherent non-compositionality of abstract
interpretation dealt with (if at all)?
The research on these questions has allowed us to establish
connections between abstract interpretation and several other
areas of computer science, including dynamic descriptive
complexity, automated reasoning/decision procedures, concept
learning, and constraint programming.
Algebraic program analysis:
Automating abstract interpretation:
SMT-streamlined Software Model Checking
Natasha E. Sharygina (Universita della Svizzera Italiana)
Abstract: Formal verification using model checking and
related logic-based reasoning is a popular though highly
non-trivial approach when it comes to reasoning about software
correctness. It often requires ingenuity both from the
verification tools developers and their users. In this session I
will present an approach which interleaves SMT-based reasoning
with the basic model checking tasks thus enabling scalable
verification and simplifying the use of the tools for non-experts.
The integrated development of a model checker backed up by the
efficient SMT solver is the key; SMT solving is used not only as a
computational engine of reasoning as in most existing tools, but
also for system modelling and the automated adjustment of its
precision necessary for scalable verification. I will illustrate
the integrated approach using our HiFrog and UpProver projects
which feature a function-summarization-based model checker using
SMT as the modelling and summarization language. Our model checker
supports various encoding precisions through SMT, i.e.,
uninterpreted functions, linear real and integer arithmetic, and
propositional logic. In addition the tool allows optimised
traversal of reachability properties, counter-example-guided
summary refinement, summary compression, and user-provided
summaries. I will describe the use of the tool through the
description of its architecture and a rich set of features and
compare it to our earlier work where we invented the SAT-based
function summarization approach. The presentation will be
complemented by labs which will demonstrate an experimental
evaluation on the practical impact the different SMT precisions
have on program verification.
Proving Properties of Algorithms, Hardware,
and Software with ACL2
J Strother Moore and Warren A. Hunt,
Jr. (University of Texas)
(ACL2 home page (see
Supplemental Material below))
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,
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.
Executable Formal Specification and Verification in Maude
Jose Meseguer (University of Illinois at Urbana-Champaign)
Abstract: Rewriting Logic is a simple, yet very expressive,
computational logic in which a wide range of concurrent systems,
programming languages, biological systems, and also other logical
formalisms and tools can be specified and analyzed. Maude is a
high-performance declarative language based directly on rewriting
logic. Using Maude, the formal specification of a system as a
rewrite theory can be: (i) excuted and simulated; (ii) model
checked; (iii) symbolically excuted and model checked with
symbolic states/inputs, and (iv) formally analyzed using various
model checking and theorem proving tools in the Maude formal
environment. The lectures will give an introduction to rewriting
logic and to the use of Maude in formal specification and
A recent paper that can provide a good overview of Maude and its
most recent symbolic features is:
Francisco Durán, Steven Eker, Santiago Escobar, Narciso
Martí-Oliet, José Meseguer, Rubén Rubio, Carolyn L. Talcott:
Programming and symbolic computation in Maude.
J. Log. Algebr. Meth. Program. 110 (2020)
Speaking Logic: Background Course
The main lectures in the summer school will be preceded by a background course on logic
Natarajan Shankar and Stéphane Graham-Lengrand (SRI CSL):
Abstract: Formal logic has become the lingua franca of
computing. It is used for specifying digital systems, annotating
programs with assertions, defining the semantics of programming
languages, and proving or refuting claims about software or hardware
systems. Familiarity with the language and methods of logic is a
foundation for research into formal aspects of computing. This course
covers the basics of logic focusing on the use of logic as a medium for
formalization and proof.
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: Underrepresented minority
refers to African Americans, Mexican-Americans, Native Americans
(American Indians, Alaska Natives, and Native Hawaiians),
Pacific Islanders, and mainland Puerto Ricans.