## VeriStar

swMATH ID: | 9393 |

Software Authors: | Stewart, Gordon; Beringer, Lennart; Appel, Andrew W. |

Description: | Verified heap theorem prover by paramodulation. We present VeriStar, a verified theorem prover for a decidable subset of separation logic. Together with VeriSmall, 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, a tightly integrated collection of machine-verified program logics and compilers giving foundational correctness guarantees.par 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. |

Homepage: | http://dl.acm.org/citation.cfm?doid=2364527.2364531 |

Keywords: | paramodulation; separation logic; theorem proving |

Related Software: | Coq; jStar; Smallfoot; Rocksalt; Gallina; VeriSmall; SLAyer |

Referenced in: | 3 Publications |

all
top 5

### Referenced by 9 Authors

1 | Appel, Andrew W. |

1 | Beringer, Lennart |

1 | Blazy, Sandrine |

1 | GorĂ©, Rajeev Prabhakar |

1 | Hou, Zhe |

1 | Laporte, Vincent |

1 | Pichardie, David |

1 | Stewart, Gordon |

1 | Tiu, Alwen Fernanto |

### Referenced in 1 Serial

1 | Journal of Automated Reasoning |

### Referenced in 2 Fields

3 | Computer science (68-XX) |

1 | Mathematical logic and foundations (03-XX) |