Date: Wed, 20 Nov 1996 19:14:45 GMT Server: Apache/1.0.3 Content-type: text/html Content-length: 2389 Last-modified: Wed, 15 May 1996 16:33:38 GMT
This research adapts a formal programming methodology to the construction of digital systems. An algebra for manipulating modeling expressions is used to reduce higher-level specifications of behavior to structures mapping directly into VLSI technologies. This work links a large body of research in program refinement---to which this department has been a significant contributor---with other formal methods as applied to digital design. A principal goal of this research has been to establish algebraic derivation as a mode of formal verification. The tendency in formal methods research toward deductive proofs of correctness does not reflect design practice. Our central thesis is that effective automated reasoning in design must provide well-integrated support of a variety of reasoning systems. Hence, a task of this project is to develop an algebraic formalism that is on a par, mathematically and mechanically, with contemporary deductive systems. A large component of our research activity has to do with the the implementation of the DDD algebra, its integration with CAD tools and other formal systems, and the application these tools to realistic design problems.
Associated Faculty:
Associated Graduate Students:
Bhaskar Bose (PhD 1994),
Kathi Fisler,
Paul Miner ,
Kamlesh Rath (PhD 1995),
M. Esen Tuna<\A>.
Zheng Zhu (PhD 1992),
Support:
Supported by NSF under grants
MIP87-07067 (1987--89), MIP89-21842 (1989--92), MIP92-08745 (1992--95),
with infrastructure support from DCR85-52598 and CDA93-03189.
For more information Coming Soon