Merge branch 'master' of https://gitlab.fi.muni.cz/xjonas/DTEDI (cee98701) · Commits · Martin Jonáš / DTEDI

Bibliography.bib

+562 −1

Original line number	Original line	Diff line number	Diff line
	@@ -192,3 +192,564 @@
	pages = {155--184},		pages = {155--184},
	year = {2009}		year = {2009}
	}		}

			@inproceedings{HD04,
			author = {Jinbo Huang and
			Adnan Darwiche},
			title = {Toward Good Elimination Orders for Symbolic {SAT} Solving},
			booktitle = {16th {IEEE} International Conference on Tools with Artificial Intelligence
			{(ICTAI} 2004), 15-17 November 2004, Boca Raton, FL, {USA}},
			pages = {566--573},
			year = {2004}
			}

			@inproceedings{AV01,
			author = {Alfonso San Miguel Aguirre and
			Moshe Y. Vardi},
			title = {Random 3-SAT and BDDs: The Plot Thickens Further},
			booktitle = {Principles and Practice of Constraint Programming - {CP} 2001, 7th
			International Conference, {CP} 2001, Paphos, Cyprus, November 26 -
			December 1, 2001, Proceedings},
			pages = {121--136},
			year = {2001}
			}

			@inproceedings{JS04,
			author = {HoonSang Jin and
			Fabio Somenzi},
			title = {CirCUs: {A} Hybrid Satisfiability Solver},
			booktitle = {{SAT} 2004 - The Seventh International Conference on Theory and Applications
			of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada,
			Online Proceedings},
			year = {2004}
			}

			@inproceedings{PV04,
			author = {Guoqiang Pan and
			Moshe Y. Vardi},
			title = {Search vs. Symbolic Techniques in Satisfiability Solving},
			booktitle = {{SAT} 2004 - The Seventh International Conference on Theory and Applications
			of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada,
			Online Proceedings},
			year = {2004}
			}

			@article{Bry86,
			author = {Randal E. Bryant},
			title = {Graph-Based Algorithms for Boolean Function Manipulation},
			journal = {{IEEE} Trans. Computers},
			volume = {35},
			number = {8},
			pages = {677--691},
			year = {1986}
			}

			@inproceedings{HKB96,
			author = {Ramin Hojati and
			Sriram C. Krishnan and
			Robert K. Brayton},
			title = {Early Quantification and Partitioned Transition Relations},
			booktitle = {1996 International Conference on Computer Design {(ICCD} '96), {VLSI}
			in Computers and Processors, October 7-9, 1996, Austin, TX, USA, Proceedings},
			pages = {12--19},
			year = {1996}
			}

			@incollection{DP09,
			author = {Adnan Darwiche and
			Knot Pipatsrisawat},
			title = {Complete Algorithms},
			booktitle = {Handbook of Satisfiability},
			pages = {99--130},
			year = {2009}
			}

			@inproceedings{HKWB11,
			author = {Marijn Heule and
			Oliver Kullmann and
			Siert Wieringa and
			Armin Biere},
			title = {Cube and Conquer: Guiding {CDCL} {SAT} Solvers by Lookaheads},
			booktitle = {Hardware and Software: Verification and Testing - 7th International
			Haifa Verification Conference, {HVC} 2011, Haifa, Israel, December
			6-8, 2011, Revised Selected Papers},
			pages = {50--65},
			year = {2011}
			}

			@inproceedings{HKM16,
			author = {Marijn J. H. Heule and
			Oliver Kullmann and
			Victor W. Marek},
			title = {Solving and Verifying the Boolean Pythagorean Triples Problem via
			Cube-and-Conquer},
			booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2016 - 19th
			International Conference, Bordeaux, France, July 5-8, 2016, Proceedings},
			pages = {228--245},
			year = {2016}
			}

			@inproceedings{LS04,
			author = {Shuvendu K. Lahiri and
			Sanjit A. Seshia},
			title = {The {UCLID} Decision Procedure},
			booktitle = {Computer Aided Verification, 16th International Conference, {CAV}
			2004, Boston, MA, USA, July 13-17, 2004, Proceedings},
			pages = {475--478},
			year = {2004}
			}

			@incollection{BSST09,
			author = {Clark W. Barrett and
			Roberto Sebastiani and
			Sanjit A. Seshia and
			Cesare Tinelli},
			title = {Satisfiability Modulo Theories},
			booktitle = {Handbook of Satisfiability},
			pages = {825--885},
			year = {2009}
			}

			@inproceedings{Barcelogic,
			author = {Robert Nieuwenhuis and
			Albert Oliveras},
			title = {Decision Procedures for SAT, {SAT} Modulo Theories and Beyond. The
			BarcelogicTools},
			booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 12th
			International Conference, {LPAR} 2005, Montego Bay, Jamaica, December
			2-6, 2005, Proceedings},
			pages = {23--46},
			year = {2005}
			}

			@inproceedings{CVC4,
			author = {Clark Barrett and
			Christopher L. Conway and
			Morgan Deters and
			Liana Hadarean and
			Dejan Jovanovic and
			Tim King and
			Andrew Reynolds and
			Cesare Tinelli},
			title = {{CVC4}},
			booktitle = {Computer Aided Verification - 23rd International Conference, {CAV}
			2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
			pages = {171--177},
			year = {2011}
			}

			@inproceedings{MathSAT,
			author = {Alessandro Cimatti and Alberto Griggio and Bastiaan Schaafsma and Roberto Sebastiani},
			title = {{The MathSAT5 SMT Solver}},
			editor = {Nir Piterman and Scott Smolka},
			booktitle = {Proceedings of TACAS},
			year = {2013},
			volume = {7795},
			series = {LNCS},
			publisher = {Springer},
			}

			@article{Simplify,
			author = {David Detlefs and
			Greg Nelson and
			James B. Saxe},
			title = {Simplify: a theorem prover for program checking},
			journal = {J. {ACM}},
			volume = {52},
			number = {3},
			pages = {365--473},
			year = {2005}
			}

			@inproceedings{Yices,
			author = {Bruno Dutertre},
			title = {Yices 2.2},
			booktitle = {Computer Aided Verification - 26th International Conference, {CAV}
			2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
			Austria, July 18-22, 2014. Proceedings},
			pages = {737--744},
			year = {2014}
			}

			@inproceedings{Z3,
			author = {Leonardo Mendon{\c{c}}a de Moura and
			Nikolaj Bj{\o}rner},
			title = {{Z3:} An Efficient {SMT} Solver},
			booktitle = {Tools and Algorithms for the Construction and Analysis of Systems,
			14th International Conference, {TACAS} 2008, Held as Part of the Joint
			European Conferences on Theory and Practice of Software, {ETAPS} 2008,
			Budapest, Hungary, March 29-April 6, 2008. Proceedings},
			pages = {337--340},
			year = {2008}
			}

			@inproceedings{OpenSMT,
			author = {Roberto Bruttomesso and
			Edgar Pek and
			Natasha Sharygina and
			Aliaksei Tsitovich},
			title = {The OpenSMT Solver},
			booktitle = {Tools and Algorithms for the Construction and Analysis of Systems,
			16th International Conference, {TACAS} 2010, Held as Part of the Joint
			European Conferences on Theory and Practice of Software, {ETAPS} 2010,
			Paphos, Cyprus, March 20-28, 2010. Proceedings},
			pages = {150--153},
			year = {2010}
			}

			@inproceedings{FJOS03,
			author = {Cormac Flanagan and
			Rajeev Joshi and
			Xinming Ou and
			James B. Saxe},
			title = {Theorem Proving Using Lazy Proof Explication},
			booktitle = {Computer Aided Verification, 15th International Conference, {CAV}
			2003, Boulder, CO, USA, July 8-12, 2003, Proceedings},
			pages = {355--367},
			year = {2003}
			}

			@inproceedings{ABCKS02,
			author = {Gilles Audemard and
			Piergiorgio Bertoli and
			Alessandro Cimatti and
			Artur Kornilowicz and
			Roberto Sebastiani},
			title = {A {SAT} Based Approach for Solving Formulas over Boolean and Linear
			Mathematical Propositions},
			booktitle = {Automated Deduction - CADE-18, 18th International Conference on Automated
			Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings},
			pages = {195--210},
			year = {2002}
			}

			@inproceedings{ACG99,
			author = {Alessandro Armando and
			Claudio Castellini and
			Enrico Giunchiglia},
			title = {SAT-Based Procedures for Temporal Reasoning},
			booktitle = {Recent Advances in {AI} Planning, 5th European Conference on Planning,
			ECP'99, Durham, UK, September 8-10, 1999, Proceedings},
			pages = {97--108},
			year = {1999}
			}

			@article{Seb07,
			author = {Roberto Sebastiani},
			title = {Lazy Satisfiability Modulo Theories},
			journal = {{JSAT}},
			volume = {3},
			number = {3-4},
			pages = {141--224},
			year = {2007}
			}

			@inproceedings{Cot10,
			author = {Scott Cotton},
			title = {Natural Domain {SMT:} {A} Preliminary Assessment},
			booktitle = {Formal Modeling and Analysis of Timed Systems - 8th International
			Conference, {FORMATS} 2010, Klosterneuburg, Austria, September 8-10,
			2010. Proceedings},
			pages = {77--91},
			year = {2010}
			}

			@article{Mon16,
			author = {David Monniaux},
			title = {A Survey of Satisfiability Modulo Theory},
			journal = {CoRR},
			volume = {abs/1606.04786},
			year = {2016}
			}

			@inproceedings{BNOT06,
			author = {Clark Barrett and
			Robert Nieuwenhuis and
			Albert Oliveras and
			Cesare Tinelli},
			title = {Splitting on Demand in {SAT} Modulo Theories},
			booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 13th
			International Conference, {LPAR} 2006, Phnom Penh, Cambodia, November
			13-17, 2006, Proceedings},
			pages = {512--526},
			year = {2006}
			}

			@inproceedings{CC79,
			author = {Patrick Cousot and
			Radhia Cousot},
			title = {Systematic Design of Program Analysis Frameworks},
			booktitle = {Conference Record of the Sixth Annual {ACM} Symposium on Principles
			of Programming Languages, San Antonio, Texas, USA, January 1979},
			pages = {269--282},
			year = {1979}
			}

			@inproceedings{BSHGK13,
			author = {Martin Brain and
			Vijay D'Silva and
			Leopold Haller and
			Alberto Griggio and
			Daniel Kroening},
			title = {An Abstract Interpretation of {DPLL(T)}},
			booktitle = {Verification, Model Checking, and Abstract Interpretation, 14th International
			Conference, {VMCAI} 2013, Rome, Italy, January 20-22, 2013. Proceedings},
			pages = {455--475},
			year = {2013}
			}

			@inproceedings{SHK13,
			author = {Vijay D'Silva and
			Leopold Haller and
			Daniel Kroening},
			title = {Abstract conflict driven learning},
			booktitle = {The 40th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
			Programming Languages, {POPL} '13, Rome, Italy - January 23 - 25,
			2013},
			pages = {143--154},
			year = {2013}
			}

			@article{BSGHK14,
			author = {Martin Brain and
			Vijay D'Silva and
			Alberto Griggio and
			Leopold Haller and
			Daniel Kroening},
			title = {Deciding floating-point logic with abstract conflict driven clause
			learning},
			journal = {Formal Methods in System Design},
			volume = {45},
			number = {2},
			pages = {213--245},
			year = {2014}
			}

			@inproceedings{DHK14,
			author = {Vijay D'Silva and
			Leopold Haller and
			Daniel Kroening},
			title = {Abstract satisfaction},
			booktitle = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
			Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21,
			2014},
			pages = {139--150},
			year = {2014}
			}

			@inproceedings{GSF08,
			author = {Dan Goldwasser and
			Ofer Strichman and
			Shai Fine},
			title = {A Theory-Based Decision Heuristic for {DPLL(T)}},
			booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2008, Portland, Oregon,
			USA, 17-20 November 2008},
			pages = {1--8},
			year = {2008}
			}

			@inproceedings{MJ13,
			author = {Leonardo de Moura and
			Dejan Jovanović},
			title = {A Model-Constructing Satisfiability Calculus},
			booktitle = {Verification, Model Checking, and Abstract Interpretation, 14th International
			Conference, {VMCAI} 2013, Rome, Italy, January 20-22, 2013. Proceedings},
			pages = {1--12},
			year = {2013}
			}

			@INPROCEEDINGS{JMB13,
			author = {Dejan Jovanović and
			Clark Barrett and
			Leonardo de Moura},
			booktitle = {Formal Methods in Computer-Aided Design (FMCAD), 2013},
			title = {The design and implementation of the model constructing satisfiability calculus},
			year = {2013},
			pages = {173-180}
			}

			@misc{Ack54,
			title = "Solvable cases of the decision problem",
			author = "Wilhelm Ackermann",
			series = "Studies in logic and the foundations of mathematics",
			publisher = "North-Holland",
			address = "Amsterdam",
			year = {1954}
			}

			@article{MB08,
			author = {Leonardo Mendon{\c{c}}a de Moura and
			Nikolaj Bj{\o}rner},
			title = {Model-based Theory Combination},
			journal = {Electr. Notes Theor. Comput. Sci.},
			volume = {198},
			number = {2},
			pages = {37--49},
			year = {2008}
			}

			@book{Dan63,
			address = {Princeton, NJ},
			author = {George B. Dantzig},
			pagetotal = {XVI, 625},
			ppn_gvk = {180926950},
			publisher = {Princeton Univ. Press},
			series = {Rand Corporation Research Study},
			title = {Linear programming and extensions},
			year = 1963
			}

			@inproceedings{CGS07,
			author = {Alessandro Cimatti and
			Alberto Griggio and
			Roberto Sebastiani},
			title = {A Simple and Flexible Way of Computing Small Unsatisfiable Cores in
			{SAT} Modulo Theories},
			booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2007, 10th
			International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings},
			pages = {334--339},
			year = {2007}
			}

			@inproceedings{UltimateCores14,
			author = {Matthias Heizmann and
			J{\"{u}}rgen Christ and
			Daniel Dietsch and
			Jochen Hoenicke and
			Markus Lindenmann and
			Betim Musa and
			Christian Schilling and
			Stefan Wissert and
			Andreas Podelski},
			title = {Ultimate Automizer with Unsatisfiable Cores - (Competition Contribution)},
			booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
			- 20th International Conference, {TACAS} 2014, Held as Part of the
			European Joint Conferences on Theory and Practice of Software, {ETAPS}
			2014, Grenoble, France, April 5-13, 2014. Proceedings},
			pages = {418--420},
			year = {2014}
			}

			@inproceedings{UltimateInterpol13,
			author = {Matthias Heizmann and
			J{\"{u}}rgen Christ and
			Daniel Dietsch and
			Evren Ermis and
			Jochen Hoenicke and
			Markus Lindenmann and
			Alexander Nutz and
			Christian Schilling and
			Andreas Podelski},
			title = {Ultimate Automizer with SMTInterpol - (Competition Contribution)},
			booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
			- 19th International Conference, {TACAS} 2013, Held as Part of the
			European Joint Conferences on Theory and Practice of Software, {ETAPS}
			2013, Rome, Italy, March 16-24, 2013. Proceedings},
			pages = {641--643},
			year = {2013}
			}

			@article{Pud97,
			author = {Pavel Pudl{\'{a}}k},
			title = {Lower Bounds for Resolution and Cutting Plane Proofs and Monotone
			Computations},
			journal = {J. Symb. Log.},
			volume = {62},
			number = {3},
			pages = {981--998},
			year = {1997}
			}

			@article{McM05,
			author = {Kenneth L. McMillan},
			title = {An interpolating theorem prover},
			journal = {Theor. Comput. Sci.},
			volume = {345},
			number = {1},
			pages = {101--121},
			year = {2005}
			}

			@inproceedings{McM11,
			author = {Kenneth L. McMillan},
			title = {Interpolants from {Z3} proofs},
			booktitle = {International Conference on Formal Methods in Computer-Aided Design,
			{FMCAD} '11, Austin, TX, USA, October 30 - November 02, 2011},
			pages = {19--27},
			year = {2011}
			}

			@inproceedings{GLS11,
			author = {Alberto Griggio and
			Thi Thieu Hoa Le and
			Roberto Sebastiani},
			title = {Efficient Interpolant Generation in Satisfiability Modulo Linear Integer
			Arithmetic},
			booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
			- 17th International Conference, {TACAS} 2011, Held as Part of the
			Joint European Conferences on Theory and Practice of Software, {ETAPS}
			2011, Saarbr{\"{u}}cken, Germany, March 26-April 3, 2011. Proceedings},
			pages = {143--157},
			year = {2011}
			}

			@article{BKRW11,
			author = {Angelo Brillout and
			Daniel Kroening and
			Philipp R{\"{u}}mmer and
			Thomas Wahl},
			title = {An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic},
			journal = {J. Autom. Reasoning},
			volume = {47},
			number = {4},
			pages = {341--367},
			year = {2011}
			}

			@inproceedings{KLR10,
			author = {Daniel Kroening and
			J{\'{e}}r{\^{o}}me Leroux and
			Philipp R{\"{u}}mmer},
			title = {Interpolating Quantifier-Free Presburger Arithmetic},
			booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 17th
			International Conference, LPAR-17, Yogyakarta, Indonesia, October
			10-15, 2010. Proceedings},
			pages = {489--503},
			year = {2010}
			}

			@inproceedings{CHN12,
			author = {J{\"{u}}rgen Christ and
			Jochen Hoenicke and
			Alexander Nutz},
			title = {SMTInterpol: An Interpolating {SMT} Solver},
			booktitle = {Model Checking Software - 19th International Workshop, {SPIN} 2012,
			Oxford, UK, July 23-24, 2012. Proceedings},
			pages = {248--254},
			year = {2012}
			}

			@book{BM07,
			author = {Aaron R. Bradley and
			Zohar Manna},
			title = {The calculus of computation - decision procedures with applications
			to verification},
			publisher = {Springer},
			year = {2007}
			}

			@inproceedings{McM06,
			author = {Kenneth L. McMillan},
			title = {Lazy Abstraction with Interpolants},
			booktitle = {Computer Aided Verification, 18th International Conference, {CAV}
			2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
			pages = {123--136},
			year = {2006}
			}

			@book{End01,
			title={{A Mathematical Introduction to Logic}},
			author={Enderton, Herbert B.},
			year={2001},
			publisher={Harcourt/Academic Press}
			}

Chapters/Chapter02.tex

+306 −80

File changed.

Preview size limit exceeded, changes collapsed.

Includes/notation.tex

+14 −0

Original line number	Original line	Diff line number	Diff line
	@@ -2,10 +2,24 @@

	\newcommand{\cnf}{\textsc{cnf}\xspace}		\newcommand{\cnf}{\textsc{cnf}\xspace}
	\newcommand{\sat}{\textsc{sat}\xspace}		\newcommand{\sat}{\textsc{sat}\xspace}
			\newcommand{\smt}{\textsc{smt}\xspace}
	\newcommand{\dppr}{\textsc{dp}\xspace}		\newcommand{\dppr}{\textsc{dp}\xspace}
	\newcommand{\dpll}{\textsc{dpll}\xspace}		\newcommand{\dpll}{\textsc{dpll}\xspace}
	\newcommand{\cdcl}{\textsc{cdcl}\xspace}		\newcommand{\cdcl}{\textsc{cdcl}\xspace}
			\newcommand{\acdcl}{\textsc{acdcl}\xspace}
			\newcommand{\mcsat}{\textsc{mc-sat}\xspace}
	\newcommand{\bcp}{\textsc{bcp}\xspace}		\newcommand{\bcp}{\textsc{bcp}\xspace}
			\newcommand{\bdds}{\textsc{bdd}s\xspace}
			\newcommand{\bdd}{\textsc{bdd}\xspace}
			\newcommand{\robdd}{\textsc{robdd}\xspace}
			\newcommand{\dpllt}{\textsc{dpll(t)}\xspace}

			%solvers
			\newcommand{\uclid}{\textsc{uclid}\xspace}
			\newcommand{\fpacdcl}{\textsc{fp-acdcl}\xspace}

			%complexity
			\newcommand{\NP}{\textsf{NP}}

	\newcommand{\state}[2]{\ensuremath{#1 \; \|\| \; #2}\xspace}		\newcommand{\state}[2]{\ensuremath{#1 \; \|\| \; #2}\xspace}
	\newcommand{\dec}[1]{\ensuremath{#1^\bullet}}		\newcommand{\dec}[1]{\ensuremath{#1^\bullet}}

classicthesis.sty

+2 −2

Original line number	Original line	Diff line number	Diff line
	@@ -357,7 +357,7 @@
	{\relax}%		{\relax}%
	%{\renewcommand{\chaptermark}[1]{\markboth{\spacedlowsmallcaps{#1}}{\spacedlowsmallcaps{#1}}}}		%{\renewcommand{\chaptermark}[1]{\markboth{\spacedlowsmallcaps{#1}}{\spacedlowsmallcaps{#1}}}}
	\renewcommand{\sectionmark}[1]{\markright{\thesection\enspace\spacedlowsmallcaps{#1}}}		\renewcommand{\sectionmark}[1]{\markright{\thesection\enspace\spacedlowsmallcaps{#1}}}
	\lehead{\mbox{\llap{\small\thepage\kern2em}\headmark\hfil}}		\lehead{\mbox{\llap{\small\thepage\kern1em}\headmark\hfil}}
	\rohead{\mbox{\hfil{\headmark}\rlap{\small\kern2em\thepage}}}		\rohead{\mbox{\hfil{\headmark}\rlap{\small\kern2em\thepage}}}
	\renewcommand{\headfont}{\small}		\renewcommand{\headfont}{\small}
	% \DeclareRobustCommand{\fixBothHeadlines}[2]{} % <--- ToDo		% \DeclareRobustCommand{\fixBothHeadlines}[2]{} % <--- ToDo
	@@ -375,7 +375,7 @@
	% ********************************************************************		% ********************************************************************

	\newlength\titleindent		\newlength\titleindent
	\setlength\titleindent{.15in}		\setlength\titleindent{1em}

	\RequirePackage{titlesec}		\RequirePackage{titlesec}
	% parts		% parts