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

COMP 335/435
| `Department of Computer Science <http://luc.edu/cs>`_
| `Loyola University Chicago <http://luc.edu>`_

You have reached the home of the Formal Methods in Software Engineering course (COMP 335/435) in the Computer Science Department of Loyola University Chicago.


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

.. warning::

   These notes are still under construction for spring 2025, 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
   35-specification
   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>`_



AI Disclosure
-------------

This text contains a mix of original writing and programming with strategic use of ChatGPT via intentional prompting. 
Some examples will be available in our repository with an appropriate build configurations and tests. 
We may also make some prompts and analyses available, similar to what my colleagues have done for their recent ongoing study of ChatGPT and Systems Programming. 
See also https://doi.org/10.6084/m9.figshare.22257274.



.. 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