Current Year

Bradford, R., Davenport, J. H., England, M., Errami, H., Gerdt, V., Grigoriev, D., … Weber, A. (2020). Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks. Journal of Symbolic Computation, 98. doi:10.1016/j.jsc.2019.07.008
Export
BibTeX
@article{BradfordDavenport:19a, TITLE = {Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks}, AUTHOR = {Bradford, Russell and Davenport, James H. and England, Matthew and Errami, Hassan and Gerdt, Vladimir and Grigoriev, Dima and Hoyt, Charles and Ko{\v s}ta, Marek and Radulescu, Ovidiu and Sturm, Thomas and Weber, Andreas}, LANGUAGE = {eng}, ISSN = {0747-7171}, DOI = {10.1016/j.jsc.2019.07.008}, PUBLISHER = {Academic Press}, ADDRESS = {London}, YEAR = {2020}, DATE = {2020}, JOURNAL = {Journal of Symbolic Computation}, VOLUME = {98}, PAGES = {84--119}, }
Endnote
%0 Journal Article %A Bradford, Russell %A Davenport, James H. %A England, Matthew %A Errami, Hassan %A Gerdt, Vladimir %A Grigoriev, Dima %A Hoyt, Charles %A Košta, Marek %A Radulescu, Ovidiu %A Sturm, Thomas %A Weber, Andreas %+ External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks : %G eng %U http://hdl.handle.net/21.11116/0000-0002-F04B-B %R 10.1016/j.jsc.2019.07.008 %7 2020 %D 2020 %J Journal of Symbolic Computation %V 98 %& 84 %P 84 - 119 %I Academic Press %C London %@ false
Fleury, M. (2020). Formalization of logical calculi in Isabelle/HOL. Universität des Saarlandes, Saarbrücken.
Abstract
I develop a formal framework for propositional satifisfiability with the conflict-driven clause learning (CDCL) procedure using the Isabelle/HOL proof assistant. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis-Putnam-Logemann-Loveland procedure. The most noteworthy aspects of my work are the inclusion of rules for forget and restart and the refinement approach. I use the formalization to develop three extensions: First, an incremental solving extension of CDCL. Second, I verify an optimizing CDCL (OCDCL): Given a cost function on literals, OCDCL derives an optimal model with minimum cost. Finally, I work on model covering. Thanks to the CDCL framework I can reuse, these extensions are easier to develop. Through a chain of refinements, I connect the abstract CDCL calculus first to a more concrete calculus, then to a SAT solver expressed in a simple functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The imperative version relies on the two-watched-literal data structure and other optimizations found in modern solvers. I used the Isabelle Refinement Framework to automate the most tedious refinement steps. After that, I extend this work with further optimizations like blocking literals and the use of machine words as long as possible, before switching to unbounded integers to keep completeness.
Export
BibTeX
@phdthesis{Fleuryphd2019, TITLE = {Formalization of logical calculi in Isabelle/{HOL}}, AUTHOR = {Fleury, Mathias}, LANGUAGE = {eng}, DOI = {10.22028/D291-30179}, SCHOOL = {Universit{\"a}t des Saarlandes}, ADDRESS = {Saarbr{\"u}cken}, YEAR = {2020}, DATE = {2020}, ABSTRACT = {I develop a formal framework for propositional satifisfiability with the conflict-driven clause learning (CDCL) procedure using the Isabelle/HOL proof assistant. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis-Putnam-Logemann-Loveland procedure. The most noteworthy aspects of my work are the inclusion of rules for forget and restart and the refinement approach. I use the formalization to develop three extensions: First, an incremental solving extension of CDCL. Second, I verify an optimizing CDCL (OCDCL): Given a cost function on literals, OCDCL derives an optimal model with minimum cost. Finally, I work on model covering. Thanks to the CDCL framework I can reuse, these extensions are easier to develop. Through a chain of refinements, I connect the abstract CDCL calculus first to a more concrete calculus, then to a SAT solver expressed in a simple functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The imperative version relies on the two-watched-literal data structure and other optimizations found in modern solvers. I used the Isabelle Refinement Framework to automate the most tedious refinement steps. After that, I extend this work with further optimizations like blocking literals and the use of machine words as long as possible, before switching to unbounded integers to keep completeness.}, }
Endnote
%0 Thesis %A Fleury, Mathias %Y Weidenbach, Christoph %A referee: Biere, Armin %+ Automation of Logic, MPI for Informatics, Max Planck Society International Max Planck Research School, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Formalization of logical calculi in Isabelle/HOL : %G eng %U http://hdl.handle.net/21.11116/0000-0005-AE07-0 %R 10.22028/D291-30179 %I Universität des Saarlandes %C Saarbrücken %D 2020 %P 169 p. %V phd %9 phd %X I develop a formal framework for propositional satifisfiability with the conflict-driven clause learning (CDCL) procedure using the Isabelle/HOL proof assistant. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis-Putnam-Logemann-Loveland procedure. The most noteworthy aspects of my work are the inclusion of rules for forget and restart and the refinement approach. I use the formalization to develop three extensions: First, an incremental solving extension of CDCL. Second, I verify an optimizing CDCL (OCDCL): Given a cost function on literals, OCDCL derives an optimal model with minimum cost. Finally, I work on model covering. Thanks to the CDCL framework I can reuse, these extensions are easier to develop. Through a chain of refinements, I connect the abstract CDCL calculus first to a more concrete calculus, then to a SAT solver expressed in a simple functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The imperative version relies on the two-watched-literal data structure and other optimizations found in modern solvers. I used the Isabelle Refinement Framework to automate the most tedious refinement steps. After that, I extend this work with further optimizations like blocking literals and the use of machine words as long as possible, before switching to unbounded integers to keep completeness. %U https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/28722