Open AccessAn automata theory dedicated towards formal circuit synthesis
Author(s) -
Dirk Eisenbiegler,
Ramayya Kumar
Publication year - 1995
Publication title -
lecture notes in computer science
Language(s) - English
Resource type - Book series
SCImago Journal Rank - 0.249
H-Index - 400
eISSN - 1611-3349
pISSN - 0302-9743
ISBN - 3-540-60275-5
DOI - 10.1007/3-540-60275-5_63
Subject(s) - computer science , automaton , hol , constructive , automata theory , formal methods , programming language , theoretical computer science , formal verification , process (computing)
We present a theory for automata in HOL, which is dedicatedtowards formal hardware synthesis. The theory contains definitionsfor formally representing and transforming automata. In this approachhardware is represented by automata descriptions and formal synthesisis performed by applying formally proven theorems. The approach presentedis constructive --- i.e. starting from specifications at higher levelsof abstractions, synthesis can be performed by repeated applications ofthese...
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom