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

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

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.