*To*: acl2 at cs.utexas.edu, <coq-club at pauillac.inria.fr>, <formal-methods at cs.uidaho.edu>, <hol-info at lists.sourceforge.net>, <isabelle-users at cl.cam.ac.uk>, <mizar-forum at mizar.uwb.edu.p>, <nuprlnotes at cs.cornell.edu>, <pvs at csl.sri.com>, <rewriting at ens-lyon.fr>, <theorem-provers at ai.mit.edu>, <theory-logic at cs.cmu.edu>*Subject*: [isabelle] ISPASS-08 Tutorial: Call for Participation*From*: Osman Hasan <o_hasan at ece.concordia.ca>*Date*: Mon, 31 Mar 2008 15:08:40 -0400 (Eastern Daylight Time)

We apologize if you receive multiple copies of this email. ====================================================================== Half Day Tutorial on "Performance Analysis of Systems and Software using a Theorem Prover" 2008 IEEE International Symposium on Performance Analysis of Systems and Software (ISPASS` 2008) April 20, 2008 Austin, Texas CALL FOR PARTICIPATION ====================================================================== -------- Abstract -------- Nowadays, computer simulation is one of the most widely used performance analysis technique. However, simulation based analysis usually provides approximate results due to its inherent nature and it cannot handle large-scale problems due to its enormous CPU time requirements. The unreliability of the results poses a serious problem in safety critical applications, such as those in space travel, military, and medicine, where a mismatch between the predicted and the actual system performance may result in either inefficient usage of the available resources or by unnecessarily paying higher costs to meet some performance or reliability criteria. A possible solution for overcoming these limitations is to conduct performance analysis within the environment of a higher-order-logic theorem prover. Higher-order logic is a system of deduction with a precise semantics and can be used for the development of almost all classical mathematical theories. Whereas, interactive theorem proving is the field of computer science and mathematical logic concerned with computer based formal proof tools that require some sort of human assistance. Due to the high expressiveness of the higher-order logic and the inherent soundness of interactive theorem proving, this approach can be used to conduct error free performance analysis at the cost of significant user interaction. There has been some fruitful developments in this emerging area and a preliminary infrastructure has been proposed that allows the formalization of random variables in higherorder-logic and the formal verification their useful probabilistic and statistical properties within the theorem prover. The main focus of the tutorial is to introduce this new area of research and present its practical effectiveness for conducting precise performance analysis of real world system and software examples. The tutorial begins by presenting a comprehensive introduction to formal methods and their usefulness in the system design process. It is followed by an overview of the HOL theorem prover, which is the higher-order-logic theorem prover that we have used in this project. Next, we present the process of formalizing (or modeling) random variables and verifying their correctness by proving the corresponding probabilistic and statistical properties, such as mean and variance, in HOL. These formalized random variables can be used to model the uncertainties and random elements found in a system and thus allow us to reason about its performance issues in HOL. For illustration purposes, we present the performance analysis of two examples. Firstly, we verify the average number of trials required for the Coupon Collectors problem, which is a well known commercially used algorithm. Next, we verify the average message delay relation for the Stop-and-Wait protocol, which is a commonly used Automated Repeat Request (ARQ) protocol. ---------- Organizers ---------- Osman Hasan and Sofiene Tahar, {o_hasan,tahar at ece.concordia.ca} Concordia University, Montreal, Canada --------------- Important Dates --------------- Early Registeration until: April 4th, 2008 Tutorial Date: April 20th, 2008 ---------------- More Information ---------------- For registeration and more details http://ispass.org/ispass2008/

- Previous by Date: [isabelle] propositional calculi equivalence
- Previous by Thread: [isabelle] propositional calculi equivalence
- Cl-isabelle-users March 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list