Qed. Computing What Remains To Be Proved
Proceedings of the 6th International Symposium on NASA Formal Methods - Volume 8430(2014)
Abstract
We propose a framework for manipulating in a efficient way terms and formulae in classical logic modulo theories. Qed was initially designed for the generation of proof obligations of a weakest-precondition engine for C programs inside the Frama-C framework, but it has been implemented as an independent library. Key features of Qed include on-the-fly strong normalization with various theories and maximal sharing of terms in memory. Qed is also equipped with an extensible simplification engine. We illustrate the power of our framework by the implementation of non-trivial simplifications inside the Wp plug-in of Frama-C. These optimizations have been used to prove industrial, critical embedded softwares.
MoreTranslated text
Key words
Proof Obligation, Logical Connective, Automate Theorem Prover, Variable Elimination, Weak Precondition
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined