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.