Tenth Summer School on Formal Techniques

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.

Lecturers

• 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:
  1. What formalism is used to express concrete semantics?
  2. What formalism is used to specify the abstract domain?
  3. What is the "engine" at work that applies/constructs abstract transformers (and, in particular, whether it provides a way to
     1. merely apply an abstract transformer, or to
     2. compile/synthesize a representation of an abstract transformer that can be manipulated as an explicit artifact)?
  4. 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.
  Supplemental Material:

  Algebraic program analysis:

  • Compositional Recurrence Analysis,
  • Program analyses using Newton's method,
  • Newtonian program analysis via tensor product,
  • Compositional recurrence analysis revisited,
  • Non-linear reasoning for invariant synthesis
  
  

  Automating abstract interpretation:

  • Paper

• Specification, Implementation, and Verification of Network Properties
  Pamela Zave (Princeton University) ()
  Abstract: Today's networks are overly complex and not trustworthy. At the same time, society is ever-more-dependent on network services, and is continually creating new uses for them, accompanied by new requirements. These problems have stimulated a great deal of interest in new ways to develop and deploy network logic (both hardware and software), particularly with the help of automated code generation. They have also stimulated interest in verification of network services, which becomes easier when network logic is developed in a disciplined way. These lectures present a new model of networking that has proven successful at describing today's networks precisely, facilitating recognition of re-usable patterns, and providing a well-structured, modular framework for implementation and verification. They include the first formal model of networking that supports unified reasoning about all the logical (as opposed to quantitative) properties of networks. Based on this model, the lectures and labs will explore the specification, implementation, and verification of desirable network properties. Properties will be specified (at least partially) in Alloy, and their specifications will be validated with the Alloy Analyzer. We will be working with an Internet simulator and a P4 implementation of generic forwarders. To implement a toy network with specific properties enforced by routing and forwarding, we can use Alloy to synthesize forwarding rules and install them in the forwarders. Because the synthesis automatically guarantees most proof lemmas in these experiments, we will discuss the issues and possibilities surrounding verification of properties in real networks. We will also discuss implications of the close relationship between networks and distributed systems.
• 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, 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.
• 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 verification.

  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

• Natarajan Shankar and Stéphane Graham-Lengrand (SRI CSL):
  Speaking Logic
  (Speaking Logic, PVS Tutorial)
  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.

Invited Speakers

TBA

Schedule

TBA

Previous Summer Schools on Formal Techniques

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

• SSFT19
• SSFT18
• SSFT17
• SSFT16
• SSFT15
• SSFT14
• SSFT13
• SSFT12
• SSFT11

Jay Bosamiya of CMU has blogged about the 2018 Summer School at https://www.jaybosamiya.com/blog/2018/05/31/ssft/

Registration

We expect to provide support for the travel and accommodation for (a limited number of) students registered at US universities. We welcome applications from non-US students as well as non-students (if space permits). Non-US students will have to cover their own travel; the cost (which covers meals and lodging) is:

• US$800 for the summer school (SSFT20)
• US$700 for the boot camp (FMiTF)

Due to the ongoing Covid-19 pandemic, the Tenth Summer School and Formal Techniques and the First Formal Methods in the Field Bootcamp have been postponed until further notice. Registration will be closed for now and will reopen once the event has been rescheduled. If you have already registered, we will contact you when we have a new schedule.