[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: acl2@xxxxxxxxxxxxx, <coq-club@xxxxxxxxxxxxxxxxx>, <formal-methods@xxxxxxxxxxxxx>, <hol-info@xxxxxxxxxxxxxxxxxxxxx>, <isabelle-users@xxxxxxxxxxxx>, <mizar-forum@xxxxxxxxxxxxxxx>, <nuprlnotes@xxxxxxxxxxxxxx>, <pvs@xxxxxxxxxxx>, <rewriting@xxxxxxxxxxx>, <theorem-provers@xxxxxxxxxx>, <theory-logic@xxxxxxxxxx>*Subject*: [PVS] ISPASS-08 Tutorial: Call for Participation*From*: Osman Hasan <o_hasan@xxxxxxxxxxxxxxxx>*Date*: Mon, 31 Mar 2008 15:08:40 -0400 (Eastern Daylight Time)*Cc*:*List-archive*: <http://lists.csl.sri.com/mailman/private/pvs>*List-help*: <mailto:pvs-request@csl.sri.com?subject=help>*List-id*: PVS <pvs.csl.sri.com>*List-post*: <mailto:pvs@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs>, <mailto:pvs-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs>, <mailto:pvs-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-bounces+archive=csl.sri.com@xxxxxxxxxxx

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@xxxxxxxxxxxxxxxx} 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/

- Prev by Date:
**[PVS] 3rd International Compulog/ALP Summer School on Logic Programming and Computational Logic** - Next by Date:
**[PVS] [CIBCB] CIBCB08 - submission deadline extension** - Previous by thread:
**[PVS] 3rd International Compulog/ALP Summer School on Logic Programming and Computational Logic** - Next by thread:
**[PVS] [CIBCB] CIBCB08 - submission deadline extension** - Index(es):