### Abstract

We present VeriStar, a verified theorem prover for a decidable subset of separation logic. Together with VeriSmall [3], a proved-sound Smallfoot-style program analysis for C minor, VeriStar demonstrates that fully machine-checked static analyses equipped with efficient theorem provers are now within the reach of formal methods. As a pair, VeriStar and VeriSmall represent the first application of the Verified Software Toolchain [4], a tightly integrated collection of machine-verified program logics and compilers giving foundational correctness guarantees. VeriStar is (1) purely functional, (2) machine-checked, (3) end-to-end, (4) efficient and (5) modular. By purely functional, we mean it is implemented in Gallina, the pure functional programming language embedded in the Coq theorem prover. By machine-checked, we mean it has a proof in Coq that when the prover says "valid", the checked entailment holds in a proved-sound separation logic for C minor. By end-to-end, we mean that when the static analysis+theorem prover says a C minor program is safe, the program will be compiled to a semantically equivalent assembly program that runs on real hardware. By efficient, we mean that the prover implements a state-of-the-art algorithm for deciding heap entailments and uses highly tuned verified functional data structures. By modular, we mean that VeriStar can be retrofitted to other static analyses as a plug-compatible entailment checker and its soundness proof can easily be ported to other separation logics.

Original language | English (US) |
---|---|

Title of host publication | ICFP'12 - Proceedings of the 2012 ACM SIGPLAN International Conference on Functional Programming |

Pages | 3-14 |

Number of pages | 12 |

DOIs | |

State | Published - Oct 22 2012 |

Event | 17th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012 - Copenhagen, Denmark Duration: Sep 9 2012 → Sep 15 2012 |

### Publication series

Name | Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP |
---|

### Other

Other | 17th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012 |
---|---|

Country | Denmark |

City | Copenhagen |

Period | 9/9/12 → 9/15/12 |

### All Science Journal Classification (ASJC) codes

- Software

## Fingerprint Dive into the research topics of 'Verified heap theorem prover by paramodulation'. Together they form a unique fingerprint.

## Cite this

*ICFP'12 - Proceedings of the 2012 ACM SIGPLAN International Conference on Functional Programming*(pp. 3-14). (Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP). https://doi.org/10.1145/2364527.2364531