## Michael Mendler

### Lax Logic and its Application to the Timing Analysis of Combinational Systems

Traditionally, classical logic is the logic of choice in formal
system analysis. This talk discusses the application of an
intuitionistic modal logic, Lax Logic, to the timing
analysis of combinational systems. In contrast to classical logic,
proofs in intuitionistic logic do not only witness the mere
extensional fact "that" a given functional specification is valid
but also provide intensional information about "how" it is valid.
The best-known technical formalisation of this is the so-called
"propositions-as-types" or "proofs-as-programs" principle.
The application of Lax Logic rests on a novel variant of this
idea, called the "proofs-as-constraints" or "proofs-as-delays"
principle. Following this principle I will show how
timing information may be extracted from proofs in Propositional Lax
Logic (PLL). This suggest a verification-driven timing analysis
system, based on an automatic theorem prover for PLL. In my talk I
will sketch the basic ingredients of such a system.

The proposed timing analysis framework exploits the fact that in PLL
one and the same (Boolean) input-output function may be represented in
many different ways. Depending on the particular the specification style
different amounts of timing information can be associated with the
function. The granularity can be adjusted within wide limits and in
this way several standard timing analysis methods, and many
non-standard ones, may be characterised as special cases of this
general principle.

June 4, 1999

3:30pm

Wean 8220