Current Year

Azmy, N., Merz, S., & Weidenbach, C. (2018). A Machine-checked Correctness Proof for Pastry. Science of Computer Programming, 158. doi:10.1016/j.scico.2017.08.003
Export
BibTeX
@article{Azmy2018, TITLE = {A machine-checked correctness proof for {Pastry}}, AUTHOR = {Azmy, Noran and Merz, Stephan and Weidenbach, Christoph}, LANGUAGE = {eng}, ISSN = {0167-6423}, DOI = {10.1016/j.scico.2017.08.003}, PUBLISHER = {Elsevier}, ADDRESS = {Amsterdam}, YEAR = {2018}, DATE = {2018}, JOURNAL = {Science of Computer Programming}, VOLUME = {158}, PAGES = {64--80}, }
Endnote
%0 Journal Article %A Azmy, Noran %A Merz, Stephan %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T A Machine-checked Correctness Proof for Pastry : %G eng %U http://hdl.handle.net/21.11116/0000-0001-4F95-F %R 10.1016/j.scico.2017.08.003 %7 2017 %D 2018 %J Science of Computer Programming %V 158 %& 64 %P 64 - 80 %I Elsevier %C Amsterdam %@ false
Blanchette, J. C., Fleury, M., Lammich, P., & Weidenbach, C. (2018). A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. Journal of Automated Reasoning, 61(1-4). doi:10.1007/s10817-018-9455-7
Export
BibTeX
@article{Blanchette2018, TITLE = {A Verified {SAT} Solver Framework with Learn, Forget, Restart, and Incrementality}, AUTHOR = {Blanchette, Jasmin Christian and Fleury, Mathias and Lammich, Peter and Weidenbach, Christoph}, LANGUAGE = {eng}, ISSN = {0168-7433}, DOI = {10.1007/s10817-018-9455-7}, PUBLISHER = {Springer}, ADDRESS = {New York, NY}, YEAR = {2018}, DATE = {2018}, JOURNAL = {Journal of Automated Reasoning}, VOLUME = {61}, NUMBER = {1-4}, PAGES = {333--365}, }
Endnote
%0 Journal Article %A Blanchette, Jasmin Christian %A Fleury, Mathias %A Lammich, Peter %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality : %G eng %U http://hdl.handle.net/21.11116/0000-0001-7ADB-0 %R 10.1007/s10817-018-9455-7 %7 2018 %D 2018 %J Journal of Automated Reasoning %V 61 %N 1-4 %& 333 %P 333 - 365 %I Springer %C New York, NY %@ false
Fleury, M., Blanchette, J. C., & Lammich, P. (2018). A Verified SAT Solver with Watched Literals using Imperative HOL. In CPP’18, 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. Los Angeles, CA, USA: ACM. doi:10.1145/3167080
Export
BibTeX
@inproceedings{FleuryCPP2018, TITLE = {A verified {SAT} solver with watched literals using imperative {HOL}}, AUTHOR = {Fleury, Mathias and Blanchette, Jasmin Christian and Lammich, Peter}, LANGUAGE = {eng}, ISBN = {978-1-4503-5586-5}, DOI = {10.1145/3167080}, PUBLISHER = {ACM}, YEAR = {2018}, DATE = {2018}, BOOKTITLE = {CPP'18, 7th ACM SIGPLAN International Conference on Certified Programs and Proofs}, EDITOR = {Andronick, June and Felty, Amy}, PAGES = {158--171}, ADDRESS = {Los Angeles, CA, USA}, }
Endnote
%0 Conference Proceedings %A Fleury, Mathias %A Blanchette, Jasmin Christian %A Lammich, Peter %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T A Verified SAT Solver with Watched Literals using Imperative HOL : %G eng %U http://hdl.handle.net/21.11116/0000-0001-4174-3 %R 10.1145/3167080 %D 2018 %B 7th ACM SIGPLAN International Conference on Certified Programs and Proofs %Z date of event: 2018-01-08 - 2018-01-09 %C Los Angeles, CA, USA %B CPP'18 %E Andronick, June; Felty, Amy %P 158 - 171 %I ACM %@ 978-1-4503-5586-5
Schlichtkrull, A., Blanchette, J. C., Traytel, D., & Waldmann, U. (2018). Formalization of Bachmair and Ganzinger’s Ordered Resolution Prover. Archive of Formal Proofs.
Export
BibTeX
@article{BlanchetteAFP2018, TITLE = {Formalization of {B}achmair and {G}anzinger’s Ordered Resolution Prover}, AUTHOR = {Schlichtkrull, Anders and Blanchette, Jasmin Christian and Traytel, Dmitriy and Waldmann, Uwe}, LANGUAGE = {eng}, ISSN = {2150-914X}, YEAR = {2018}, JOURNAL = {Archive of Formal Proofs}, }
Endnote
%0 Journal Article %A Schlichtkrull, Anders %A Blanchette, Jasmin Christian %A Traytel, Dmitriy %A Waldmann, Uwe %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Formalization of Bachmair and Ganzinger’s Ordered Resolution Prover : %G eng %U http://hdl.handle.net/21.11116/0000-0000-6489-5 %7 2018-01-18 %D 2018 %8 18.01.2018 %J Archive of Formal Proofs %@ false %U https://www.isa-afp.org/browser_info/current/AFP/Ordered_Resolution_Prover/document.pdf