Extending Coq with Imperative Features and Its Application to SAT Verification

Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry. Extending Coq with Imperative Features and Its Application to SAT Verification. In Matt Kaufmann, Lawrence C. Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. Volume 6172 of Lecture Notes in Computer Science, pages 83-98, Springer, 2010. [doi]

@inproceedings{ArmandGST10,
  title = {Extending Coq with Imperative Features and Its Application to SAT Verification},
  author = {Michaël Armand and Benjamin Grégoire and Arnaud Spiwack and Laurent Théry},
  year = {2010},
  doi = {10.1007/978-3-642-14052-5_8},
  url = {http://dx.doi.org/10.1007/978-3-642-14052-5_8},
  researchr = {https://researchr.org/publication/ArmandGST10},
  cites = {0},
  citedby = {0},
  pages = {83-98},
  booktitle = {Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
  editor = {Matt Kaufmann and Lawrence C. Paulson},
  volume = {6172},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-14051-8},
}