Lecture Notes: Formal Methods in Software Engineering
=====================================================

`Comp 335 <https://academics.cs.luc.edu/courses/comp335.html>`_
| `Department of Computer Science <http://luc.edu/cs>`_
| `Loyola University Chicago <http://luc.edu>`_

*Welcome! Willkomme! ¡Bienvenidos/as! Benvenuti/e!*

.. warning::

   These notes are still under construction for spring 2024, so expect a few rough edges. But we're getting closer!
   Your contributions are *highly welcome!*
   Please submit `issues <https://github.com/lucformalmethodscourse/lucformalmethodscourse.github.io/issues>`_
   and `pull requests <https://github.com/lucformalmethodscourse/lucformalmethodscourse.github.io/pulls>`_.

In this course, we study formal methods suitable for contemporary software engineering practice. 
This version of the course is normally taught by `Konstantin Läufer <https://laufer.cs.luc.edu>`_.

Please get started by reading the :doc:`10-overview`.

.. toctree::
   :maxdepth: 3
   :caption: Contents
   :numbered:
   :hidden:

   10-overview
   15-softwareengineering
   20-foundations
   30-testing
   40-modelchecking
   50-rtverification
   70-summary

   80-software
   85-resources 
   90-syllabi
   95-todo

Latest version
   |version|
   
Build status
   .. only:: html

      .. image:: https://github.com/lucformalmethodscourse/lucformalmethodscourse.github.io/actions/workflows/main.yml/badge.svg
         :target: https://github.com/lucformalmethodscourse/lucformalmethodscourse.github.io/actions
         :alt: GitHub Pages and Release PDF

   See `github.com/lucformalmethodscourse/lucformalmethodscourse.github.io/actions <https://github.com/lucformalmethodscourse/lucformalmethodscourse.github.io/actions>`_

Repository
   `github.com/lucformalmethodscourse/lucformalmethodscourse.github.io <https://github.com/lucformalmethodscourse/lucformalmethodscourse.github.io>`_

Releases
   The current book (|version|) in PDF is available at
   `GitHub Releases <https://github.com/lucformalmethodscourse/lucformalmethodscourse.github.io/releases/latest>`_


.. todo:: Indices and tables (put at end of TOC above)

   * :ref:`genindex`
   * :ref:`modindex`


.. todo:: add sample projects, activities, tests, and (tiered) master list for presentations