Program Verification
via Finite Automata

workshop, spring 2016

About the Workshop


Omega-Automata

from Wikipedia: In automata theory, an ω-automaton is a variation of finite automaton that runs on infinite strings as input. Since ω-automata do not stop, they have a variety of acceptance conditions rather than simply a set of accepting states. ω-automata are useful for specifying behavior of systems that are not expected to terminate, such as hardware, operating systems and control systems.

Workshop

Program Verification via Finite State Automata is a workshop given by Professor Muli Safra from Tel-Aviv University. The workshop covers the topic of Omega-automata and focuses particularly on Safra's determinization algorithms for some of the non-deterministic Omega-automata variations (Buchi, Streett) into deterministic numbered automata (DNA).

Website

This website presents the final projects of all teams in the workshop. Click on "Projects" on the top menu to view and browse the various projects results. In addition, the source code for both NBA-DNA and NSA-DNA constructions is given under Source Code on the top menu.

The Workshop Projects