Formal Softwre Development Methods: Textbooks and Readings


  • Textbooks:
  • Verification of Sequential and Concurrent Programs

    3rd Edition, by Apt, de Boer, Olderog Entire book available online through UIUC library (go to link above and click on SpringerLink - Full Text Online Service).

  • Calculus of Computation--Bradley and Manna
    Available online from UIUC net domain.
  • Principles of Program Analysis -- Nielson, Nielson, and Hankin
    Available online from UIUC net domain.
  • Static Program Analysis -- Moller and Schwartzbach
    Available online.
  • Automated reasoning, Gerard A.W. Vreeswijk
  • Principles of Model Checking -- Baier and Katoen, MIT Press
  • Introduction to Static Analysis: An Abstract Interpretation Perspective -- Rival and Yi
    •
  • Program Verification Foundations:
  • Floyd's paper

    • Assigning Meanings to Programs , Robert W. Floyd In Schwartz, J.T. Mathematical Aspects of Computer Science. Proceedings of Symposium on Applied Mathematics. 19. American Mathematical Society. pp. 19--32, 1967.

  • Hoare's 1969 paper
  • The Rely-Guarantee Method for Verifying Shared Variable Concurrent Programs, which explains the Jones' method.
  • Dijkstra's Guarded commands, non-determinacy and formal derivation of programs, which introduces weakest precondition generation.
  • Contracts
  • Design by Contract -- Wikipedia page
  • Applying Design By Contract -- Meyer
  • Eiffel Programming Language
  • Embedded Contract Languages
  • Logic
  • An introduction to Logic, by Madhavan Mukund and S. P. Suresh
  • An introduction to Proof Theory, by Sam Buss
  • First-Order Proof Theory of Arithmetic, by Sam Buss
  • Sharad Malik's slides on the quest for efficient Boolean SAT solvers
  • Operational Semantics
  • Operational Semantics -- Steffen van Bakel
    •
  • Formal symbolic testing
  • King'76: Symbolic execution
  • DART: Directed Automated Random Testing
  • Abstraction-based verification
  • Abstract Interpretation: Cousot and Cousot 1977
  • Lecture slides by Cousot on abstract interpretation
  • Graf-Saidi: Construction of abstract state graphs with PVS
  • The SLAM story: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft
  • Parameteric Shape Analysis via 3-valued logic
  • Model-checking
  • Software Model Checking -- Ranjit Jhala and Rupak Majumdar
  • Symbolic Model-Checking (Ken McMillan's Ph.D. thesis)
    • Tools:
  • Verification tools
  • DAFNY - a verification engine for a small object-oriented programming langauge.
    See DAFNY INFORMATION PAGE for more information on installing and using Dafny.
  • SAT/SMT Solvers
  • Z3 - an SMT solver.
  • Other tools
  • Dafny
    Download an install, maybe with Visual Studio.
    Also see online site where you can use it: Rise4fun/Dafny
  • Boogie
  • Visual Studio 2010 includes CodeContracts which allows writing contracts for .NET code.
  • VCC - a verifier for concurrent C that uses Boogie.
  • Constraint-solver based symbolic testing
  • PEX from Microsoft generates tests automatically; can exploit .NET code contracts to generate tests satisfying pre-conditions for unit testing.
  • PEX for fun - An online tool that illustrates PEX for educational purposes.
  • A sample program where PEX does not find the error (uncommenting i=1000 shows error)
  • Abstract Interpretation
  • ASTREE analyzer used in verification of Airbus flight control software. Commercial product from AbsInt.
  • APRON - library for numerical abstract domains.
  • Interproc analyzer for a toy language using Apron, available with an online interface.
  • TVLA - supports standard abstract domains as well as shape analysis.
  • Predicate Abstraction
  • SLAM/SDV: A tool for verifying device drivers against Windows APIs
  • Explicit Model checking
  • Java Path Finder from NASA
  • ZING from MSR
    • Previous Iterations of the Course:
  • Elsa Gunter's CS 477 (Spring 2020)
  • Madhusudan Parthasarathy's CS 477 (Spring 2019)
    •