Skip to content

Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language Theory Research, Formal Methods and their application in some most active computer Science fields.

Notifications You must be signed in to change notification settings

SatyendraBanjare/plt-formal-methods-resources

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

36 Commits
 
 
 
 
 
 

Repository files navigation

Programming Language Theory & Formal Methods - Resources

FORSYTE group pics Image Courtsey : Forsyte group

Formal methods are mathematical techniques that are used for design, verification and specifications of software and hardware problems. These are essentially a subset of Programming Language Theory research that are being used to study complex computer science problems.

Analysis by Formal Methods basically involves these steps :

  1. Formal Specification
  2. Formal Proofs
  3. Model Checking
  4. Abstraction

The formal proof development and model checking are primarily done using interactive theorem provers often called as proof Assistants. Abstraction is creating structurally sound relations between parts of models.

Here is my attempt to curate a list of useful reading materials, videos and tools accompanied by some upcoming challenges in the field.

NOTE :

  1. I have tried to make the content more focused on current research and industrial application. People looking for purely academic collection must refer Formal Methods in Education - Jeremy Avigad.

  2. The reader is expected to have some basic knowledge of Type Theory. A more academic insight can be found here learn-tt.

Contents

Books & Lectures

  • Software Foundations Tool Used : I highly advice this as a starting material for diving deep into this field. The book is very helpful in building basic concepts and serves as a very sound introduction to the field. Beautifully illustrated concepts with examples to practice are provided all throughout making interactive theorem proving learning fun.

  • FRAP - Adam Chlipala Tool Used : A book that helps you understand and reason formal correctness of programs. Imperative language (C) inspired examples of data structures and algorithms helps immensely to begin thinking about their formal verification.

  • Certified Programming with Dependent Types - Adam Chlipala Tool Used : One of the best theoretical books to learn theorem proving using coq.

  • Formal Verification - Jacques Fleuriot : This a course that involves theorem proving using some more developed tools like SAT and SMT solvers.

  • Abstract Interpretation - Patrick Cousot The best available material on the theory of Abstract Interpretation. It gives a complete and pure mathematical analysis of program mutations. The Program behaviour as a continuously modifying relation between different abstract mathematical structures is explained and proved!!.

  • Logic and Proof - CMU & Lean introduction Tool Used : This is course designed at CMU and it also serves as a introductory material for theorem proving in Lean

If you feel you need more theoretical insights, please refer Note above.

Blogs

MOOCs

Tools

Proof Assistants

  • coq: The most popular and widely used theorem prover. It supports a lot of features including ML-extraction, Project packaging (Project and Makefile creation). There are plenty of how-to material available that use coq for formalization. Anyone might find this very interesting 100 Theorems in Coq.

  • lean: A fairly new Theorem Prover by Microsoft Research. Has a nice interactive tutorial, is easy to get started with.

  • PRISM model checker : It is model checker developed by University of Oxford.

  • Nuprl : Theorem Prover by Cornell under Proof Refinement Logic Project.

  • Agda: A quite Mature Proof Assistant. Has features similar to Coq. easy to learn after some experience in coq.

  • Isabelle: It is an old theorem Prover. Has nice implementation of core logic but lacks other UX related features.

  • VCC : A mechanical verifier for concurrent C programs by Microsoft.

  • TLA+ : High Level language for modelling languages and systems ( especially concurrent & distributed).

SAT/SMT/SMC solvers

SAT Solvers :

SMT Solvers :

SMC Solvers :

Hybrid Solvers

Proof Assitants have very strong implmentations of program logics. Sometimes it may not be tactically possible to carry out complex proofs only by using them. Therefore Current research combines this principle of strong logic based reasoning with powerful SMT and SMC solvers to ease the proof development. Some examples are here below :

Projects

Most of the projects are more or less development of the respective theorem provers or SAT/SMT/SMC/ solvers and hence can be looked up there. These are some of other projects actively developed.

  • DeepSpec is an umbrella project that focuses on building verified software systems. Follwoing major sub-projects are actively worked upon :

  • ikos is a reliable bug-free C compiler based on the theory of abstract interpretation.

  • Project Everest: It is research project that aims at creating secure and verified HTTPS ecosystem.

  • CertiCrypt: It is a project focuse on modelling public key cryptography using coq proof assistant.

  • Iris: Iris is a Higher-Order Concurrent Separation Logic Framework implemented and verified in the proof assistant Coq.

  • VeriDeep - Safety Verification of Deep Neural Networks

  • VeHICal : Project focused on developing the foundations of verified co-design of interfaces and control for human cyber-physical systems.

  • FastSMT - Tool to augment your SMT solver by learning to optimize its performance for your dataset of formulas. It is developed by SRI lab, ETH Zurich built on top of Z3 SMT solver.

  • fm4cps - Formal methods for Cyber Physical Systems, joint efforts by INRIA and ECNU shanghai.

Upcoming Challenges

Security Related

Abstract Interpretation focused

Programming Language Research related

This particularily deals with improving certain properties (like Parallelism & Concurrency) of existing programming languages. A lot can be easily looked up in regard to this since after all this is the sole most important reason to study PL theory. All the conferences listed up in here ACM SIGPLAN have majority of research papers on programming language development do check them out.

Related Industries & Startups

License

CC0

Any suggestions are welcome. Please do consider submitting a pull request if you feel like !!