3

Towards proved formal specification and verification of STL operators as synchronous observers

Submission [pdf] Proofs [pdf] Lustre files Eventually [lus] Always [lus] Until [lus] script to generate tables [sh] Logs (here nodes are analyzed at once, while figures were reported node by node in a modular way in the paper, see build script)