### Abstract

Cminor is a mid-level imperative programming language; there are proved-correct optimizing compilers from C to Cminor and from Cminor to machine language. We have redesigned Cminor so that it is suitable for Hoare Logic reasoning and we have designed a Separation Logic for Cminor. In this paper, we give a small-step semantics (instead of the big-step of the proved-correct compiler) that is motivated by the need to support future concurrent extensions. We detail a machine-checked proof of soundness of our Separation Logic. This is the first large-scale machine-checked proof of a Separation Logic w.r.t. a small-step semantics. The work presented in this paper has been carried out in the Coq proof assistant. It is a first step towards an environment in which concurrent Cminor programs can be verified using Separation Logic and also compiled by a proved-correct compiler with formal end-to-end correctness guarantees.

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

Title of host publication | Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings |

Publisher | Springer Verlag |

Pages | 5-21 |

Number of pages | 17 |

ISBN (Print) | 9783540745907 |

DOIs | |

State | Published - 2007 |

Event | 20th International Conference on Theorem Proving in Higher-Order Logics, TPHOLs 2007 - Kaiserslautern, Germany Duration: Sep 10 2007 → Sep 13 2007 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 4732 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 20th International Conference on Theorem Proving in Higher-Order Logics, TPHOLs 2007 |
---|---|

Country | Germany |

City | Kaiserslautern |

Period | 9/10/07 → 9/13/07 |

### All Science Journal Classification (ASJC) codes

- Theoretical Computer Science
- Computer Science(all)

## Fingerprint Dive into the research topics of 'Separation logic for small-step Cminor'. Together they form a unique fingerprint.

## Cite this

*Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings*(pp. 5-21). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4732 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-540-74591-4_3