-
Yannick Moy and Claude Marché.
Inferring Local (Non-) Aliasing and Strings for Memory Safety.
Heap Analysis and Verification (HAV'07),
pp 35-51,
2007.
Keyword(s): abstract interpretation.
@article{moyInferringLocalNon2007,
title = {Inferring Local (Non-) Aliasing and Strings for Memory Safety},
author = {Moy, Yannick and March{\'e}, Claude},
year = {2007},
pages = {35--51},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4708-Moy_Marche (2007) - Inferring local (non-) aliasing and strings for memory safety.pdf},
journal = {Heap Analysis and Verification (HAV'07)},
keywords = {abstract interpretation}
}
-
Sumit Gulwani and Ashish Tiwari.
An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software.
In Werner Damm and Holger Hermanns, editors, Computer Aided Verification,
volume 4590,
pages 379-392.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
2007.
ISBN: 978-3-540-73367-6.
Keyword(s): abstract interpretation.
@incollection{gulwaniAbstractDomainAnalyzing2007,
title = {An {{Abstract Domain}} for {{Analyzing Heap}}-{{Manipulating Low}}-{{Level Software}}},
booktitle = {Computer {{Aided Verification}}},
author = {Gulwani, Sumit and Tiwari, Ashish},
editor = {Damm, Werner and Hermanns, Holger},
year = {2007},
volume = {4590},
pages = {379--392},
publisher = {{Springer Berlin Heidelberg}},
address = {{Berlin, Heidelberg}},
doi = {10.1007/978-3-540-73368-3_42},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4702-Gulwani_Tiwari (2007) - An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software.pdf},
isbn = {978-3-540-73367-6},
keywords = {abstract interpretation}
}
-
Osman Hasan and Sofiène Tahar.
Formalization of Continuous Probability Distributions.
In Frank Pfenning, editor, Automated Deduction - CADE-21,
volume 4603,
pages 3-18.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
2007.
ISBN: 978-3-540-73594-6 978-3-540-73595-3.
ISSN: 0302-9743, 1611-3349.
Keyword(s): HOL,
probability.
Abstract: |
In order to overcome the limitations of state-of-the-art simulation based probabilistic analysis, we propose to perform probabilistic analysis within the environment of a higher-order-logic theorem prover. The foremost requirement for conducting such analysis is the formalization of probability distributions. In this report, we present a methodology for the formalization of continuous probability distributions for which the inverse of the cumulative distribution function can be expressed in a closed mathematical form. Our methodology is primarily based on the formalization of the Standard Uniform random variable, cumulative distribution function properties and the Inverse Transform method. The report presents all this formalization using the HOL theorem prover. In order to illustrate the practical effectiveness of our methodology, the formalization of a few continuous probability distributions has also been included. |
@incollection{hasanFormalizationContinuousProbability2007,
title = {Formalization of {{Continuous Probability Distributions}}},
booktitle = {Automated {{Deduction}} -{} {{CADE}}-21},
author = {Hasan, Osman and Tahar, Sofi{\`e}ne},
editor = {Pfenning, Frank},
year = {2007},
volume = {4603},
pages = {3--18},
publisher = {{Springer Berlin Heidelberg}},
address = {{Berlin, Heidelberg}},
issn = {0302-9743, 1611-3349},
doi = {10.1007/978-3-540-73595-3_2},
abstract = {In order to overcome the limitations of state-of-the-art simulation based probabilistic analysis, we propose to perform probabilistic analysis within the environment of a higher-order-logic theorem prover. The foremost requirement for conducting such analysis is the formalization of probability distributions. In this report, we present a methodology for the formalization of continuous probability distributions for which the inverse of the cumulative distribution function can be expressed in a closed mathematical form. Our methodology is primarily based on the formalization of the Standard Uniform random variable, cumulative distribution function properties and the Inverse Transform method. The report presents all this formalization using the HOL theorem prover. In order to illustrate the practical effectiveness of our methodology, the formalization of a few continuous probability distributions has also been included.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4309-Hasan_Tahar (2007) - Formalization of Continuous Probability Distributions.pdf},
isbn = {978-3-540-73594-6 978-3-540-73595-3},
keywords = {HOL,probability},
}