.. PyCASSE Documentation documentation master file, created by
   sphinx-quickstart on Wed Jun 10 13:40:35 2020.
   You can adapt this file completely to your liking, but it should at least
   contain the root `toctree` directive.

.. figure:: figs/logo.png
   :width: 300
   :align: center

Welcome to PyCASSE, a Python Contract-based Analysis for Stochastic Systems Exploration Toolbox.
PyCASSE enables automated reasoning with assume-guarantee (A/G) contracts expressed in Signal Temporal Logic (STL) and Stochastic Signal Temporal Logic (StSTL).

.. figure:: figs/overview.png
   :width: 400
   :align: center

.. Brief explanation of PyCASSE

To cite PyCASSE in an academic work, please use the following bibtex entry::

   @inproceedings{Oh22,
      author = {Oh, Chanwook and Lora, Michele and Nuzzo, Pierluigi},
      title = {Quantitative verification and design space exploration under uncertainty with parametric stochastic contracts},
      year = {2022},
      booktitle = {Proceedings of the 41th International Conference on Computer-Aided Design},
      location = {San Diego, CA, USA},
      series = {ICCAD '22}
   }

.. toctree::
   :numbered:
   :maxdepth: 2

   install
   specifications
   contracts
   contracts_w_dyn
   contracts_w_param
   examples
   bib

Indices and tables
==================

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