Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
Martin Jonáš
DTEDI
Commits
b8836e93
Commit
b8836e93
authored
Sep 05, 2016
by
Martin Jonáš
Browse files
Mostly added references
parent
7a11c67b
Changes
5
Hide whitespace changes
Inline
Sidebyside
Bibliography.bib
View file @
b8836e93
...
...
@@ 1237,4 +1237,104 @@ year = {2005},
Part {I}}
,
pages
=
{269280}
,
year
=
{2015}
}
@incollection
{
BKOSSB07
,
year
=
{2007}
,
booktitle
=
{Tools and Algorithms for the Construction and Analysis of Systems, {TACAS} 2007}
,
volume
=
{4424}
,
series
=
{LNCS}
,
title
=
{{Deciding BitVector Arithmetic with Abstraction}}
,
publisher
=
{Springer}
,
author
=
{Bryant, Randal E. and Kroening, Daniel and Ouaknine, Jo{\"{e}}l and Seshia, Sanjit A. and Strichman, Ofer and Brady, Bryan}
,
pages
=
{358372}
,
}
@book
{
Har09
,
author
=
{Harrison, John}
,
title
=
{{Handbook of Practical Logic and Automated Reasoning}}
,
year
=
2009
,
edition
=
{1st}
,
publisher
=
{Cambridge University Press}
,
}
@TECHREPORT
{
BFT15
,
author
=
{Clark Barrett and Pascal Fontaine and Cesare Tinelli}
,
title
=
{{The SMTLIB Standard: Version 2.5}}
,
institution
=
{Department of Computer Science, The University of Iowa}
,
year
=
2015
,
note
=
{Available at {\tt www.SMTLIB.org}}
}
@inproceedings
{
ZZG13
,
author
=
{Yunhui Zheng and
Xiangyu Zhang and
Vijay Ganesh}
,
title
=
{Z3str: a z3based string solver for web application analysis}
,
booktitle
=
{Joint Meeting of the European Software Engineering Conference and
the {ACM} {SIGSOFT} Symposium on the Foundations of Software Engineering,
ESEC/FSE'13, Saint Petersburg, Russian Federation, August 1826, 2013}
,
pages
=
{114124}
,
year
=
{2013}
}
@inproceedings
{
RB16
,
author
=
{Andrew Reynolds and
Jasmin Christian Blanchette}
,
title
=
{A Decision Procedure for (Co)datatypes in {SMT} Solvers}
,
booktitle
=
{Proceedings of the TwentyFifth International Joint Conference on
Artificial Intelligence, {IJCAI} 2016, New York, NY, USA, 915 July
2016}
,
pages
=
{42054209}
,
year
=
{2016}
}
@article
{
CGPD08
,
author
=
{Cristian Cadar and
Vijay Ganesh and
Peter M. Pawlowski and
David L. Dill and
Dawson R. Engler}
,
title
=
{{EXE:} Automatically Generating Inputs of Death}
,
journal
=
{{ACM} Trans. Inf. Syst. Secur.}
,
volume
=
{12}
,
number
=
{2}
,
year
=
{2008}
}
@inproceedings
{
CDE08
,
author
=
{Cristian Cadar and
Daniel Dunbar and
Dawson R. Engler}
,
title
=
{{KLEE:} Unassisted and Automatic Generation of HighCoverage Tests
for Complex Systems Programs}
,
booktitle
=
{8th {USENIX} Symposium on Operating Systems Design and Implementation,
{OSDI} 2008, December 810, 2008, San Diego, California, USA, Proceedings}
,
pages
=
{209224}
,
year
=
{2008}
}
@article
{
CFM12
,
author
=
{Lucas C. Cordeiro and
Bernd Fischer and
Jo{\~{a}}o Marques{}Silva}
,
title
=
{SMTBased Bounded Model Checking for Embedded {ANSIC} Software}
,
journal
=
{{IEEE} Trans. Software Eng.}
,
volume
=
{38}
,
number
=
{4}
,
pages
=
{957974}
,
year
=
{2012}
}
@inproceedings
{
KLW13
,
author
=
{Daniel Kroening and Matt Lewis and Georg Weissenbacher}
,
title
=
{UnderApproximating Loops in {C} Programs for Fast Counterexample
Detection}
,
booktitle
=
{Computer Aided Verification  25th International Conference, {CAV}
2013}
,
pages
=
{381396}
,
year
=
{2013}
,
series
=
{LNCS}
,
volume
=
{8044}
,
publisher
=
{Springer}
}
\ No newline at end of file
CHANGES
View file @
b8836e93
Changes
in
version
4.2
(
September
2015
)
o
Fixed
issue
between
titlesec
and
tocloft
regarding
part
numbering
in
the
ToC
(
classicthesis
.
sty
).
part
numbering
in
the
ToC
(
classicthesis
.
sty
).
Thanks
to
Enrico
Gregorio
and
Henri
Menke
.
o
Fixed
bug
with
colored
lines
and
graffiti
o
Fixed
bug
with
colored
lines
and
graffiti
(
classicthesis
.
sty
).
Thanks
to
Enrico
Gregorio
and
Stefano
Bragaglia
for
the
fix
! (Also switched
graffiti
from
\
slshape
to
\
itshape
.)
o
Changed
\
vspace
*{
8
ex
}
to
\
vspace
{
8
ex
}
(
Contents
.
tex
)
o
Moved
\
cleardoublepage
from
end
of
Contents
.
tex
o
Changed
\
vspace
*{
8
ex
}
to
\
vspace
{
8
ex
}
(
Contents
.
tex
)
o
Moved
\
cleardoublepage
from
end
of
Contents
.
tex
to
appropriate
position
in
ClassicThesis
.
tex
o
\
bflabel
of
acronym
package
removed
,
as
it
was
o
\
bflabel
of
acronym
package
removed
,
as
it
was
removed
from
acronym
package
and
caused
errors
.
Now
set
\
aclabelfont
to
\
acsfont
for
consistency
.
o
Converted
major
files
to
UTF

8
(
thanks
to
J
ö
rn
Hees
)
(
Bibliography
.
bib
excluded
for
now
as
BibTeX
cannot
handle
UTF

8
)
o
Added
support
for
BibLaTeX
in
o
Added
support
for
BibLaTeX
in
classicthesis

config
.
tex
and
Bibliography
.
tex
(
thanks
to
J
ö
rn
Hees
).
For
LyX
we
will
have
a
work

around
for
testing
.
o
Added
an
example
for
one
's own publication list
(via BibLaTeX) in Publications.tex (renamed from
(via BibLaTeX) in Publications.tex (renamed from
Publication.tex)
o Replaced/updated scrpage2 with scrlayerscrpage
in classicthesis.sty (thanks to Ivo Pletìkosić).
X Worked on Appendix case with floatperchapter
o Replaced/updated scrpage2 with scrlayerscrpage
in classicthesis.s
g
ty (thanks to Ivo Pletìkosić).
X Worked on Appendix case with floatperchapter
(works for captions but not for references so far)
Thanks to Claus Lahiri and Clemens Niederberger
Thanks to Claus Lahiri and Clemens Niederberger
for their help on this.
[REMOVED DUE TO OTHER PROBLEMS, SEE ISSUE #82]
[REMOVED DUE TO OTHER PROBLEMS, SEE ISSUE #82]
X Removed fixltx2e from classicthesisconfig.tex and
have classicthesis.sty use or emulate the latest
have classicthesis.sty use or emulate the latest
LaTeX kernel via latexrelease (option: latest)
(thanks to Jörn Hees).
[REMOVED AS IT IS NOT AVAILABLE IN MANY
[REMOVED AS IT IS NOT AVAILABLE IN MANY
DISTRIBUTIONS, SEE ISSUE #107]
Changes in version 4.1 (August 2012)
o Working towards XeLaTeX support:
 "ifxetex" package for checking whether
XeTeX is in use (classicthesis.sty)
 Adjusted part, chapter, and tocEntry
 Adjusted part, chapter, and tocEntry
 Thanks to Joerg Weber for his ideas and code
 Option "pdfspacing" does not work for XeTeX
and is disabled when XeTeX is running
(maybe implement spacing with fontspec later)
o Load additional packages in order to
o Load additional packages in order to
reduce warnings (classicthesisconfig.tex)
 "textcomp" to fix warnings with missing font
 "textcomp" to fix warnings with missing font
shapes
 "scrhack" to fix warnings when using KOMA
with listings package
 "scrhack" to fix warnings when using KOMA
with listings package
o Replaced \mathrmcommand with \textrmcommand
(Chapter03.tex)
Changes in version 4.0 (December 2011)
o Due to lots of issues and complaints,
classicthesispreamble.sty is replaced by
o Due to lots of issues and complaints,
classicthesispreamble.sty is replaced by
classicthesisconfig.tex (which is cleaner,
nicer, better, etc. than before!)
o No perchapternumbering also for equations
o No perchapternumbering also for equations
(classicthesis.sty and Chapter03.tex)
o classicthesis.sty now also works without the
o classicthesis.sty now also works without the
KOMAclasses (scrbook, scrartcl, etc.):
 This affects the text body shape, where the
package "typearea" is always loaded in order
package "typearea" is always loaded in order
to use \areaset
 And affects the layout of footnotes where the
 And affects the layout of footnotes where the
package "footmisc" is loaded otherwise
(not 100\% identical lookandfeel but OK)
o Help for using spanish babel with classicthesis
o Help for using spanish babel with classicthesis
(classicthesisconfig.tex)
o Note about pdfsync issues with graffiti
o Note about pdfsync issues with graffiti
(Chapter01.tex)
o Minor cleanup of comments and duplicate lines
o Minor cleanup of comments and duplicate lines
(classicthesis.sty)
o Adjusted the colophon text (Colophon.tex)
o Increased space for labels in the LoF, LoT, LoL
o Included version information on the title page and
in the drafting and final version information
in the drafting and final version information
(classicthesis.sty and Titlepage.tex)
Changes in version 3.0 (June 2011)
o There have been some major changes in order to port
o There have been some major changes in order to port
classicthesis to LyX easily. See below for details.
Special thanks go to Ivo Pletikosi\'
c
for
all
his
Special thanks go to Ivo Pletikosi\'
c
for
all
his
hard
work
he
put
into
this
project
!
o
Changes
in
ClassicThesis
.
tex
:

Redundant
fleqn
removed
from
documentclass
options

Redundant
fleqn
removed
from
documentclass
options
(
will
be
set
by
amsmath
package
in
preamble
)

KOMA
adjustments
for
documentclass
:

KOMA
adjustments
for
documentclass
:
fontsize
=
11
pt
,
paper
=
14

Moved
language
options
into
documentclass
due
to
LyX
issues
with
babel
...
...
@@ 108,18 +108,18 @@ o Changes to classicthesispreamble.sty:

Now
contains
all
configuration
information
,
such
as
the
title
,
your
name
etc
.

This
package
now
also
loads
classicthesis
.
sty
,
change
the
options
classicthesis
to
be
loaded
with
here

Package
inputenc
now
loaded
with
latin9
option
the
options
classicthesis
to
be
loaded
with
here

Package
inputenc
now
loaded
with
latin9
option

Package
listings
now
also
loaded
here

Now
safer
package
loading
regarding
options
by
using
\
PassOptionsToPackage
command
extensively

Inserted
new
string
for
\
mySubtitle
o
Changes
in
Titlepage
.
tex
and
Titleback
.
tex
because
of
new
o
Changes
in
Titlepage
.
tex
and
Titleback
.
tex
because
of
new
string
\
mySubtitle
o
Changed
a
lot
of
the
documentation
,
e
.
g
.,
in
Chapter01
.
tex
Changes
in
version
2.9
(
January
2011
)
o
Fixed
onlytext
euler
font
for
MinionPro
font
(
in
o
Fixed
onlytext
euler
font
for
MinionPro
font
(
in
classicthesis
.
sty
)
o
Option
"listsseparated"
deprecated
,
because
it
led
to
some
strange
side

effects
(
in
classicthesis
.
sty
)
...
...
@@ 127,7 +127,7 @@ o Changed default font size to 11pt (in ClassicThesis.tex) and
adjusted
text
block
size
accordingly
(
in
classicthesis
.
sty
)
o
Fixed
bug
with
backward
compatibility
regarding
old
commands
\
myChapter
and
\
myPart
in
classicthesis
.
sty
o
New
option
"floatperchapter"
for
classicthesis
.
sty
,
removed
o
New
option
"floatperchapter"
for
classicthesis
.
sty
,
removed
all
code
for
that
from
classicthesis

ldpkg
.
sty
o
Removed
"nochapters"
option
from
classicthesis

ldpkg
.
sty
o
Removed
redundant
loading
of
listings
package
(
in
...
...
@@ 143,15 +143,15 @@ o Included backward compatibility regarding old commands
\
myChapter
and
\
myPart
in
classicthesis
.
sty
o
Fixed
drafting
issues
(
draft
information
not
shown
at
all
)
caused
by
wrong
code
for
listings
and
listsseparated
options
in
classicthesis
.
sty
in
classicthesis
.
sty
Changes
in
version
2.7
(
February
2010
,
cumulative
release
)
o
Removed
option
for
classicthesis

ldpkg
.
sty
:
nobackref
o
Removed
option
for
classicthesis

ldpkg
.
sty
:
nobackref
Introduced
instead
option
"backref"
for
consistency
which
works
the
other
way
(
no
backrefs
by
default
)
Changes
in
version
2.6.2
(
January
2010
,
released
as
beta
)
o
New
option
for
classicthesis

ldpkg
.
sty
:
nobackref
o
New
option
for
classicthesis

ldpkg
.
sty
:
nobackref
(
removes
links
to
cited
page
in
bibliography
)
o
Fixed
some
spacing
issues
for
LoF
,
LoT
,
LoL
with
option
"listsseparated"
(
in
classicthesis
.
sty
)
...
...
@@ 162,23 +162,23 @@ o Removed \myChapter and \myPart, you can now use the regular
(
thanks
to
Hinrich
Harms
for
this
)
o
Fixed
used
KOMA

options
:
numbers
=
noenddot
,
cleardoublepage
=
empty
(
in
ClassicThesis
.
tex
)
o
Included
hack
to
use
citations
in
float
environments
,
will
o
Included
hack
to
use
citations
in
float
environments
,
will
be
fixed
with
caption
package
version
3.2
(
in
classicthesis
.
sty
)
o
Included
some
font
and
text
area
fine

tuning
code
o
Included
some
font
and
text
area
fine

tuning
code
(
in
ClassicThesis
.
tex
)
o
Some
testing
with
Libertine
font
(
classicthesis

book
.
tex
)
o
Fixed
numbering
of
listings
used
in
different
chapters
(
in
ClassicThesis
.
tex
,
classicthesis
.
sty
,
classicthesis

ldpkg
.
sty
)
o
Spacing
between
listings
in
different
chapters
and
after
List
o
Spacing
between
listings
in
different
chapters
and
after
List
of
Listings
header
fixed
(
in
classicthesis
.
sty
)
o
Increased
\
newnumberwidth
to
sizeof
(
999
)
which
is
better
for
o
Increased
\
newnumberwidth
to
sizeof
(
999
)
which
is
better
for
documents
with
more
than
99
pages
(
in
classicthesis
.
sty
)
o
New
option
for
classicthesis
.
sty
:
manychapters
Changes
in
version
2.6
(
August
2009
)
o
Centered
the
title
page
with
the
addmargin
environment
(
thanks
to
Nicolas
Repp
for
the
hint
)
o
Fixed
header
for
page
two
of
Table
of
Contents
(
with
3
o
Fixed
header
for
page
two
of
Table
of
Contents
(
with
3
or
more
pages
)
(
in
Contents
.
tex
)
o
Added
numbering
of
\
subsubsection
(
in
Contents
.
tex
)
o
Added
correct
Table
of
Contents
entries
for
\
subsubsection
...
...
@@ 202,11 +202,11 @@ o Cumulative release, some minor cleanup and bugfixing
Changes
in
version
2.4
.{
1

3
}
(
February
and
April
2008
,
released
as
betas
)
o
Switched
back
to
"obsolete"
KOMA
options
due
to
o
Switched
back
to
"obsolete"
KOMA
options
due
to
compatibility
issues
on
some
installations
o
Increased
robustness
of
\
cauthor
command
in
o
Increased
robustness
of
\
cauthor
command
in
classicthesis

ldpk
.
sty
o
Spacing
fix
for
\
sectionmark
(
in
classicthesis
.
sty
)
o
Spacing
fix
for
\
sectionmark
(
in
classicthesis
.
sty
)
o
Made
Booleans
private
(
in
classicthesis
.
sty
)
o
Acronyms
header
for
long
acronym
lists
(
in
Contents
.
tex
)
o
Moved
"amsmath"
package
from
classicthesis
.
sty
to
...
...
@@ 218,22 +218,22 @@ o Fixed issue with contents headings (in classicthesis.sty
o
Thanks
to
Lorenzo
Changes
in
version
2.3
(
November
2007
)
o
Fixed
serious
bug
with
\
myChapter
command
(
using
plain
o
Fixed
serious
bug
with
\
myChapter
command
(
using
plain
LaTeX
)
o
Removed
hypcap
package
from
classicthesis

ldpkg
.
sty
and
placeins
package
from
classicthesis
.
sty
.
Put
both
into
ClassicThesis
.
tex
for
finer
end

user
control
o
Removed
obsolete
KOMA
options
from
ClassicThesis
.
tex
o
Option
"subfigure"
deprecated
,
replaced
by
"subfig"
(
in
o
Option
"subfigure"
deprecated
,
replaced
by
"subfig"
(
in
classicthesis
.
sty
)
o
Inserted
some
mechanisms
to
detect
whether
subfig
(
ure
)
o
Inserted
some
mechanisms
to
detect
whether
subfig
(
ure
)
package
was
loaded
or
not
(
in
classicthesis
.
sty
)
o
Inserted
some
mechanism
to
detect
whether
classicthesis
packackage
was
loaded
or
not
(
in
classicthesis

ldpkg
.
sty
)
o
Moved
"headlines"
code
block
a
bit
up
in
o
Moved
"headlines"
code
block
a
bit
up
in
classicthesis
.
sty
(
seemed
to
cause
problems
with
new
KOMA

Script
classes
)
o
Removed
accidental
"natbib"
from
classicthesis

ldpkg
.
sty
o
Removed
accidental
"natbib"
from
classicthesis

ldpkg
.
sty
o
Some
fine

tuning
in
(
Dirty
)
Titlepage
.
tex
o
Thanks
to
Lorenzo
and
Denis
! :)
...
...
@@ 242,20 +242,20 @@ o \myChapter and \myPart now take an optional argument
just
as
the
regular
\
part
and
\
chapter
commands
o
Did
some
minor
changes
to
classicthesis

book
.
tex
so
it
's a better example
o Inserted some \cleardoublepage before \myPart
o Inserted some \cleardoublepage before \myPart
occurences to avoid pdfbookmark problems
o Introduced some general typographic finetuning
(linespread, penalties, etc.)
o Did some finetuning of the \graffito command
Changes in version 2.1 (July 2007)
o Removed duplicate xcolor package call from
o Removed duplicate xcolor package call from
classicthesisldpkg.sty and shifed some color
definitions around
o Removed redefinition of \ttdefault
Changes in version 2.0 (June 2007, cumulative release)
o Better setup of the list of acronyms
o Better setup of the list of acronyms
(in classicthesisldpkg.sty)
o Using KOMA option footinclude in ClassicThesis.tex
(text block sizes are adjusted to this)
...
...
@@ 284,13 +284,13 @@ o Introduced new commands in classicthesisldpkg.sty to make
 \backrefnotcitedstring (ref is not cited)
 \backrefcitedsinglestring (ref is cited on one page)
 \backrefcitedmultistring (ref is cited on multiple pages)
o Removed ellipsis package from classicthesisldpkg.sty due to
o Removed ellipsis package from classicthesisldpkg.sty due to
some undesired results for some users
o Removed the following packages from classicthesisldpkg.sty as
o Removed the following packages from classicthesisldpkg.sty as
these seem to require changes to their options from most users:
inputenc, babel, natbib (now in ClassicThesis.tex)
o New option for classicthesisldpkg.sty: nochapters
Use the package with classes that do not have chapter divisions
Use the package with classes that do not have chapter divisions
Changes in version 1.5 (April 2007, not released separately)
o Fixed some bugs to use classicthesis.sty for article layout
...
...
@@ 315,13 +315,13 @@ o Some minor bug fixes
Changes in version 1.4 (January 2007)
o Replaced \lineheight with \baselineskip in classicthesis.sty
o Removed obsolete "usenames" option from xcolor package (classicthesis.sty)
o Now classicthesis.sty processes the global a5paper option and adjusts
o Now classicthesis.sty processes the global a5paper option and adjusts
the layout accordingly (experimental!)
Changes in version 1.3.1 (August 2006)
o Urgent bug concerning ToC spacing etc. fixed
Changes in version 1.3 (August 2006)
Changes in version 1.3 (August 2006)
o New option for classicthesis.sty: parts
Turn this on if you use Part divisions. It finetunes the ToC and
adds support for Part division via \myPart{} (cf. \myChapter{})
...
...
@@ 329,15 +329,15 @@ o New option for classicthesis.sty: parts
o New option for classicthesis.sty: eulermath
Uses the awesome Euler fonts for math (Palatino fonts are default).
o Added mparhack package to loadpackages.sty to get the graffiti right
o Added a hint to loadpackages.sty on how to typeset the List of
o Added a hint to loadpackages.sty on how to typeset the List of
Listings consistently with classicthesis
o Some minor finetuning of typographic details
o Collaboration with babel package improved (now easier to use
with other languages than English)
o Added appropriate textwidth values for 11pt Palatino and Minion
(See comments near \areaset in classicthesis.sty)
o Note: There is a problem with the case of math text in part,
chapter, and section titles and I have no clue how to fix this
o Note: There is a problem with the case of math text in part,
chapter, and section titles and I have no clue how to fix this
(either the case or the spacing breaks). So far, I chose the case. :(
Changes in version 1.2 (June 2006)
...
...
@@ 347,7 +347,7 @@ o New option for classicthesis.sty: nochapters
Allows
to
use
the
look

and

feel
with
classes
that
do
not
use
chapters
.
o
New
option
for
classicthesis
.
sty
:
beramono
Loads
Bera
Mono
as
typewriter
font
.
(
Default
=
no
typewriter
font
.)
o
Included
list
of
files
,
see
LISTOFFILES
.
o
Included
list
of
files
,
see
LISTOFFILES
.
Changes
in
version
1.1
(
May
2006
)
o
classicthesis
.
sty
now
stand

alone
and
usable
w
/
o
whole
bundle
!
...
...
Chapters/Chapter01.tex
View file @
b8836e93
...
...
@@ 2,7 +2,7 @@
\chapter
{
Introduction
}
\label
{
ch:introduction
}
% ************************************************
During the last decades, the area
\emph
{
satisfiability modulo
During the last decades, the area
of
\emph
{
satisfiability modulo
theories
}
(
\smt
)~
\cite
{
BSST09
}
has undergone steep development in
both theory and practice. Achieved advances of
\smt
solving opened new
research directions in program analysis and verification, where
\smt
...
...
@@ 15,13 +15,13 @@ also has the ability to provide its model. Modern \smt solvers support
wide range of different firstorder theories  for example theories
of integers, real numbers, floatingpoint numbers, arrays, strings,
inductively defined data types, bitvectors, and various combinations
and subtheories of these theories
. From the software analysis and0
verification point of view, a particularly
important of these theories
is the theory of bitvectors, which can be
used to describe properties
of computer programs, since programs
usually use datatypes of bounded
size instead of mathematical integers. Additionally, operations over
these bounded datatypes naturally corespond to
operations o
f
the
bitvector theory.
and subtheories of these theories
~
\cite
{
BFT15, ZZG13, RB16
}
. From the
software analysis and
verification point of view, a particularly
important of these theories
is the theory of bitvectors, which can be
used to describe properties
of computer programs, since programs
usually use datatypes of bounded size instead of mathematical
integers. Additionally,
operations o
ver
the
se bounded datatypes
naturally corespond to operations of the
bitvector theory.
The benefit of describing properties of programs by bitvector
formulas is twofold. Formulas in the bitvector theory allow to model
...
...
@@ 32,26 +32,28 @@ even if the multiplication is allowed.
Therefore, quantifierfree bitvector formulas are used in tools for
symbolic execution, bounded model checking, analysis of hardware
circuits, static analysis, or test generation. Most of the current
\smt
solvers for the quantifierfree bitvector formulas eagerly or
lazily translate the formula to the propositional logic
(
\emph
{
bitblasting
}
) and use an efficient
\sat
solver to decide its
satisfiability. Therefore, the efficiency of most of the bitvector
\smt
solvers is tightly connected to the efficiency of the
\sat
solvers. Plenty of solvers for the quantifierfree bitvector formulas
exist: for example Beaver~
\cite
{
Beaver
}
, Boolector~
\cite
{
Boolector
}
,
CVC4~
\cite
{
CVC4
}
, MathSAT5~
\cite
{
MathSAT
}
, OpenSMT~
\cite
{
OpenSMT
}
,
Sonolar~
\cite
{
Sonolar
}
, Spear~
\cite
{
Spear
}
, STP~
\cite
{
STP
}
,
UCLID~
\cite
{
LS04
}
, Yices~
\cite
{
Yices
}
, and Z3~
\cite
{
Z3
}
.
circuits, static analysis, or test generation~
\cite
{
CGPD08, CDE08,
CFM12
}
. Most of the current
\smt
solvers for the quantifierfree
bitvector formulas eagerly or lazily translate the formula to the
propositional logic (
\emph
{
bitblasting
}
) and use an efficient
\sat
solver to decide its satisfiability. Therefore, the efficiency of most
of the bitvector
\smt
solvers is tightly connected to the efficiency
of the
\sat
solvers. Plenty of solvers for the quantifierfree
bitvector formulas exist: Beaver~
\cite
{
Beaver
}
,
Boolector~
\cite
{
Boolector
}
, CVC4~
\cite
{
CVC4
}
, MathSAT5~
\cite
{
MathSAT
}
,
OpenSMT~
\cite
{
OpenSMT
}
, Sonolar~
\cite
{
Sonolar
}
, Spear~
\cite
{
Spear
}
,
STP~
\cite
{
STP
}
, UCLID~
\cite
{
LS04
}
, Yices~
\cite
{
Yices
}
, and
Z3~
\cite
{
Z3
}
.
In some cases, quantifierfree formulas are not succinct enough and
using quantification is necessary keep size of the formula
reasonable. Bitvector quantified formulas arise naturally for example
in applications that need to decide equality of two symbolically
represented states, or in applications that generate loop invariants,
ranking functions, or loop summaries. However, the current
\smt
solvers' support of quantified bitvector logic is much more modest 
only CVC4, Yices, and Z3 officially support quantifiers in bitvector
represented states~
\cite
{
BHB14
}
, or in applications that generate loop
invariants, ranking functions, or loop
summaries~
\cite
{
WHD13,KLW13
}
. However, the current
\smt
solvers'
support of quantified bitvector logic is much more modest  only
CVC4, Yices, and Z3 officially support quantifiers in bitvector
formulas. Recently, quantifiers have been also implemented in an
development version of Boolector~
\cite
{
BoolectorComp
}
. All of these
\smt
solvers solve quantified bitvector formulas by some variant of
...
...
Chapters/Chapter02.tex
View file @
b8836e93
...
...
@@ 760,16 +760,17 @@ its model $M$ and another call to the \QFBV solver is made to
determine whether
$
M
$
is also a~model of
$
\forall
x
_
1
, x
_
2
,
\dots
, x
_
n
\,
(
\psi
)
$
. This is achieved by asking
the solver whether the formula
$
\neg
\widehat
{
\psi
}$
is satisfiable,
where
$
\widehat
{
\psi
}$
is the formula
$
\psi
$
with uninterpreted
constants replaced by their corresponding values in
$
M
$
. If
$
\neg
\widehat
{
\psi
}$
is not satisfiable, then the structure
$
M
$
is
indeed a model of the formula
$
\forall
x
_
1
, x
_
2
,
\dots
, x
_
n
\,
(
\psi
)
$
,
therefore the entire formula is satisfiable and
$
M
$
is its model. If
$
\neg
\widehat
{
\psi
}$
is satisfiable, we get values
$
v
_
1
,
\dots
, v
_
n
$
such that
$
\neg\widehat
{
\psi
}
[
v
_
1
,
\dots
, v
_
n
]
$
holds. To rule out
$
M
$
as a model of the input formula, the instance
$
\psi
[
v
_
1
,
\dots
, v
_
n
]
$
of the quantified formula is added to the quantifierfree part,
i.e.~the formula
$
\varphi
$
is modified to
where
$
\widehat
{
\psi
}$
is the formula
$
\psi
$
after substituting values
of all variables except for
$
x
_
1
\ldots
x
_
n
$
and uninterpreted
functions replaced by their values in
$
M
$
. If
$
\neg
\widehat
{
\psi
}$
is
not satisfiable, then the structure
$
M
$
is indeed a model of the
formula
$
\forall
x
_
1
, x
_
2
,
\dots
, x
_
n
\,
(
\psi
)
$
, therefore the entire
formula is satisfiable and
$
M
$
is its model. If
$
\neg
\widehat
{
\psi
}$
is satisfiable, we get values
$
v
_
1
,
\dots
, v
_
n
$
such that
$
\neg\widehat
{
\psi
}
[
v
_
1
,
\dots
, v
_
n
]
$
holds. To rule out
$
M
$
as a
model of the input formula, the instance
$
\psi
[
v
_
1
,
\dots
, v
_
n
]
$
of
the quantified formula is added to the quantifierfree part, i.e.~the
formula
$
\varphi
$
is modified to
\[
\varphi
' ~
\equiv
~
\varphi
\wedge
\psi
[
v
_
1
,
\dots
, v
_
n
]
,
\]
...
...
Chapters/Chapter03.tex
View file @
b8836e93
...
...
@@ 57,9 +57,9 @@ the size of the formula. Dually, the existential quantification can be
distributed over disjunctions.
Moreover, universal quantification can distribute over disjunctions in
cases where the variable bound by the quantifier does not occur in one
cases where the variable bound by the quantifier does not occur
g
in one
of the disjuncts. This leads to the following rule and its dual
version, which is known as
\emph
{
miniscoping
}
:
version, which is known as
\emph
{
miniscoping
}
~
\cite
{
Har09
}
:
\[
\forall
x.
\,
(
\varphi
~
\vee
~
\psi
)
~~
\leadsto
~~
(
\forall
x .
\,
\varphi
)
~
\vee
~
\psi
,
...
...
@@ 139,8 +139,8 @@ unsatisfiability of an overapproximation implies unsatisfiability of
the input formula.
Q3B employs approximations similar to those used by the
\smt
solver
\uclid
. In
\uclid
, the quantifierfree input formula
is
underapproximated by representing each bitvector variable by the
\uclid
~
\cite
{
BKOSSB07
}
. In
\uclid
, the quantifierfree input formula
is
underapproximated by representing each bitvector variable by the
smaller number of bit variables than its original bitwidth. The
number of bits by which the bitvariable is represented is called the
\emph
{
effective bitwidth
}
. For reducing the effective bitwidth,
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment