Find Research outputs

Search in all content

Filters for Research output

Search concepts
Selected filters

Publication Year

  • 2018
  • 2014
  • 2012
  • 2011

Author

  • Jasmin Christian Blanchette
  • 6 results
  • Export search results

Search results

  • Article

    A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

    Blanchette, J. C., Fleury, M., Lammich, P. & Weidenbach, C., 12 Mar 2018, In: Journal of Automated Reasoning. 2018, 1-4, p. 1-33 33 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access
  • Conference contribution

    A verified SAT solver with watched literals using Imperative HOL

    Fleury, M., Blanchette, J. C. & Lammich, P., Jan 2018, CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018. New York, NY: Association for Computing Machinery, Inc, p. 158-171 14 p.

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

  • Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

    Schlichtkrull, A., Blanchette, J. C., Traytel, D. & Waldmann, U., 2018, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, p. 89-107 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10900 LNAI).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

  • Superposition for Lambda-Free Higher-Order Logic

    Bentkamp, A., Blanchette, J. C., Cruanes, S. & Waldmann, U., 2018, Automated Reasoning: 9th International Joint Conference, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 Oxford, UK, July 14–17, 2018 Proceedings. Galmiche, D., Schulz, S. & Sebastiani, R. (eds.). Springer/Verlag, p. 28-46 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10900 LNAI).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

  • Superposition with Datatypes and Codatatypes

    Blanchette, J. C., Peltier, N. & Robillard, S., 2018, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, p. 370-387 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10900 LNAI).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

  • Editorial

    Introduction to Milestones in Interactive Theorem Proving

    Avigad, J., Blanchette, J. C., Klein, G., Paulson, L., Popescu, A. & Snelting, G., Jun 2018, In: Journal of Automated Reasoning. 61, p. 1-8 8 p.

    Research output: Contribution to JournalEditorialAcademicpeer-review

    Open Access
    File
    28 Downloads (Pure)