Skip to content
/ TAES Public

Coq definitions and proofs for a tiny subset of CSP (communicating sequential processes)

Notifications You must be signed in to change notification settings

gabritto/TAES

Folders and files

NameName
Last commit message
Last commit date

Latest commit

6851276 · Jul 17, 2020

History

44 Commits
Nov 25, 2018
Sep 7, 2018
Jul 17, 2020
Sep 6, 2018
Sep 6, 2018
Sep 6, 2018
Sep 6, 2018
Sep 6, 2018
Sep 7, 2018
Sep 15, 2018
Sep 27, 2018
Sep 25, 2018
Sep 30, 2018
Oct 2, 2018
Oct 2, 2018
Sep 8, 2018

Repository files navigation

TAES

Code for the Advanced Topics in Software Engineering (TAES) course. The course used Coq to develop programs and prove properties about them. There are Coq files for each class, with completed exercises. There is also a project that defines a tiny subset of CSP, a traces semantic for it, and proves the correctness of the functional definition of traces with regards to the inductive relation definition of traces.

About

Coq definitions and proofs for a tiny subset of CSP (communicating sequential processes)

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published