Imperial College London > Talks@ee.imperial > Clare E Drysdale's list > Machines Reasoning about Machines
Log inImperial users Other users No account?Information onFinding a talk Adding a talk Syndicating talks Who we are Everything else |
Machines Reasoning about MachinesAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Clare E Drysdale. Computer hardware and software can be modelled precisely in mathematical logic. If expressed appropriately, these models can be executable. This allows them to be used as simulation engines or rapid prototypes. But because they are formal they can be manipulated by symbolic means: theorems can be proved about them, directly, with mechanical theorem provers. But how practical is this vision of machines reasoning about machines? In this highly personal talk, I will describe the 45 year history of the ``Boyer-Moore Project,’’ starting with its use to prove simple theorems by mathematical induction about list processing (e.g., the reverse of the reverse of x is x) to its routine use in the microprocessor industry (e.g., the floating point operatios of the Via Nano 64-bit X86 microprocessor are compliant with the IEEE standard). Along the way we will see applications in program verification, models of instruction set architectures including the JVM , and security and information flow This talk is part of the Clare E Drysdale's list series. This talk is included in these lists:Note that ex-directory lists are not shown. |
Other listsTalks CAS Talks IEEE TalksOther talksPersonalized Chronic Disease Treatment Mobile Data Off-loading Deadbeat Observers for Continuous-Time Linear Systems: Historical Perspective and Recent Advances |