diff options
Diffstat (limited to 'cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf')
5 files changed, 5661 insertions, 0 deletions
diff --git a/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/Makefile b/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/Makefile new file mode 100644 index 000000000..99046573a --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/Makefile @@ -0,0 +1,23 @@ +TEX = pdflatex -shell-escape -interaction=nonstopmode -file-line-error +PRE = $(TEX) -ini -job-name="preamble" "&pdflatex preamble.tex\dump" +BIB = bibtex + +all: cmsv4.pdf + +view : + open cmsv4.pdf + +cmsv4.pdf : cmsv4.tex cmsv4.bbl cmsv4.blg + $(TEX) cmsv4.tex + +cmsv4.bbl cmsv4.blg : cmsv4.bib cmsv4.aux + $(BIB) cmsv4 + +cmsv4.aux : cmsv4.tex + $(TEX) cmsv4.tex + +cmsv4.bib : cmsv4.tex + $(TEX) cmsv4.tex + +clean: + rm -f *.aux *.bbl *.out cmsv4.pdf *.log *.blg diff --git a/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/cmsv4.tex b/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/cmsv4.tex new file mode 100644 index 000000000..ec9b29d20 --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/cmsv4.tex @@ -0,0 +1,73 @@ +%\documentclass[runningheads]{llncs} +\documentclass[final]{ieee} + +\usepackage{microtype} %This gives MUCH better PDF results! +%\usepackage[active]{srcltx} %DVI search +\usepackage[cmex10]{amsmath} +\usepackage{amssymb} +\usepackage{fnbreak} %warn for split footnotes +\usepackage{url} +%\usepackage{qtree} %for drawing trees +%\usepackage{fancybox} % if we need rounded corners +%\usepackage{pict2e} % large circles can be drawn +%\usepackage{courier} %for using courier in texttt{} +%\usepackage{nth} %allows to \nth{4} to make 1st 2nd, etc. +%\usepackage{subfigure} %allows to have side-by-side figures +%\usepackage{booktabs} %nice tables +%\usepackage{multirow} %allow multiple cells with rows in tabular +\usepackage[utf8]{inputenc} % allows to write Faugere correctly +\usepackage[bookmarks=true, citecolor=black, linkcolor=black, colorlinks=true]{hyperref} +\hypersetup{ +pdfauthor = {Mate Soos}, +pdftitle = {CryptoMiniSat v4}, +pdfsubject = {SAT Competition 2013}, +pdfkeywords = {SAT Solver, DPLL}, +pdfcreator = {PdfLaTeX with hyperref package}, +pdfproducer = {PdfLaTex}} +%\usepackage{butterma} + +%\usepackage{pstricks} +\usepackage{graphicx,epsfig,xcolor} +\usepackage[algoruled, linesnumbered, lined]{algorithm2e} %algorithms + +\begin{document} +\title{CryptoMiniSat v4} +\author{Mate Soos\\Security Research Labs} + +\maketitle +\thispagestyle{empty} +\pagestyle{empty} + +\section{Introduction} +This paper presents the conflict-driven clause-learning SAT solver CryptoMiniSat v4 (\emph{cmsat4}). \emph{cmsat4} aims to be a modern SAT Solver that allows for multi-threaded in-processing techniques while still retaining a strong CDCL component. In this description only the features relative to \emph{forl}, the previous year's submission, are explained. Please refer to the previous years' description for details. + + +\subsection{Cleaner code} +The code has been significantly cleaned up. In particular, it has been refactored to use more descriptive names, smaller functions and uses C++11 constructs that aid in simplifying code. + +\subsection{Better data gathering} +More data is gathered into an SQL database that allows for interactive display of solving parameters. It also allows for later analysis of the solving, spotting e.g. that certain simplification steps take too long. Every simplification step is recorded and many important factors about clauses, clause cleaning, propagation and conflict analysis are dumped to the database. + +\subsection{Bounded variable addition} +As per \cite{DBLP:conf/hvc/MantheyHB12} +variables are added to simplify the formula. CryptoMiniSat allows for not only 1-literal diff as per the research paper, but also 2-literal diffs. In terms of the algorithm in the research paper this difference introduces almost no change, though makes the implementation somewhat more elaborate. + +\subsection{Tuned time-outs} +Thanks to the SQL-based query functionality, time-outs could be queried easily and checked. This allowed for fine-tuning of time-outs for weird problems. + +\subsection{Multi-threading} +An experimental multi-threading system has been added. It only exchanges unit and binary lemmas. The system works even in case of library usage: it cleanly aborts the other threads even if the other threads are solving subcomponents with subsolvers. + +\subsection{Better stability} +The API has been cleaned up and connected to a number of fuzzers, including e.g. a wrapper for python and a python-based test-suite. This allowed for more rigorious testing to be carried out. + +\section*{Acknowledgements} +The author would like to thank in no particular order Horst Samulowitz, Marius T. Lindauer, Martin Maurer, Martin Albrecht, Vegard Nossum, Valentin Mayer-Eichberger, George Katsirelos, Karsten Nohl, Luca Melette, Marijn Heule, Vijay Ganesh, Trevor Hansen and Robert Aston for their help. + +\bibliographystyle{splncs03} +\bibliography{sigproc} + +\vfill +\pagebreak + +\end{document} diff --git a/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/ieee.cls b/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/ieee.cls new file mode 100644 index 000000000..3c57bba5d --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/ieee.cls @@ -0,0 +1,1497 @@ +% Copyright 2014 IEEEE +% for terms of use see https://www.ieee.org/publications_standards/publications/rights/copyrightpolicy.html + +% ========================================================================= +% ------------------------------------------------------------------------- +% XX X +% X +% XX XXX XXX XXX XXX X XXXX +% X X X X X X X X X X X +% X XXXXX XXXXX XXXXX X X XXX +% X X X X XX X X X X +% XXX XXX XXX XXX XX XXX X XXXX +% ------------------------------------------------------------------------- +% ========================================================================= +% ieee.cls --- For formatting IEEE conference & journal papers +% --- Compiled by Gregory Plett, Sept 1997 +% +% This class was inspired by one first compiled by Gerry Murray and +% Silvano Balemi for LaTeX209. It was later updated for use with +% LaTeX2e, and some bugs were fixed, all by Istvan Kollar. Lastly, +% I have tried to make the class easier to use by paper authors. +% Significant new functionality has been added. Many routines are +% "borrowed" from other people's packages and modified extensively. +% When I rembered where I got the routines from, I gave the author +% credit. +% +% After I made many changes on my own, I found a version by Peter +% N"uchter, and tried to retain some amount of compatibility with his +% version. To be completely compatible with him, you may need to +% manually: +% \usepackage{rawfonts}\usepackage{oldlfont} +% \AtBeginDocument{\parindent1.0em} (?) +% +%=========================================================================== +% +% Usage: +% \documentclass[main-mode,sub-mode,misc-options]{ieee} +% \usepackage{your own packages} +% \begin{document} +% \bibliographystyle{IEEEbib} +% \title[short]{regular} +% \author[short]{full} +% \maketitle +% \begin{abstract}...\end{abstract} +% \begin{keywords}...\end{keywords} +% \section{...} +% \PARstart ... or \PARstartCal ... +% ... +% \begin{biography}[picname.ps]{Author's name}...\end{biography} +% \end{document} +% +% The document class options are: +% +% main-mode: One of the following is required. (draft is the default) +% draft: Double-spaced, single column with date/time stamp. +% submission: Double-spaced, suitable for submission for review. +% compressed: Same as "submission", only single spaced. +% final: Double-column, for assessing page-length and +% format of final version. +% +% sub-mode: +% techreport: This can modify "final" to produce a two-col +% technical report. +% internal: This can modify "submission", "compressed" or "final". +% It changes the header to notify the reader that +% this is a version of the manuscript to be used for +% internal review processes only, and not to be +% distributed. +% submitted: This can modify "compressed" or "final". It changes +% the header to notify the reader that this +% is a preprint and not to be distributed. +% inpress: This can modify "compressed" or "final". It changes the +% header to notify the reader that this paper has +% been accepted for publishing, but it is not yet to be +% distributed. +% reprint: This can modify "final". It changes the header +% to notify the reader where the paper is reprinted from. +% +% misc-options: +% narroweqnarray: Changes the spacing around the "=" sign in +% equation arrays to make it the same as in displayed math. +% inline: Compresses the horizontal spacing of inline math equations. +% notitlepage: No separate title page. (default) +% titlepage: Separate title page. +% anonymous: Omit all author information from main part of paper. +% Author info only prints on titlepage. +% 9pt,10pt,11pt,12pt: Choose the appropriate type size. You should +% not need to do this as the "correct" size is automatically +% chosen. However, if you want, you may use these to change +% the type size of the main text. "9pt" is a bit of a hack +% to retain backward-compatibility. +% invited: If the paper is an "invited" paper, then this option +% prints "(Invited Paper)" under the authors' names. +% +% For regular IEEE submissions, define the journal name as: +% \journal{IEEE Trans. Inst. Meas.} +% +% To specify the conference place and date: +% \confplacedate{Ottawa, Canada, May 19--21, 1997} +% +% Before \maketitle, define: +% \title{Title of paper} +% \author{Author1\member{Fellow}\authorinfo{Department of +% Electrical Engineering\\ Some University, Somewhere, CA 94305 +% USA} \and Author2\member{Senior Member}\authorinfo{Deptartment of +% Measurement and Instrument Eng., Another University, ...}} +% +% Note, the contents of \authorinfo tends to vary depending on if it is +% a conference or journal paper. The amount of manual changes are +% small, and must be done by a human anyway. The example given is for an +% IMTC conference. +% +% See also IEEEbib.bst and ieeefig.sty +% Also very useful for document preparation is the style file "endfloat", +% available on all CTAN TeX archives. +% +%=========================================================================== +% modified 14 October 2002: +% - fixed bibliography listing of [#] when # < 10 and number of +% references is greater than 9. Thanks for Janos Markus for finding +% this bug and suggesting a solution. +% modified 15 January 2000: +% - "fixed" narroweqnarray. Never implemented! Now it is... +% modified 12 January 2000: +% - modified so only first \title and \author commands are recognized. +% This allows LyX to have \title and \author with full syntax in +% header, but dummy \title and \author show up in GUI. +% - added "\date" so the \date command can change "submitted" and +% "draft" date headers. +% modified 11 January 2000: +% - added PARstartLyX and PARstartCalLyX for LyX compatibility +% - added biographyLyX +% modified 1 Dec 1997: +% - fixed first page in reprint mode to be same length as other pages +% - added "invited" misc-option +% modified 5 Sept 1997: +% - added the inpress, reprint and internal sub-modes +% - removed IMTC-conf and CDC-conf to separate files +% modified 1 Sept 1997: +% - included Babel package compatibility +% - removed paper title from header on first page of draft +% manuscript +% - removed the fixed option "letterpaper" to allow a4paper (etc) +% modified 1 Aug 1997: +% - included the CDC-conf option +%=========================================================================== +% ************************************************************************** +% ****** ****************************************** +% ***** LaTeX2e INITIALIZATION ***************************************** +% ****** ****************************************** +% ************************************************************************** +\typeout{Document Class `ieee' <Modified: 2000, Gregory L. Plett>.} +\NeedsTeXFormat{LaTeX2e}[1993/11/11] % Oldest acceptable version of LaTeX2e +\ProvidesClass{ieee}[2000/01/11] % Name of package provided, date +\def\i@@@cls{exists} + +% Initial Code & Declaration of Options +% ------------------------------------- +\newif\ifev@l \ev@lfalse % true if "final" mode. +\newif\ifsubm@t \subm@tfalse % true if "submission" mode. +\newif\ifdr@ft \dr@fttrue % true if "draft" mode. +\newif\ifc@mpress \c@mpressfalse % true if "compressed" mode. + +\newif\if@technote \@technotefalse % true if "technote" sub-mode. +\newif\ifintern@l \intern@lfalse % true if "internal" sub-mode. +\newif\ifprepr@nt \prepr@ntfalse % true if "preprint" sub-mode. +\newif\ifinpr@ss \inpr@ssfalse % true if "inpress" sub-mode. +\newif\ifrepr@nt \repr@ntfalse % true if "reprint" sub-mode. + +\newif\iftitlep@ge \titlep@gefalse % true if has own titlepage +\newif\if@non \@nonfalse % true if anonymous +\newif\ifixpt \ixptfalse % true if trying to do 9 pt +\newif\if@nvited \@nvitedfalse % true if an invited paper + +% Main options +% ------------ +\DeclareOption{draft}{\ev@lfalse\subm@tfalse\dr@fttrue% + \typeout{ieee: `Draft' mode selected.}} +\DeclareOption{submission}{\ev@lfalse\dr@ftfalse\subm@ttrue% + \typeout{ieee: `Submission' mode selected.}} +\DeclareOption{compressed}{\ev@lfalse\dr@ftfalse\subm@tfalse\c@mpresstrue% + \typeout{ieee: `Compressed' mode selected.}} +\DeclareOption{final}{\ev@ltrue\dr@ftfalse\subm@tfalse% + \typeout{ieee: `Final' mode selected.}} +\DeclareOption{evaluation}{\ev@ltrue\dr@ftfalse\subm@tfalse% + \typeout{ieee: `Final' mode selected.}} % synonym for final + +% Sub options +% ----------- +\DeclareOption{technote}{\@technotetrue% + \typeout{ieee: `Technote' sub-mode selected.}} +\DeclareOption{internal}{\intern@ltrue\prepr@ntfalse\inpr@ssfalse\repr@ntfalse% + \typeout{ieee: `Internal-Review' sub-mode selected.}} +\DeclareOption{submitted}{\intern@lfalse\prepr@nttrue\inpr@ssfalse\repr@ntfalse% + \typeout{ieee: `Submitted' sub-mode selected.}} +\DeclareOption{preprint}{\intern@lfalse\prepr@nttrue\inpr@ssfalse\repr@ntfalse% + \typeout{ieee: `Submitted' sub-mode selected.}} % synonym for submitted +\DeclareOption{inpress}{\intern@lfalse\prepr@ntfalse\inpr@sstrue\repr@ntfalse% + \typeout{ieee: `Inpress' sub-mode selected.}} +\DeclareOption{reprint}{\intern@lfalse\prepr@ntfalse\inpr@ssfalse\repr@nttrue% + \typeout{ieee: `Reprint' sub-mode selected.}} + +% Misc options +% ------------ + % regular or compressed "=" spacing in +\def\eqnarr@ysep{\arraycolsep} % eqnarray (this is the default) + % NOTE: we must use "def" and not "=" + % as arraycolsep not yet defined. +\DeclareOption{narroweqnarray}{\gdef\eqnarr@ysep{0.28em\relax}% + \typeout{ieee: Narrow equation arrays selected.}} +\DeclareOption{inline}{\everymath{\thinmuskip=2mu plus 1mu + \medmuskip=3mu plus 1mu minus 2mu + \thickmuskip=4mu plus 2mu\relax}% + \typeout{ieee: Narrower inline equations selected.}} +\DeclareOption{notitlepage}{\titlep@gefalse% + \typeout{ieee: No separate title page.}} +\DeclareOption{titlepage}{\titlep@getrue% + \typeout{ieee: Use separate title page.}} +\DeclareOption{anonymous}{\@nontrue\AtBeginDocument{\glpexclude{biography}} + \typeout{ieee: Omit author information from paper.}} +\DeclareOption{invited}{\@nvitedtrue% + \typeout{ieee: (Invited Paper).}} + +\DeclareOption{9pt}{\ixpttrue% + \typeout{ieee: Trying to emulate old `9pt' document class.}} + +\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}} + +% Execution of Options/Package Loading +% ------------------------------------ +\newlength\narrowcol +\newlength\parindentsave % recover parindent in blsone text + +\ProcessOptions +\ifev@l % if "final" mode... + \if@technote\ixpttrue\typeout{ieee: Trying to emulate old `9pt' + document class.}\fi% + \LoadClass[twoside,final,twocolumn,10pt]{article} +\else % if "draft"/"submission"/(compressed) mode... + \ifixpt + \LoadClass[oneside,final,onecolumn,10pt]{article} + \else + \LoadClass[oneside,final,onecolumn,12pt]{article} + \fi +\fi +\RequirePackage[final]{graphicx} +\RequirePackage{ifthen} + +% Re-Definitions of English words which must be done before +% the Babel package (optional) is loaded. +% --------------------------------------------------------- +\def\keywordsname{Index Terms} +\def\indexterms#1{\def\keywordsname{#1}} +\def\appendicesname{Appendices} +\def\figurename{Fig.} + +% ************************************************************************** +% ***** Check Sub-Options for Compatibility w/ Main-Options ************ +% ************************************************************************** +\if@technote\ifev@l\else\ClassError{ieee}{`technote' sub-mode may be + used only with the `final' ^^Jmain-mode. It may not be used + with either the `draft,' `submission,' or ^^J`compressed' + main-modes}{}\endinput\fi\fi +\ifintern@l\ifdr@ft\ClassError{ieee}{`internal' sub-mode may be + used only with the ^^J`submission,' `compressed,' or `final' main-modes. + It may not be used ^^Jwith the `draft' main-mode}{}\endinput\fi\fi +\ifprepr@nt\ifc@mpress\else\ifev@l\else\ClassError{ieee}{`submitted' + sub-mode may be used only with the ^^J`compressed' or `final' + main-modes. It may not be used with either the ^^J`draft' or + `submission' main-modes}{}\endinput\fi\fi\fi +\ifinpr@ss\ifc@mpress\else\ifev@l\else\ClassError{ieee}{`inpress' + sub-mode may be used only with the `compressed' ^^Jor `final' + main-modes. It may not be used with either the `draft' or + ^^J`submission' main-modes}{}\endinput\fi\fi\fi +\ifrepr@nt\ifev@l\else\ClassError{ieee}{`reprint' + sub-mode may be used only with the `final' ^^Jmain-mode. It may not be + used with either the `draft,' `submission,' or ^^J`compressed' + main-modes}{}\endinput\fi\fi + +% ************************************************************************** +% ***** Page Layout Definition ***************************************** +% ************************************************************************** +%% Layout definitions (mostly) common to all options. + +\hoffset 0in \voffset 0in +\headheight 12pt \headsep 7mm +\marginparsep 10pt \marginparwidth 20pt +\marginparpush 25pt +\columnsep 4mm +\parindent 1.0em +\lineskip 1pt +\normallineskip 1pt +\def\baselinestretch{1} + +\partopsep \z@ +\topsep 1.3ex +\parsep \z@ +\itemsep \z@ + +\setlength{\parindentsave}{\parindent} + +\ifev@l % if "evaluation" mode + % if camera-ready or A4paper ... + \ifdim\paperwidth<211mm + \oddsidemargin -11.4mm \evensidemargin -11.4mm + % for regular US Letter, not camera-ready + \else + \oddsidemargin -8.45mm \evensidemargin -8.45mm + \fi + \ifrepr@nt + \textheight 237.5mm % leave 6mm for cpyright on first page + \else + \textheight 243.5mm + \fi + \voffset -0.5in + \textwidth 182.0mm + \topmargin -12pt + \setlength{\narrowcol}{89mm} +\else % if "draft"/"submission" mode... + \ifc@mpress % and "compressed" + \oddsidemargin -0.25in \evensidemargin -0.25in + \textheight 9in \textwidth 7in + \topmargin -0.25in + \setlength{\narrowcol}{7in} + \else % and NOT "compressed" + \renewcommand\baselinestretch{1.8}\renewcommand{\arraystretch}{0.8} + \parindent=1.8\parindent + \oddsidemargin 0pt \evensidemargin 0pt + \headheight 12pt \headsep 0.375in + \topmargin 0pt + \textheight 8.5in \textwidth 6.5in + \marginparsep 0in \marginparwidth 0pt + \marginparpush 5pt + \setlength{\narrowcol}{6.5in} + \fi +\fi + +\def\normalstyle{\rmfamily} + +% ************************************************************************** +% ***** Font Definition ************************************************ +% ************************************************************************** +%% The 9-point option is being faked since it is not supported by the +%% article base class. + +%% Check if we have selected 9 points +\ifixpt +\typeout{-- This is a 9 point document} +\gdef\@ptsize{9} +\def\@normalsize{\@setsize\normalsize{10.7pt}\ixpt\@ixpt +\abovedisplayskip 1em plus2pt minus5pt\belowdisplayskip \abovedisplayskip +\abovedisplayshortskip \z@ plus3pt\belowdisplayshortskip .6em plus3pt minus3pt +\topsep \belowdisplayshortskip%!PN +} +\def\small{\@setsize\small{9.12pt}\viiipt\@viipt} +\def\footnotesize{\@setsize\footnotesize{8.15pt}\viipt\@vipt} +\def\scriptsize{\@setsize\scriptsize{8pt}\vipt\@vpt} +\def\tiny{\@setsize\tiny{5pt}\vpt\@vpt} +\def\large{\@setsize\large{12pt}\xpt\@xpt} +\def\Large{\@setsize\Large{14pt}\xiipt\@xiipt} +\def\LARGE{\@setsize\LARGE{18pt}\xivpt\@xivpt} +\def\huge{\@setsize\huge{22pt}\xviipt\@xviipt} +\def\Huge{\@setsize\Huge{25pt}\xxpt\@xxpt} +\fi +%% +%% Check if we have selected 10 points +\def\@tempa{0}\if\@ptsize\@tempa +\typeout{-- This is a 10 point document} +\def\@normalsize{\@setsize\normalsize{11.9pt}\xpt\@xpt +\abovedisplayskip 1em plus2pt minus5pt\belowdisplayskip \abovedisplayskip +\abovedisplayshortskip \z@ plus3pt\belowdisplayshortskip .6em plus3pt minus3pt +\topsep \belowdisplayshortskip%!PN +} +\def\small{\@setsize\small{9.2pt}\viiipt\@viiipt} +\def\footnotesize{\@setsize\footnotesize{8.8pt}\viiipt\@viiipt} +\def\scriptsize{\@setsize\scriptsize{8pt}\viipt\@viipt} +\def\tiny{\@setsize\tiny{6pt}\vpt\@vpt} +\def\normalsize{\@setsize\normalsize{11.9pt}\xpt\@xpt} +\def\large{\@setsize\large{14pt}\xiipt\@xiipt} +\def\Large{\@setsize\Large{18pt}\xivpt\@xivpt} +\def\LARGE{\@setsize\LARGE{22pt}\xviipt\@xviipt} +\def\huge{\@setsize\huge{22pt}\xxpt\@xxpt} +\def\Huge{\@setsize\Huge{28pt}\xxvpt\@xxvpt} +\fi +%% +%% Check if we have selected 11 points +\def\@tempa{1}\if\@ptsize\@tempa +\typeout{-- This is an 11 point document} +\def\@normalsize{\@setsize\normalsize{13.6pt}\xipt\@xipt +\abovedisplayskip 1em plus2pt minus5pt\belowdisplayskip \abovedisplayskip +\abovedisplayshortskip \z@ plus3pt\belowdisplayshortskip .6em plus3pt minus3pt +\topsep \belowdisplayshortskip%!PN +} +\def\small{\@setsize\small{12pt}\xpt\@xpt} +\def\footnotesize{\@setsize\footnotesize{11pt}\ixpt\@ixpt} +\def\scriptsize{\@setsize\scriptsize{9.5pt}\viiipt\@viiipt} +\def\tiny{\@setsize\tiny{7pt}\vipt\@vipt} +\def\normalsize{\@setsize\normalsize{13.6pt}\xipt\@xipt} +\def\large{\@setsize\large{14pt}\xiipt\@xiipt} +\def\Large{\@setsize\Large{18pt}\xivpt\@xivpt} +\def\LARGE{\@setsize\LARGE{22pt}\xviipt\@xviipt} +\def\huge{\@setsize\huge{25pt}\xxpt\@xxpt} +\def\Huge{\@setsize\Huge{30pt}\xxvpt\@xxvpt} +\fi +%% +%% Check if we have selected 12 points +\def\@tempa{2}\if\@ptsize\@tempa +\typeout{-- This is a 12 point document} +\def\@normalsize{\@setsize\normalsize{14pt}\xiipt\@xiipt +\abovedisplayskip 1em plus3pt minus6pt\belowdisplayskip \abovedisplayskip +\abovedisplayshortskip \z@ plus3pt\belowdisplayshortskip .6em plus4pt minus4pt +\topsep \belowdisplayshortskip%!PN +} +\def\small{\@setsize\small{11.4pt}\xpt\@xpt} +\def\footnotesize{\@setsize\footnotesize{10pt}\ixpt\@ixpt} +\def\scriptsize{\@setsize\scriptsize{9pt}\viiipt\@viiipt} +\def\tiny{\@setsize\tiny{8pt}\vipt\@vipt} +\def\normalsize{\@setsize\normalsize{14pt}\xiipt\@xiipt} +\def\large{\@setsize\large{18pt}\xivpt\@xivpt} +\def\Large{\@setsize\Large{22pt}\xviipt\@xviipt} +\def\LARGE{\@setsize\LARGE{25pt}\xxpt\@xxpt} +\def\huge{\@setsize\huge{30pt}\xxvpt\@xxvpt} +\let\Huge=\huge +\fi + +\AtBeginDocument{\normalsize\normalstyle\ps@headings\pagenumbering{arabic}} + +% ************************************************************************** +% ***** List Definition ************************************************ +% ************************************************************************** +%% Change aspect of lists with +%% 1) \itemindent, label indentation wrt to left list margin +%% 2) \leftmargini, the indentation of the whole list (on left, first level) +\ifev@l + \itemindent -1em + \leftmargini 2em + \leftmarginii 1em + \leftmarginiii 1.5em + \leftmarginiv 1.5em + \leftmarginv 1.0em + \leftmarginvi 1.0em +\else + \itemindent -1em + \leftmargini 3em + \leftmarginii 3em + \leftmarginiii 3em + \leftmarginiv 3em + \leftmarginv 3em + \leftmarginvi 3em +\fi +%\itemindent 2em % Alternative values: sometimes used.. +%\leftmargini 0em +\labelsep 5pt +\leftmargin\leftmargini +\labelwidth \z@ + +\def\@listI{\leftmargin\leftmargini} \@listI +\def\@listi{\leftmargin\leftmargini \topsep \z@ plus 1pt minus 1pt} +\def\@listii{\leftmargin\leftmarginii\labelwidth\leftmarginii + \advance\labelwidth-\labelsep \topsep \z@} +\def\@listiii{\leftmargin\leftmarginiii\labelwidth\leftmarginiii + \advance\labelwidth-\labelsep \topsep \z@} +\def\@listiv{\leftmargin\leftmarginiv\labelwidth\leftmarginiv + \advance\labelwidth-\labelsep \topsep \z@} +\def\@listv{\leftmargin\leftmarginv\labelwidth\leftmarginv + \advance\labelwidth-\labelsep \topsep \z@} +\def\@listvi{\leftmargin\leftmarginvi\labelwidth\leftmarginvi + \advance\labelwidth-\labelsep \topsep \z@} + +\def\labelenumi{\theenumi.} \def\theenumi{\arabic{enumi}} +\def\labelenumii{(\theenumii)} \def\theenumii{\alph{enumii}} +\def\labelenumiii{\theenumiii.} \def\theenumiii{\roman{enumiii}} +\def\labelenumiv{\theenumiv.} \def\theenumiv{\Alph{enumiv}} +\def\p@enumii{\theenumi} +\def\p@enumiii{\theenumi(\theenumii)} +\def\p@enumiv{\p@enumiii\theenumiii} + +\def\labelitemi{$\scriptstyle\bullet$} +\def\labelitemii{\bf --} +\def\labelitemiii{$\ast$} +\def\labelitemiv{$\cdot$} + +%% \itemindent is set to \z@ by list, so define new temporary variable +\newdimen\tmpitemindent +\def\verse{\let\\=\@centercr + \list{}{\itemsep\z@ \itemindent -1.5em \listparindent \itemindent + \rightmargin\leftmargin\advance\leftmargin 1.5em}\item[]} +\let\endverse\endlist +\def\quotation{\list{}{\listparindent 1.5em \itemindent\listparindent + \rightmargin\leftmargin \parsep 0pt plus 1pt}\item[]} +\let\endquotation=\endlist +\def\quote{\list{}{\rightmargin\leftmargin}\item[]} +\let\endquote=\endlist +\def\@mklab#1{#1} +\def\description{\tmpitemindent\itemindent\list{}{\itemindent\tmpitemindent + \labelwidth\z@\def\makelabel##1{\hspace\labelsep\emph{##1}}}} +\def\enddescription{\endlist\par} +\def\enumerate{\tmpitemindent\itemindent\ifnum \@enumdepth >3 \@toodeep\else + \advance\@enumdepth \@ne \edef\@enumctr{enum\romannumeral\the\@enumdepth}% + \list{\csname label\@enumctr\endcsname}{\itemindent\tmpitemindent + \usecounter{\@enumctr}\def\makelabel##1{\hspace\labelsep\hfil{##1}}}\fi} +\def\endenumerate{\endlist\par} +\def\itemize{\tmpitemindent\itemindent\ifnum \@itemdepth >3 \@toodeep\else + \advance\@itemdepth\@ne + \edef\@itemitem{labelitem\romannumeral\the\@itemdepth}% + \list{\csname\@itemitem\endcsname}{\itemindent\tmpitemindent + \def\makelabel##1{\hspace\labelsep\hfil\emph{##1}}}\fi} +\def\enditemize{\endlist\par} + +\newif\if@restonecol +\def\titlepage{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn + \else \newpage \fi \thispagestyle{coverpagestyle}\c@page\z@} +\def\endtitlepage{\if@restonecol\twocolumn \else \newpage \fi% +\if@twoside\mbox{}\thispagestyle{coverpagestyle}\c@page\z@\cleardoublepage\fi} + +\arraycolsep 5pt +\tabcolsep 6pt +\arrayrulewidth .4pt +\doublerulesep 2pt +\tabbingsep\labelsep + +% ************************************************************************** +% ***** Footnote Definition ******************************************** +% ************************************************************************** +\skip\footins 10pt plus 5pt minus 2pt +\footnotesep 7pt +\footskip 6mm +\skip\@mpfootins = \skip\footins +\fboxsep = 3pt \fboxrule = .4pt +\long\def\@makefntext#1{\parindent .8em\indent$^{\@thefnmark}$#1} +\def\footnoterule{} + +% Reset baselinestretch within footnotes. +% Originally stolen from Stanford University thesis style. +% -------------------------------------------------------- +\long\def\@footnotetext#1{\insert\footins{\blsone% + \footnotesize\interlinepenalty\interfootnotelinepenalty + \splittopskip\footnotesep + \splitmaxdepth \dp\strutbox \floatingpenalty \@MM + \hsize\columnwidth \@parboxrestore + \edef\@currentlabel{\csname p@footnote\endcsname\@thefnmark}\@makefntext + \let\par\\ + {\rule{\z@}{\footnotesep}\ignorespaces + #1\strut}}} + +% ************************************************************************** +% ***** Keep track of Sections ***************************************** +% ************************************************************************** +\if@technote + \setcounter{secnumdepth}{3} +\else + \setcounter{secnumdepth}{4} +\fi + +\def\thesection{\@Roman\c@section} +\def\thesubsection{\Alph{subsection}} +\def\thesubsubsection{\thesubsection.\arabic{subsubsection}} +\def\thesubsubsectiondis{\Alph{subsection}.\arabic{subsubsection}} +\def\theparagraph{\thesubsubsection.\alph{paragraph}} +\def\theparagraphdis{\thesubsubsectiondis.\alph{paragraph}} + +\def\theequation{\arabic{equation}} + +% ************************************************************************** +% ***** Table of Contents, List of Figures/Tables Definitions ********** +% ************************************************************************** +\def\@pnumwidth{1.55em} +\def\@tocrmarg {2.55em} +\def\@dotsep{4.5} +\setcounter{tocdepth}{3} + +\def\tableofcontents{\section*{\contentsname}\@starttoc{toc}} +\def\l@section#1#2{\addpenalty{\@secpenalty} \addvspace{1.0em plus 1pt} + \@tempdima 1.8em \begingroup \parindent \z@ \rightskip \@pnumwidth + \parfillskip-\@pnumwidth \bf\leavevmode #1\hfil\hbox to\@pnumwidth{\hss #2} + \par \endgroup} +\def\l@subsection{\@dottedtocline{2}{1.5em}{2.3em}} +\def\l@subsubsection{\@dottedtocline{3}{3.8em}{3.2em}} +\def\listoffigures{\section*{\listfigurename}\@starttoc{lof}} +\def\l@figure{\@dottedtocline{1}{1em}{1.8em}} +\def\listoftables{\section*{\listtablename}\@starttoc{lot}} +\let\l@table\l@figure + +% ************************************************************************** +% ***** Float Definitions ********************************************** +% ************************************************************************** +%% Normal Floats %% Double Column Floats +\floatsep 12pt plus 2pt minus 2pt \dblfloatsep 12pt plus 2pt minus 2pt +\textfloatsep 20pt plus 2pt minus 4pt \dbltextfloatsep 20pt plus 2pt minus 4pt +%\@maxsep 20pt \@dblmaxsep 20pt %!PN +\@fptop 0pt plus 1fil \@dblfptop 0pt plus 1fil +\@fpsep 8pt plus 2fil \@dblfpsep 8pt plus 2fil +\@fpbot 0pt plus 1fil \@dblfpbot 0pt plus 1fil +\def\topfraction{1.0} \def\dbltopfraction{1.0} +\def\floatpagefraction{0.8} \def\dblfloatpagefraction{0.8} +\setcounter{topnumber}{2} \setcounter{dbltopnumber}{4} +% +\intextsep 12pt plus 2pt minus 2pt +\setcounter{bottomnumber}{2} +\def\bottomfraction{.4} +\setcounter{totalnumber}{4} +\def\textfraction{.2} + +% Reset baselinestretch within floats. +% Originally stolen from Stanford University thesis style. +% -------------------------------------------------------- +\def\@xfloat#1[#2]{\ifhmode \@bsphack\@floatpenalty -\@Mii\else + \@floatpenalty-\@Miii\fi\def\@captype{#1}\ifinner + \@parmoderr\@floatpenalty\z@ + \else\@next\@currbox\@freelist{\@tempcnta\csname ftype@#1\endcsname + \multiply\@tempcnta\@xxxii\advance\@tempcnta\sixt@@n + \@tfor \@tempa :=#2\do + {\if\@tempa h\advance\@tempcnta \@ne\fi + \if\@tempa t\advance\@tempcnta \tw@\fi + \if\@tempa b\advance\@tempcnta 4\relax\fi + \if\@tempa p\advance\@tempcnta 8\relax\fi + }\global\count\@currbox\@tempcnta}\@fltovf\fi + \global\setbox\@currbox\vbox\bgroup + \def\baselinestretch{1}\small\normalsize + \hsize\columnwidth \@parboxrestore} + +% ************************************************************************** +% ***** Caption Definition ********************************************* +% ************************************************************************** +% some journals do not have centered captions for figures. +\newif\ifc@ptionleft \c@ptionlefttrue +\def\leftfigcaptions{\c@ptionlefttrue} +\def\centerfigcaptions{\c@ptionleftfalse} + +\long\def\caption{\refstepcounter\@captype \@dblarg{\@caption\@captype}} + +\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname ext@#1\endcsname}{#1}{% + \protect\numberline{\csname the#1\endcsname}{\ignorespaces #2}} + \begingroup \@parboxrestore \normalsize + \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}{#1}\par + \endgroup} + +\def\tablestring{table} +\def\figurestring{figure} + +% changed by GLP to allow table captions to be set to a specific maximum +% width "\captionwidth", if defined. +\newlength{\captionindent} +\long\def\@makecaption#1#2#3{ +\ifx\figurestring#3 + \vskip 5pt + \setbox\@tempboxa\hbox{\small #1.~ #2} + \ifdim \wd\@tempboxa >\hsize + \setbox\@tempboxa\hbox{\small #1.~ } + %\setlength\captionindent{\wd\@tempboxa} \divide\captionindent by 2 + %\parbox[t]{\hsize}{\small \hangindent \captionindent \hangafter=1% + \parbox[t]{\hsize}{\small + \unhbox\@tempboxa#2} + \else \hbox + to\hsize{\small\ifc@ptionleft\else\hfil\fi\box\@tempboxa\hfil} + \fi +\else + \begin{center} + \ifx\captionwidth\undefined {\small #1}\\{\small\scshape #2} + \else + \begin{minipage}{\captionwidth} + \begin{center}{\small #1}\\{\small\scshape #2}\end{center} + \end{minipage} + \fi + \end{center}\vskip 4pt +\fi} + +\def\thefigure{\@arabic\c@figure} +\def\fps@figure{tbp} +\def\ftype@figure{1} +\def\ext@figure{lof} +\def\fnum@figure{\figurename\ \thefigure} +%\def\figure{\@float{figure}} % GLP +%\let\endfigure\end@float +\@namedef{figure*}{\@dblfloat{figure}} +\@namedef{endfigure*}{\end@dblfloat} + +\def\thetable{\@Roman\c@table} +\def\fps@table{tbp} +\def\ftype@table{2} +\def\ext@table{lot} +\def\fnum@table{TABLE~\thetable} +\def\table{\@float{table}} +\let\endtable\end@float +\@namedef{table*}{\@dblfloat{table}} +\@namedef{endtable*}{\end@dblfloat} + +% ************************************************************************** +% ***** Header/Footer Definition *************************************** +% ************************************************************************** +% compute the time in hours and minutes; make new vars \timehh and \timemm +\newcount\timehh\newcount\timemm\timehh=\time\divide\timehh by 60 +\timemm=\time\count255=\timehh\multiply\count255 by-60 +\advance\timemm by \count255 +\ifnum\timehh=12\def\apm{pm}\else +\ifnum\timehh>12\def\apm{pm}\advance\timehh by-12\else +\def\apm{am}\fi\fi +\def\t@me{\number\timehh\,:\,\ifnum\timemm<10 0\fi\number\timemm\,\apm} + +% default definitions +% ------------------- +\def\theevenhe@d{\footnotesize\thepage \hfil \leftmark\hbox{}} +\def\theoddhe@d{\hbox{}\footnotesize\rightmark \hfil \thepage} +\def\theevenf@@t{} +\def\theoddf@@t{} + +\def\theeventphe@d{\footnotesize\thepage \hfil \hbox{}} +\def\theoddtphe@d{\hbox{}\footnotesize \hfil \thepage} +\def\theeventpf@@t{} +\def\theoddtpf@@t{} + +\def\theevencphe@d{} +\def\theoddcphe@d{} +\def\theevencpf@@t{} +\def\theoddcpf@@t{} + +\def\internalmsg{Preliminary version for evaluation: Please do not + circulate without the permission of the author(s)} +\def\submittedmsg{SUBMITTED FOR PUBLICATION TO:} +\def\acceptedmsg{ACCEPTED FOR PUBLICATION:} +\def\inpressmsg{(IN PRESS)} +\def\reprintmsg{REPRINTED FROM:} + +% default cover page style (optional cover page) +% ---------------------------------------------- +\def\ps@coverpagestyle{ + \def\@oddhead{\theoddcphe@d} \def\@evenhead{\theevencphe@d} + \def\@oddfoot{\theoddcpf@@t} \def\@evenfoot{\theevencpf@@t} +} + +% default title page style (first page of paper) +% ---------------------------------------------- +\def\ps@titlepagestyle{ + \def\@oddhead{\theoddtphe@d} \def\@evenhead{\theeventphe@d} + \def\@oddfoot{\theoddtpf@@t} \def\@evenfoot{\theeventpf@@t} +} + +% default regular page style +% -------------------------- +\if@twoside + \def\ps@headings{ + \def\@oddhead{\theoddhe@d} + \def\@evenhead{\theevenhe@d} + \def\@oddfoot{\theoddf@@t} \def\@evenfoot{\theevenf@@t} + } +\else + \def\ps@headings{ + \def\@oddhead{\theoddhe@d} + \def\@oddfoot{\theoddf@@t} + \def\@evenhead{} \def\@evenfoot{} + } +\fi + +% For draft mode (no sub-modes allowed) +% ------------------------------------- +\ifdr@ft + \def\leftmark{\sh@rttitle}\let\rightmark\leftmark + \def\theoddf@@t{\footnotesize\today---\t@me\hfil DRAFT} + \def\theevenf@@t{\footnotesize DRAFT\hfil\today---\t@me} + \def\theoddtpf@@t{\footnotesize\today---\t@me\hfil DRAFT} + \def\theeventpf@@t{\footnotesize DRAFT\hfil\today---\t@me} +\fi + +% For submission mode (default plus internal sub-modes allowed) +% ------------------------------------------------------------- +\ifsubm@t + \def\leftmark{\sh@rttitle}\def\rightmark{\titl@line} + \ifintern@l + \def\theeventphe@d{\footnotesize\thepage \hfil \rightmark\hbox{}} + \def\theoddtphe@d{\hbox{}\footnotesize\rightmark \hfil \thepage} + \def\rightmark{\vbox to 0pt{\vss\hbox{\internalmsg} \hbox{\sh@rttitle}}} + \def\leftmark{\vbox to 0pt{\vss\hbox{\internalmsg} + \hbox{\phantom{\internalmsg}\llap{\sh@rttitle}}}} + \else % put date on first page. + \edef\TODAY{\uppercase{\today}} + \def\theeventphe@d{\footnotesize\thepage \hfil \submittedmsg\ + \@journal\@titletext, \TODAY} + \def\theoddtphe@d{\footnotesize\submittedmsg\ + \@journal\@titletext, \TODAY\hfil \thepage} + \def\theevencphe@d{\footnotesize\hbox{} \hfil \submittedmsg\ + \@journal\@titletext, \TODAY} + \def\theoddcphe@d{\footnotesize\submittedmsg\ + \@journal\@titletext, \TODAY\hfil \hbox{}} + \fi +\fi + +% For compressed mode (default, internal, submitted and +% inpress sub-modes allowed) +% ----------------------------------------------------- +\ifc@mpress + \def\leftmark{\sh@rttitle}\def\rightmark{\titl@line} + \ifintern@l + \def\theeventphe@d{\footnotesize\thepage \hfil \rightmark\hbox{}} + \def\theoddtphe@d{\hbox{}\footnotesize\rightmark \hfil \thepage} + \def\rightmark{\vbox to 0pt{\vss\hbox{\internalmsg} \hbox{\sh@rttitle}}} + \def\leftmark{\vbox to 0pt{\vss\hbox{\internalmsg} + \hbox{\phantom{\internalmsg}\llap{\sh@rttitle}}}} + \fi + \ifprepr@nt + \edef\TODAY{\uppercase{\today}} + \def\theeventphe@d{\footnotesize\thepage \hfil \submittedmsg\ + \@journal\@titletext, \TODAY} + \def\theoddtphe@d{\footnotesize\submittedmsg\ + \@journal\@titletext, \TODAY\hfil \thepage} + \def\theevencphe@d{\footnotesize\hbox{} \hfil \submittedmsg\ + \@journal\@titletext, \TODAY} + \def\theoddcphe@d{\footnotesize\submittedmsg\ + \@journal\@titletext, \TODAY\hfil \hbox{}} + \fi + \ifinpr@ss + \def\leftmark{\acceptedmsg\ \@journal\@titletext, \inpressmsg} + \def\theeventphe@d{\footnotesize\thepage \hfil \leftmark\hbox{}} + \def\theoddtphe@d{\hbox{}\footnotesize\leftmark \hfil \thepage} + \fi +\fi + +% For final (evaluate) mode (default, techreport, internal, +% submitted, inpress and reprint sub-modes allowed) +% --------------------------------------------------------- +\ifev@l + \edef\TODAY{\uppercase{\today}} + \def\leftmark{\@journal\@titletext}\def\rightmark{\titl@line} + \def\theeventphe@d{\footnotesize\thepage \hfil \leftmark\hbox{}} + \def\theoddtphe@d{\hbox{}\footnotesize\leftmark \hfil \thepage} + \if@technote % make header a little bigger + \def\theevenhe@d{\small\thepage \hfil \leftmark\hbox{}} + \def\theoddhe@d{\hbox{}\small\rightmark \hfil \thepage} + \def\theeventphe@d{\small\thepage \hfil \leftmark\hbox{}} + \def\theoddtphe@d{\hbox{}\small\leftmark \hfil \thepage} + \fi + \ifintern@l + \def\theeventphe@d{\footnotesize\thepage \hfil \rightmark\hbox{}} + \def\theoddtphe@d{\hbox{}\footnotesize\rightmark \hfil \thepage} + \def\rightmark{\vbox to 0pt{\vss\hbox{\internalmsg} \hbox{\sh@rttitle}}} + \def\leftmark{\vbox to 0pt{\vss\hbox{\internalmsg} + \hbox{\phantom{\internalmsg}\llap{\sh@rttitle}}}} + \fi + \ifprepr@nt + \def\leftmark{\submittedmsg\ \@journal\@titletext, \TODAY} + \fi + \ifinpr@ss + \def\leftmark{\acceptedmsg\ \@journal\@titletext, \inpressmsg} + \fi + \ifrepr@nt + % reset page size on second and following pages b/c no copyright info + \let\oldshipout\shipout + \gdef\shipout{\global\textheight 243.5mm\oldshipout} + \def\theeventpf@@t{\footnotesize\hfil\@ieeecopyright\hfil} + \def\theoddtpf@@t{\footnotesize\hfil\@ieeecopyright\hfil} + \def\leftmark{\reprintmsg\ \@journal\@titletext} + \fi +\fi + +%% Defines the command for putting the header. footernote{TEXT} is the same +%% as markboth{TEXT}{TEXT}. Here for compatibility with other style files. +\def\markboth#1#2{\def\leftmark{#1}\def\rightmark{#2}} +\def\footernote#1{\markboth{#1}{#1}} + +% ************************************************************************** +% ***** Citation/Bibliography Definitions ****************************** +% ************************************************************************** +%% separate citations with "], [" +\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi +\def\@citea{}\@cite{\@for\@citeb:=#2\do {\@citea\def\@citea{], +[}\@ifundefined {b@\@citeb}{{\bf ?}\@warning {Citation `\@citeb' on +page \thepage \space undefined}}% +{\csname b@\@citeb\endcsname}}}{#1}} + +\def\@cite#1#2{[{#1\if@tempswa, #2\fi}]} + +%% Allow short (name-less) citations, when used in conjunction with a +%% bibliography style that creates labels like \citename{<names>, }<year> +\let\@internalcite\cite +\def\cite{\def\citename##1{##1}\@internalcite} +\def\shortcite{\def\citename##1{}\@internalcite} +\def\@biblabel#1{\def\citename##1{##1}[#1]\hfill} + +\def\thebibliography#1{\section*{\refname}\footnotesize\list + {\hss[\arabic{enumi}]}{\settowidth\labelwidth{[#1]}\leftmargin\labelwidth + \advance\leftmargin\labelsep \itemsep 0pt plus .5pt + \usecounter{enumi}} + \def\newblock{\hskip .11em plus .33em minus .07em} + \sloppy\clubpenalty4000\widowpenalty4000 + \sfcode`\.=1000\relax + \ifev@l\else\normalsize\fi %added by GLP +} +\let\endthebibliography=\endlist + +% ************************************************************************** +% ***** Appendix/Appendices Definitions ******************************** +% ************************************************************************** +\newcounter{numappendices}\setcounter{numappendices}{0} +\newif\ifappendix \appendixfalse +%% appendix command for one single appendix +\def\appendix{\par + \appendixtrue + \typeout{appendices: \arabic{numappendices}} + \setcounter{section}{0}\setcounter{subsection}{0} + \gdef\thesection{\Alph{section}} + \ifnum \value{numappendices}>1 + \section*{\appendicesname} + \else + \section*{\appendixname} + \fi + \setcounter{numappendices}{0} +} +%% appendices command for multiple appendicies +\def\appendices{\par + \appendixtrue + \typeout{appendices: \arabic{numappendices}} + \setcounter{section}{0}\setcounter{subsection}{0} + \gdef\thesection{\Alph{section}} \section*{\appendicesname} + \setcounter{numappendices}{0} +} +\AtEndDocument{\if@filesw\immediate\write\@auxout{\string\setcounter{numappendices}{\arabic{numappendices}}}\fi} + +% ************************************************************************** +% ***** Title Definitions ********************************************** +% ************************************************************************** +\def\titl@line{\sh@rttitle} %for the header at the top of the page. + +\def\@title{\typeout{ieee: Warning! No \noexpand\title given!}} +\def\title{\@ifnextchar [{\titlea}{\titleb}}%] + +\def\set@title#1{\gdef\@title{#1}\global\def\set@title##1{}} +\def\setsh@rttitle#1{\gdef\sh@rttitle{#1}\global\def\setsh@rttitle##1{}} +\def\titlea[#1]#2{\set@title{#2}\setsh@rttitle{\uppercase{#1}}} +\def\titleb#1{\set@title{#1}\setsh@rttitle{\uppercase{#1}}} + +\def\authorinfo#1{\let\\\relax\thanks{#1}} + +\ifev@l + \if@technote + \def\member#1{} + \else + \def\member#1{, \emph{#1, IEEE}} + \fi +\else + \def\member#1{} +\fi + +\def\and{\unskip% % \begin{tabular} +\end{tabular}% +\hskip 0pt plus 0.1pt% +\begin{tabular}[t]{@{}c@{}}\ }% + +\def\@author{\typeout{ieee: Warning! No \noexpand\author given!}} +\def\author{\@ifnextchar [{\authora}{\authorb}}%] +\def\set@author#1{\gdef\@author{#1}\global\def\set@author##1{}} +\def\settitl@line#1{\gdef\titl@line{#1}\global\def\settitl@line##1{}} +\def\authora[#1]#2{\set@author{#2}\if@non\else\settitl@line{#1: \sh@rttitle}\fi} +\def\authorb#1{\set@author{#1}} + +\def\date#1{\def\today{#1}\edef\TODAY{\uppercase{\today}}} + +\long\def\maketitle{% + \begingroup + \let\@thanks\@empty + \renewcommand\thefootnote{} % the \thanks{} mark type is empty + \iftitlep@ge\begin{titlepage}\@maketitlepage\@thanks\end{titlepage}% + \let\@thanks\@empty\fi + \thispagestyle{titlepagestyle} + \if@twocolumn + \if@technote + %\if@twoside\newpage\cleardoublepage\else\newpage\fi% + \newpage\global\@topnum\z@ + \ifrepr@nt + \ifx\@loginfo\undefined\typeout{ieee: Warning! No \noexpand\loginfo + given!}\else\let\\\relax\thanks{\@loginfo}\fi% + \fi + \@maketitle + \else + \ifnum \col@number=\@ne + \ifrepr@nt + \ifx\@loginfo\undefined\typeout{ieee: Warning! No \noexpand\loginfo + given!}\else\let\\\relax\thanks{\@loginfo}\fi% + \fi + \@maketitle + \else \twocolumn[% + \ifrepr@nt% + \ifx\@loginfo\undefined\typeout{ieee: Warning! No \noexpand\loginfo% + given!}\else\let\\\relax\thanks{\@loginfo}\fi% + \fi% + \@maketitle]% + \fi + \fi + \else + \newpage + \global\@topnum\z@ % Prevents figures from going at top of page. + \ifrepr@nt + \ifx\@loginfo\undefined\typeout{ieee: Warning! No \noexpand\loginfo + given!}\else\let\\\relax\thanks{\@loginfo}\fi + \fi + \@maketitle + \fi + \thispagestyle{titlepagestyle}% + \@thanks + \endgroup + \setcounter{footnote}{0}% + \global\let\thanks\relax \global\let\maketitle\relax + \global\let\@maketitle\relax \global\let\@thanks\@empty + \global\let\@author\@empty \global\let\@date\@empty + \global\let\@title\@empty \global\let\title\relax + \global\let\author\relax \global\let\date\relax + \global\let\and\relax +} + +\long\def\@maketitle{\unskip\newpage% + \begin{center}\blsone + \let \footnote \thanks + \if@technote + {\bfseries\@title\par}\if@non\else\vskip 1.3em{\lineskip .5em + \noindent\begin{tabular}[t]{@{}c@{}}\@author\end{tabular}}\fi\par + \else\unskip + \noindent{\Huge\@title\par}% + \if@non\else\vskip1.0em% + \noindent{\large\lineskip .5em% + \begin{tabular}[t]{@{}c@{}}\@author\end{tabular}}% + \fi\par% + \if@nvited\vskip1.0em\noindent\emph{\large(Invited Paper)}\par\fi + \fi + \ifrepr@nt + \ifx\@lognumber\undefined\typeout{ieee: Warning! No + \noexpand\pubitemident or \noexpand\lognumber + given!}\else\thanks{\@lognumber}\fi% + \fi + \end{center}\par\vskip 0.5em}% + +\long\def\@maketitlepage{\newpage% + \mbox{}\vfil + \begin{center}\blsone + \let \footnote \thanks + \if@technote + {\bfseries\@title\par}\vskip 1.3em{\lineskip .5em + \noindent\begin{tabular}[t]{@{}c@{}}\@author\end{tabular}\par} + \else + \vskip0.2em{\Huge\@title\par}\vskip1.0em% + \iftitlep@ge\vfil\fi + \noindent{\large\lineskip .5em% + \begin{tabular}[t]{@{}c@{}}\@author\end{tabular}\par}% + \fi + \end{center}\par\vfil\mbox{}} + +\def\@journal{\typeout{ieee: Warning! No \noexpand\journal given!}} +\def\journal#1{\def\@journal{\uppercase{#1}}} + +\def\@ieeecopyright{\typeout{ieee: Warning! No \noexpand\ieeecopyright given!}} +\def\ieeecopyright#1{\def\@ieeecopyright{#1}} + +\def\lognumber#1{\def\@lognumber{IEEE Log Number #1.}} +\def\pubitemident#1{\def\@lognumber{Publisher Item Identifier #1.}} +\long\def\loginfo#1{\long\def\@loginfo{\hbox{\vrule height 3ex width \z@}#1}} + +\def\sh@rttitle{} +\def\@titletext{} +\def\titletext#1{\def\@titletext{#1}} + +\def\firstpage#1{\setcounter{page}{#1}} + +% ************************************************************************** +% ***** Abstract Definition ******************************************** +% ************************************************************************** +\def\abstract{% + \if@twocolumn + \small\bfseries{\itshape\abstractname\/---}% + \else + \begin{center}\vspace{-0.8em}\small\bf\abstractname\end{center} + \quotation\small + \fi\ignorespaces} +\def\endabstract{\vspace{0.6em}\par\if@twocolumn\else\endquotation\fi + \normalsize\normalstyle} + +% ************************************************************************** +% ***** Keywords Definition ******************************************** +% ************************************************************************** +\def\keywords{\vspace{-.3em} + \if@twocolumn + \small\bfseries{\itshape\keywordsname\/---}% + \else + \begin{center}\small\bf\keywordsname\end{center}\quotation\small + \fi\ignorespaces} +\def\endkeywords{\vspace{0.6em}\par\if@twocolumn\else\endquotation\fi + \normalsize\normalstyle} + +% ************************************************************************** +% ***** Fix Section Numbering ****************************************** +% ************************************************************************** +\gdef\@punct{.\ \ } % Punctuation after run-in section heading +\def\@sect#1#2#3#4#5#6[#7]#8{% + \ifnum #2>\c@secnumdepth + \def\@svsec\@empty + \else + \refstepcounter{#1}% + \protected@edef\@svsec{% + %\ifnum #2=1\Roman{#1}.\fi\ifnum #2=2\Alph{#1}.\fi + \ifnum #2=1\thesection.\fi + \ifnum #2=2\thesubsection.\fi + \ifnum #2>2{\csname the#1dis\endcsname}\if@technote.\fi\fi \hskip .5em} + \ifnum #2=1\ifappendix\stepcounter{numappendices}\fi\fi + \fi + \@tempskipa #5\relax + \ifdim \@tempskipa>\z@ + \begingroup #6\relax + \@hangfrom{\hskip #3\relax\@svsec}{\interlinepenalty \@M #8\par} + \endgroup + \csname #1mark\endcsname{#7} + \addcontentsline{toc}{#1}{\ifnum #2>\c@secnumdepth\else + \protect\numberline{\csname the#1\endcsname}\fi#7} + \else + \def\@svsechd{#6\hskip #3\@svsec #8\@punct\csname #1mark\endcsname{#7} + \addcontentsline{toc}{#1}{\ifnum #2>\c@secnumdepth \else + \protect\numberline{\csname the#1\endcsname}\fi#7}} + \fi + \@xsect{#5}} + +\def\@ssect#1#2#3#4#5{\@tempskipa #3\relax + \ifdim \@tempskipa>\z@ + \begingroup #4\@hangfrom{\hskip #1}{\interlinepenalty \@M #5\par}\endgroup + \else \def\@svsechd{#4\hskip #1\relax #5\@punct}\fi + \@xsect{#3}} + +% ************************************************************************** +% ***** Section Definitions ******************************************** +% ************************************************************************** +\def\section{\@startsection{section}{1}{\z@}{2.0ex plus .5ex + minus .2ex}{1.0ex plus .2ex}{\centering\scshape}} +\def\subsection{\@startsection{subsection}{2}{\z@}{2.0ex plus .5ex + minus .2ex}{1.0ex plus .2ex}{\itshape}} +\if@technote + \def\subsubsection{\@startsection{subsubsection}{3}{\z@}{2.0ex plus .5ex + minus .1ex}{0pt}{\itshape}} +\else + \def\subsubsection{\@startsection{subsubsection}{3}{\z@}{2.0ex plus .5ex + minus .2ex}{1.0ex plus .2ex}{\normalstyle}} + \def\paragraph{\@startsection{paragraph}{4}{\z@}{1.0ex plus .5ex + minus .2ex}{0ex}{\normalstyle}} +\fi + +% ************************************************************************** +% ***** Special Environment Definitions ******************************** +% ************************************************************************** +\def\QED{\mbox{\rule[0pt]{1.5ex}{1.5ex}}} +\def\proof{\noindent\hspace{1em}{\it Proof: }} +\def\endproof{\hspace*{\fill}~\QED\par\endtrivlist\unskip} +\def\@begintheorem#1#2{\tmpitemindent\itemindent\topsep 0pt\normalstyle\trivlist + \item[\hskip \labelsep{\indent\it #1\ #2:}]\itemindent\tmpitemindent} +\def\@opargbegintheorem#1#2#3{\tmpitemindent\itemindent\topsep 0pt\normalstyle \trivlist + \item[\hskip\labelsep{\indent\it #1\ #2\ \normalstyle(#3)}]\itemindent\tmpitemindent} +\def\@endtheorem{\endtrivlist\unskip} + +% ************************************************************************** +% ***** Special Environment Definitions ******************************** +% ************************************************************************** +\if@twoside\else\raggedbottom\fi + +%% Definition for Big letter at the beginning of a paragraph +%% +\def\PARstart#1#2 {\begingroup\def\par{\endgraf\endgroup\lineskiplimit=0pt} + \setbox2=\hbox{\uppercase{#2} }\newdimen\tmpht \tmpht \ht2 + \advance\tmpht by \baselineskip\font\hhuge=cmr10 at \tmpht + \setbox1=\hbox{{\hhuge #1}} + \count7=\tmpht \count8=\ht1\divide\count8 by 1000 \divide\count7 by\count8 + \tmpht=.001\tmpht\multiply\tmpht by \count7\font\hhuge=cmr10 at \tmpht + \setbox1=\hbox{{\hhuge #1}} \noindent \hangindent1.05\wd1 + \hangafter=-2 {\hskip-\hangindent \lower1\ht1\hbox{\raise1.0\ht2\copy1}% + \kern-0\wd1}\copy2\lineskiplimit=-1000pt} + +\def\PARstartCal#1#2 {\begingroup\def\par{\endgraf\endgroup\lineskiplimit=0pt} + \setbox2=\hbox{\uppercase{#2} }\newdimen\tmpht \tmpht \ht2 + \advance\tmpht by \baselineskip\font\hhuge=cmsy10 at \tmpht + \setbox1=\hbox{{\hhuge #1\/}} + \count7=\tmpht \count8=\ht1\divide\count8 by 1000 \divide\count7 by\count8 + \tmpht=.001\tmpht\multiply\tmpht by \count7\font\hhuge=cmsy10 at \tmpht + \setbox1=\hbox{{\hhuge #1\/}} \noindent \hangindent1.05\wd1 + \hangafter=-2 {\hskip-\hangindent \lower1\ht1\hbox{\raise1.0\ht2\copy1}% + \kern-0\wd1}\copy2\lineskiplimit=-1000pt} + +\def\PARstartLyX#1{\PARstart #1} +\def\PARstartCalLyX#1{\PARstartCal #1} + +\if@technote\def\PARstart#1#2{#1#2}\fi % if technical note, disable it +\if@technote\def\PARstartCal#1#2{#1#2}\fi % if technical note, disable it +\if@technote\def\PARstartLyX#1{#1}\fi % if technical note, disable it +\if@technote\def\PARstartCalLyx#1{#1}\fi % if technical note, disable it + +% ************************************************************************** +% ***** Misc. Definitions ********************************************** +% ************************************************************************** +%Restore single spacing +\newcommand{\blsone}{\renewcommand\baselinestretch{1}% + \renewcommand\arraystretch{1.2}\setlength{\parindent}{\parindentsave}% + \normalsize} +\newcommand{\capitem}[1]{{\hspace{0.2ex}(#1)}~} +\newcommand{\insdate}{} + +% ************************************************************************** +% ***** MATH Definitions *********************************************** +% ************************************************************************** +\def\eqnarray{% + \stepcounter{equation}% + \def\@currentlabel{\p@equation\theequation}% + \global\@eqnswtrue + \m@th + \global\@eqcnt\z@ + \tabskip\@centering + \let\\\@eqncr + $$\everycr{}\halign to\displaywidth\bgroup + \hskip\@centering$\displaystyle\tabskip\z@skip{##}$\@eqnsel + &\global\@eqcnt\@ne\hskip \eqnarr@ysep\hfil${##}$\hfil + &\global\@eqcnt\tw@ \hskip \eqnarr@ysep + $\displaystyle{##}$\hfil\tabskip\@centering + &\global\@eqcnt\thr@@ \hb@xt@\z@\bgroup\hss##\egroup + \tabskip\z@skip + \cr +} +\def\endeqnarray{% + \@@eqncr + \egroup + \global\advance\c@equation\m@ne + $$\@ignoretrue +} + +% ************************************************************************** +% ***** Biography Definitions ****************************************** +% ************************************************************************** +% This is the main code for the biography environment of the IEEE +% transactions class. The previous biography code had some known +% problems which were difficult to fix. The crux of the issue was that +% the photo frame was overlaid by text when \baselinestretch>1 or when +% the biography consisted of multiple short paragraphs. +% +% The fix was done by extracting code from the excellent package: +% 'picinpar.sty' version 1.2a as of july 13, 1993 +% by Friedhelm Sowa +% +% (At least most of) The bugs you find in this code were introduced +% unwittingly by myself. +% +%---------------- +% Known problems: +% +% - Don't use multiple blank lines to separate paragraphs. A single +% blank line works well, but multiple blank lines will confuse +% the code. This has something to do with the \def\par{\\\indent} +% line, but I can't think of an appropriate fix. Similarly, make +% sure the environment doesn't end with an extra blank line. +% - Don't use \samepage +% - Use \footnotemark within and \footnotetext outside the +% window-environment instead of \footnote +% - When using the epic-package load picinpar before epic +% like \documentstyle[...,picinpar,epic]{...} +% +% Counts +\newcount\br \newcount\nb \newcount\tcdsav \newcount\tcl \newcount\tcd +\newcount\tcn \newcount\cumtcl +% Dimens +\newdimen\rtside \newdimen\hpic \newdimen\vpic \newdimen\strutilg +\newdimen\picwd \newdimen\topheight \newdimen\ilg \newdimen\lpic +\newdimen\lwindowsep \newdimen\rwindowsep % VK 10 Feb 93 +\lwindowsep0.5\baselineskip % " +\rwindowsep0.5\baselineskip % " +\newdimen\cumpar +% Tokens +\newtoks\twa \newtoks\la \newtoks\ra \newtoks\ha \newtoks\pictoc +% Boxes +\newbox\rawtext \newbox\holder \newbox\windowbox \newbox\wartext +\newbox\finaltext \newbox\aslice \newbox\bslice \newbox\wbox +\newbox\wstrutbox \newbox\picbox \newbox\waslice \newbox\wbslice +\newbox\fslice + % Another strut +\def\wstrut{\relax\ifmmode\copy\wstrutbox\else\unhcopy\wstrutbox\fi} +% + +\def\getpic#1{\sbox{\@tempboxa}{\includegraphics{#1}}% +\newcount\tmpcta \tmpcta=\ht\@tempboxa% +\newcount\tmpctb \tmpctb=\wd\@tempboxa% +\divide\tmpctb by 100% +\divide\tmpcta by\tmpctb% +\ifnum\tmpcta>133% +\typeout{ieee: Biography picture `#1' too tall.}% +\frame{\hbox to 25mm{\hfil\resizebox{!}{32mm}{\usebox{\@tempboxa}}\hfil}}% +\else \ifnum\tmpcta<123% +\typeout{ieee: Biography picture `#1' too wide.}% +\frame{\vbox to 32mm{\vss\hbox{\resizebox{25mm}{!}{\usebox{\@tempboxa}}}\vss}}% +\else% +\resizebox{25mm}{32mm}{\usebox{\@tempboxa}} +\fi\fi} + +\long\def\biographyLyX#1{\if@non\else\begin{biography} #1\end{biography}\fi} + +\if@non + \long\def\biography{} +\else + \long\def\biography{\@ifnextchar [{\@biographyb}{\@biographya[{\unitlength + 1mm\hbox{\framebox(25,32){}}}]}} +\fi + +\long\def\@biographyb[#1]{\@biographya[\getpic{#1}]} + +\long\def\@biographya[#1]#2{\bgroup +\footnotesize\bigskip\bigskip\bigskip\parskip=0pt\par% +\rule{0pt}{35mm}\vspace*{-35mm}\par% garantees correct page breaking +\begin{main@bio}[{#1}]% +\noindent{\bf #2}% +} +\def\endbiography{\if@non\else\end{main@bio}\egroup\fi} + +\long\def\main@bio[#1]{% #1 is the material for setting a graphic box +\vskip\parskip\everypar{} +\global\cumpar=0pt +\global\cumtcl=0 + \tcd=0 + \rtside=0pt +% \hpic=\linewidth + \twa={} \la={} \ra={} \ha={} +\setbox\wbox=\hbox{(} +\computeilg +\pictoc={#1} +\setbox\windowbox=\vbox{\hbox{#1}} +\picwd=\wd\windowbox +\hpic=\picwd +\vpic=\ht\windowbox\advance\vpic\dp\windowbox +\rtside=\linewidth\advance\rtside-\picwd +\setbox\picbox=\vbox{\hsize=\hpic\vbox to\vpic{\box\windowbox}}% \vfill}}% + +\vpic=\ht\picbox\advance\vpic\dp\picbox +\ifdim\rtside>0pt\advance\rtside-\rwindowsep\fi % " +\global\br=\rtside +\ifnum\picwd=0 +\ifdim\vpic>0pt\picwd=\hpic +\else\vpic=\ht\picbox\advance\vpic\dp\picbox +\fi +\fi + \global\tcl=0 \lpic=0pt + \loop\global\advance\tcl by 1 \lpic=\tcl\baselineskip + \ifdim\lpic<\vpic\repeat + \vpic=\lpic + \global\cumtcl=\tcl +% +% Here we know exactly the number of indented lines and +% are able to generate the tokens for the \parshape list +% + \ifnum\br>0\ra={ 0pt \rtside}\fi + \ifnum\tcd>0\ha={ 0pt \linewidth}\fi + \ifnum\tcl<1\global\tcl=1\fi + \createparshapespec + \tcd=0 % restore the lintel + \global\tcdsav=0 +% +% This is a very tricky part of the package. Some day there +% will exist a detailed documentation. +% +\def\par{\\\indent} +% +% This is where we start to pick up the paragraph(s) +% + \setbox\rawtext=\vbox\bgroup\unvbox\rawtext\unskip + \clubpenalty=0\widowpenalty=0 + \ifnum\brokenpenalty<\maxdimen\else\brokenpenalty=9999\fi + \tolerance=1000 + \parshape=\tcn \the\twa } +% +\def\endmain@bio{% + %\par + \global\tcd=\tcdsav + \egroup\vskip\parskip\parshape=0 % reset parshape; end \box\rawtext + \vbadness=10000 + \splittopskip=0pt +% +% Now we build the boxes beside the window +% +\global\topheight=\tcl\baselineskip +\ifnum\br>0\setbox\holder=\vsplit\rawtext to\topheight\fi +\tcn=\tcl \nb=0 +\ifnum\br>0\nb=\tcn\fi +% +% text on the right side +% +\ifnum\nb>0 + \loop\advance\nb -1 + \setbox\bslice=\vsplit\holder to\baselineskip + \prune\bslice\rtside + \setbox\wbslice=\vbox{\unvbox\wbslice\hbox + to\rtside{\box\bslice\hfil}} + \ifdim\ht\holder>0pt\repeat +\fi +%GLP add fix to make sure bio starts at top of picture +\setbox\wbslice=\vbox to\topheight{\unvbox\wbslice\vfill\vss} +% +% fixing the dimensions of the window part +% +\topheight=\ht\wbslice +% +% ship out the window material to the main vertical list +% +\setbox\windowbox=\vbox{\hbox to\linewidth{% +\vbox to\topheight{\hrule width\picwd height0pt depth0pt\vskip0pt% +\vfill\unvbox\picbox% +\ifnum\picwd>0\vfill\fi% +\vss}\ifnum\br>0\hfill\vbox{\box\wbslice}\fi}}% +% +\unvbox\windowbox% +\loop% lines below picture.... + \setbox\bslice=\vsplit\rawtext to\baselineskip + \prune\bslice\linewidth + \setbox\wbslice=\vbox{\hbox to\linewidth{\box\bslice\hfil}} + \unvbox\wbslice + \ifdim\ht\rawtext>0pt +\repeat +%GLP +%\ifnum\nb>0\topheight=\nb\baselineskip %\advance\topheight by\ilg +%\vspace*{\topheight} +%\fi +}% FINITO +% +% What else do we need? +% +\def\prune#1#2{ +% take a \vbox containing a single \hbox, +% \unvbox it, and cancel the \lastskip +% put in a \hbox of width #2 + \unvbox#1 \setbox#1=\lastbox % \box#1 now is an \hbox + \ifdim\ht#1=\parskip + \setbox#1=\hbox to#2{\vrule height\parskip depth0pt width0pt\hfill} + \else\ifdim\ht#1=0pt\relax + \else\setbox#1=\hbox to#2{\wstrut\unhbox#1\unskip}\fi\fi} +% +% Here the token \twa is generated. +% It's not so difficult as it looks like. +% +\def\createparshapespec{% +\global\tcn=0 +\ifnum\br>0\global\tcn=\tcl\fi +\nb=0 +\ifnum\br>0\nb=\tcn\fi +\global\advance\tcn by\tcd \global\advance\tcn by1 +\ifnum\tcd>0 +\loop\twa=\expandafter{\the\twa\the\ha}\advance\tcd -1 +\ifnum\tcd>0\repeat +\fi +\ifnum\nb>0 +\loop\twa=\expandafter{\the\twa\the\ra}\advance\nb -1 +\ifnum\nb>0\repeat +\fi +\global\twa=\expandafter{\the\twa 0pt \the\linewidth}} +% +\def\computeilg{% compute the interline glue + \tcl=0\ilg=0pt\strutilg=0pt + \loop\setbox\wbox=\hbox{\char\tcl} + \ifdim\ht\wbox>\ilg\ilg=\ht\wbox\fi + \ifdim\dp\wbox>\strutilg\strutilg=\dp\wbox\fi + \advance\tcl by 1 + \ifnum\tcl<128\repeat + \ht\wbox=\ilg + \dp\wbox=\strutilg + \strutilg=\ht\wbox %\advance\strutilg by\ilg + \ifdim\strutilg>\baselineskip + \typeout{character with height greater baselineskip found in font} + \typeout{baselineskip changed to 1.5 of that height!} + \baselineskip=1.5\strutilg + \fi + \global\ilg=\baselineskip + \global\advance\ilg-\ht\wbox \global\advance\ilg-\dp\wbox + \strutilg=\ht\wbox \advance\strutilg by\ilg + \setbox\wstrutbox=\hbox{\vrule height\strutilg depth\dp\wbox width0pt}} + + +% the following code from version.sty by Stephen Bellantoni 1990, loosely +% based on "annotation.sty" by Tom Hofmann. Used to exclude "biography" from +% anonymous mode. +\begingroup +\catcode`@=11\relax% +\catcode`{=12\relax\catcode`}=12\relax% +\catcode`(=1\relax \catcode`)=2\relax% +\gdef\glpinclude#1(% + \expandafter\gdef\csname #1\endcsname% + ()% + \expandafter\gdef\csname end#1\endcsname% + ()% +)% +\gdef\glpexclude#1(% + \expandafter\gdef\csname #1\endcsname% + (\@bsphack\catcode`{=12\relax\catcode`}=12\relax\csname #1@NOTE\endcsname)% + \long\expandafter\gdef\csname #1@NOTE\endcsname ##1\end{#1}% + (\csname #1END@NOTE\endcsname)% + \expandafter\gdef\csname #1END@NOTE\endcsname% + (\@esphack\end(#1))% +)% +\endgroup + +%------- +\def\@confplacedate{\typeout{ieee: Warning! No \noexpand\confplacedate set!} +\bfseries `confplacedate' needs to be set. For example, to: Stanford, CA, USA, +September 29--30, 1991} +\def\confplacedate#1{\def\@confplacedate{#1}} + +%%%%%%%%%%%%%%%%%%%%%%%%% End of ieee.cls %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/sigproc.bib b/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/sigproc.bib new file mode 100644 index 000000000..6ccae92ae --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/sigproc.bib @@ -0,0 +1,2549 @@ +@BOOK{salas:calculus,
+ AUTHOR = "S.L. Salas and Einar Hille",
+ TITLE = "Calculus: One and Several Variable",
+ PUBLISHER = "John Wiley and Sons",
+ ADDRESS = "New York",
+ YEAR = "1978" }
+
+@inproceedings{804350,
+ author = {Thomas J. Schaefer},
+ title = {The complexity of satisfiability problems},
+ booktitle = {{STOC}'78},
+ year = {1978},
+ pages = {216--226},
+ location = {San Diego, California, United States},
+ doi = {http://doi.acm.org/10.1145/800133.804350},
+}
+
+Proceedings of the tenth annual ACM symposium on Theory of computing --
+publisher = {ACM Press},
+address = {New York, NY, USA},
+
+@inproceedings{smith94phase,
+ author = "Barbara Smith",
+ title = "The Phase Transition in Constraint Satisfaction Problems: {A} {CL}oser Look at the Mushy Region",
+ booktitle = {{ECAI}'94},
+ year = "1994"
+}
+
+@inproceedings{cheeseman91where,
+ author = "Peter Cheeseman and Bob Kanefsky and William M. Taylor",
+ title = "Where the Really Hard Problems Are",
+ booktitle = "IJCAI-91",
+ pages = "331--337",
+ year = "1991",
+}
+Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, Sidney, Australia
+
+@INPROCEEDINGS{Juels-2004-scn,
+ author = {Juels, Ari},
+ title = {Minimalist Cryptography for Low-Cost {RFID} Tags},
+ booktitle = {International Conference on Security in Communication Networks --- SCN 2004},
+ year = {2004},
+ editor = {Blundo, Carlo and Cimato, Stelvio},
+ volume = {3352},
+ series = {LNCS},
+ pages = {149--164},
+ month = {September},
+ publisher = {Springer-Verlag},
+ address = {Amalfi, Italia},
+}
+
+
+@inproceedings{achlioptas-threshold,
+ author = {Dimitris Achlioptas and Yuval Peres},
+ title = {The Threshold for Random k-{SAT} is 2\^\ k(ln 2 - O(k))},
+ booktitle = {{STOC}'03},
+ year = {2003},
+ isbn = {1-58113-674-9},
+ pages = {223--231},
+ location = {San Diego, CA, USA},
+ doi = {http://doi.acm.org/10.1145/780542.780577},
+}
+Proceedings of the thirty-fifth annual ACM symposium on Theory of computing --
+publisher = {ACM Press}
+address = {New York, NY, USA}
+
+@article{DPLL,
+ author = {Martin Davis and Hilary Putnam},
+ title = {A Computing Procedure for Quantification Theory},
+ journal = {J. ACM},
+ volume = {7},
+ number = {3},
+ year = {1960},
+ issn = {0004-5411},
+ pages = {201--215},
+ doi = {http://doi.acm.org/10.1145/321033.321034},
+}
+publisher = {ACM Press},
+address = {New York, NY, USA},
+
+@inproceedings {Minisat+,
+ author = {E\'en, Niklas and S\"orensson, Niklas},
+ title = {Translating {P}seudo-{B}oolean constraints into {SAT}},
+ booktitle= {Journal on Satisfiability, Boolean Modeling and Computation},
+ year = {2006},
+ pages = {1-26},
+ volume = {2},
+}
+
+@inproceedings {EenS03MiniSat,
+ title = {An Extensible {SAT}-solver},
+ author = {Niklas E\'en and Niklas S\"{o}rensson},
+ booktitle = {SAT},
+ editor = {Enrico Giunchiglia and Armando Tacchella},
+ pages = {502--518},
+ publisher = {Springer},
+ series = {LNCS},
+ url = {http://dblp.uni-trier.de/db/conf/sat/sat2003.html#EenS03},
+ volume = {2919},
+ year = {2003},
+ ee = {http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/cgi/MiniSat.ps.gz.cgi},
+ keywords = {2003 2004 SAT-solver ais-07w efficiency implementation },
+}
+
+@misc { toolbar,
+ author="S. Bouveret and F. Heras and S. de Givry and J. Larrosa and M. Sanchez and T. Schiex",
+ title="Toolbar: a state-of-the-art platform for wcsp",
+ url="http://www.inra.fr/mia/T/degivry/ToolBar.pdf",
+ year="2004"
+}
+
+@inproceedings{1267340,
+ author = {Kirschenbaum, Ilan and Wool, Avishai},
+ title = {How to build a low-cost, extended-range {RFID} skimmer},
+ booktitle = {USENIX-SS'06: Proceedings of the 15th conference on {USENIX} Security Symposium},
+ year = {2006},
+ location = {Vancouver, B.C., Canada},
+ publisher = {{USENIX} Association},
+ address = {Berkeley, CA, USA},
+}
+
+@misc{Benetton-boycott,
+ author = {{CASPIAN - Consumers Against Supermarket Privacy Invasion and Numbering}},
+ howpublished={Press release},
+ note= {\url{http://www.boycottbenetton.com}},
+ title = {Boycott {B}enetton},
+ year = {2003},
+ month = {March},
+}
+
+@article{ improved-deterministic,
+ author="Michael H. Schulz and Elisabeth Auth",
+ title="Improved Deterministic Test Pattern Generation with Applications to Redundancy Identification",
+ year="1989",
+ month="July",
+ journal="IEEE Transactions on computer-aided design",
+ volume="8",
+ number="7",
+ pages={811--816},
+ issn="0278-0070"
+}
+publisher = " IEEE Circuits and Systems Society",
+address="Piscataway, NJ 08854, USA",
+
+@inproceedings{244560,
+ author = {Jo\&\#227;o P. Marques Silva and Karem A. Sakallah},
+ title = {{GRASP}-a new search algorithm for satisfiability},
+ booktitle = {ICCAD'96},
+ year = {1996},
+ isbn = {0-8186-7597-7},
+ pages = {220--227},
+ location = {San Jose, California, United States},
+ publisher = {IEEE Computer Society},
+}
+Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design ---
+address = {Washington, DC, USA},
+
+ @inproceedings{ chai03fast,
+ author = "D. Chai and A. Kuehlmann",
+ title = "A fast pseudo-boolean constraint solver",
+ pages = {305--317},
+ booktitle = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 2003",
+ year = {2003},
+ month =" mar",
+ volume = "24",
+ issue = "3",
+ issn = "0278-0070"
+}
+publisher = "IEEE Circuits and Systems Society",
+
+@TechReport{EPC-standard,
+ author = "EPCglobal",
+ url="http://www.epcglobalinc.org/standards/specs/13.56_MHz_ISM_Band_Class_1_RFID_Tag_Interface_Specification.pdf",
+ title="13.56 {MHz} {ISM} Band Class 1 Radio Frequency Identification Tag Interface Specification (2003)",
+ institution = "Auto-ID cetner, MIT",
+ year ="2003",
+ month = "February",
+ version = "1.0.0"
+}
+address = "77 massachusetts avenue, bldg 3-449, cambridge, ma 02139-4307, USA",
+
+@INPROCEEDINGS{LuLHHN-2007-percom,
+ author = {Lu, Li and Liu, Yunhao and Hu, Lei and Han, Jinsong and Ni, Lionel},
+ title = {A Dynamic Key-Updating Private Authentication Protocol for {RFID} Systems},
+ booktitle = {PerCom 2007},
+ year = {2007},
+ pages = {13--22},
+ month = {March},
+ organization = {IEEE}
+}
+International Conference on Pervasive Computing and Communications
+publisher = {IEEE Computer Society Press}
+address = {New York, USA},
+
+@INPROCEEDINGS{Ohkubo04Efficient,
+ author = {Ohkubo, Miyako and Suzuki, Koutarou and Kinoshita, Shingo},
+ title = {Efficient Hash-Chain Based {RFID} Privacy Protection Scheme},
+ booktitle = {International Conference on Ubiquitous Computing --- Ubicomp 2004, Workshop Privacy: Current Status and Future Directions},
+ month = {September},
+ year = {2004},
+ address = {Nottingham, England},
+}
+
+@INPROCEEDINGS{MolnarSW-2005-sac,
+ author = {Molnar, David and Soppera, Andrea and Wagner, David},
+ title = {A Scalable, Delegatable Pseudonym Protocol Enabling Ownership Transfer of {RFID} Tags},
+ booktitle = {Selected Areas in Cryptography --- SAC 2005},
+ editor = {Preneel, Bart and Tavares, Stafford},
+ volume = {3897},
+ series = {LNCS},
+ pages = {276--290},
+ month = {August},
+ series = {LNCS},
+ publisher = {Springer-Verlag},
+ year = {2005},
+ address = {Kingston, Canada},
+}
+
+@inproceedings{DBLP:conf/otm/FeldhoferR06,
+ author = {Martin Feldhofer and Christian Rechberger},
+ title = {A Case Against Currently Used Hash Functions in {RFID} Protocols},
+ booktitle = {OTM Workshops (1)},
+ year = {2006},
+ pages = {372-381},
+ ee = {http://dx.doi.org/10.1007/11915034_61},
+ crossref = {DBLP:conf/otm/2006-w1},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/otm/2006-w1,
+ editor = {Robert Meersman and Zahir Tari and Pilar Herrero},
+ title = {On the Move to Meaningful Internet Systems 2006: OTM 2006 Workshops, OTM Confederated International Workshops and Posters, AWeSOMe, CAMS, COMINF, IS, KSinBIT, MIOS-CIAO, MONET, OnToContent, ORM, PerSys, OTM Academy Doctoral Consortium, RDDS, SWWS, and SeBGIS 2006, Montpellier, France, October 29 - November 3, 2006. Proceedings, Part I},
+ booktitle = {OTM Workshops (1)},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {4277},
+ year = {2006},
+ isbn = {3-540-48269-5},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+
+@INPROCEEDINGS{VajdaB-2003-ubicom,
+ author = {Vajda, Istv\'an and Butty\'an, Levente},
+ title = {Lightweight Authentication Protocols for Low-Cost {RFID} Tags},
+ booktitle = {Ubicomp 2003 Second Workshop on Security in Ubiquitous Computing},
+ month = {October},
+ year = {2003}
+}
+address = {Seattle, WA, USA},
+
+@INPROCEEDINGS{LiW-2007-sec,
+ author = {Li, Tieyan and Wang, Guilin},
+ title = {Security Analysis of Two Ultra-Lightweight {RFID} Authentication Protocols},
+ booktitle = {IFIP SEC 2007},
+ month = {May},
+ organization = {IFIP},
+}
+year = {2007},
+address = {Sandton, Gauteng, South Africa},
+
+@MISC{BatinaGKMTV-2006-eprint,
+ author = {Batina, Lejla and Guajardo, Jorge and Kerins, Tim and Mentens, Nele and Tuyls, Pim and Verbauwhede, Ingrid},
+ title = {An Elliptic Curve Processor Suitable For {RFID}-Tags},
+ howpublished = {Cryptology ePrint Archive, Report 2006/227},
+ year = {2006},
+ organization = {IACR},
+}
+
+@inproceedings {AES-grain-sand,
+ title = {{AES} implementation on a grain of sand},
+ issue = "1",
+ ISSN="1747-0722",
+ pages = {13--20},
+ author="Feldhofer, M. and Wolkerstorfer, J. and Rijmen, V.",
+ year = "2005",
+ voulme="152",
+ booktitle = "Information Security",
+ organization = {IEEE},
+}
+publisher = {IEEE Computer Society Press},
+
+@MISC{Juels-2005-manuscript-2,
+ author = {Juels, Ari},
+ title = {{RFID} Security and Privacy: A research Survey},
+ howpublished = {Manuscript},
+ year = {2005},
+ month = {September},
+ organization = {RSA Laboratories},
+}
+
+@INPROCEEDINGS{JuelsW-2007-percom,
+ author = {Juels, Ari and Weis, Stephen},
+ title = {{Defining Strong Privacy for RFID}},
+ booktitle = {International Conference on Pervasive Computing and Communications --- PerCom 2007},
+ year = {2007},
+ editor = {},
+ volume = {},
+ series = {},
+ pages = {342--347},
+ address = {New York City, New York, USA},
+ month = {March},
+ organization = {IEEE},
+ publisher = {IEEE Computer Society Press},
+ bibsource = {Information Security Group (GSI), UCL, Louvain-la-Neuve, Belgium},
+}
+
+@INPROCEEDINGS{Vaudenay-2007-asiacrypt,
+ author = {Vaudenay, Serge},
+ title = {On Privacy Models for {RFID}},
+ booktitle = {Advances in Cryptology --- Asiacrypt 2007},
+ year = {2007},
+ editor = {},
+ volume = {4833},
+ series = {LNCS},
+ pages = {68--87},
+ address = {Kuching, Malaysia},
+ month = {December},
+ organization = {},
+ publisher = {Springer-Verlag},
+ bibsource = {Information Security Group (GSI), UCL, Louvain-la-Neuve, Belgium},
+}
+
+@INPROCEEDINGS{BolotnyyR-2007-percom,
+ author = {Bolotnyy, Leonid and Robins, Gabriel},
+ title = {Physically Unclonable Function-Based Security and Privacy in {RFID} Systems},
+ booktitle = {PerCom 2007},
+ year = {2007},
+ pages = {211--220},
+ month = {March},
+ organization = {IEEE},
+}
+publisher = {IEEE Computer Society Press}
+International Conference on Pervasive Computing and Communications --
+address = {New York, USA},
+
+@INPROCEEDINGS{JuelsRS-2003-ccs,
+ author = {Juels, Ari and Rivest, Ronald and Szydlo, Michael},
+ title = {The Blocker Tag: Selective Blocking of {RFID} Tags for Consumer Privacy},
+ booktitle = {ACM CCS 2003},
+ year = {2003},
+ editor = {Atluri, Vijay},
+ pages = {103--111},
+ month = {October},
+ publisher = "ACM Press"
+}
+address = {Washington, DC, USA},
+Conference on Computer and Communications Security
+organization = "ACM",
+
+@INPROCEEDINGS{JuelsW-2005-crypto,
+ author = {Juels, Ari and Weis, Stephen},
+ title = {Authenticating Pervasive Devices with Human Protocols},
+ booktitle = {Advances in Cryptology --- CRYPTO'05},
+ year = {2005},
+ editor = {Shoup, Victor},
+ volume = {3126},
+ series = {LNCS},
+ pages = {293--308},
+ month = {August},
+ organization = {IACR},
+ address = {Santa Barbara, California, USA},
+ publisher = {Springer-Verlag},
+ series = {LNCS},
+}
+
+@inproceedings{ zhang01efficient,
+ author = "Lintao Zhang and Conor F. Madigan and Matthew W. Moskewicz and Sharad Malik",
+ title = "Efficient Conflict Driven Learning in Boolean Satisfiability Solver",
+ booktitle = "{ICCAD}",
+ pages = "279-285",
+ year = "2001",
+ url = "citeseer.ist.psu.edu/article/zhang01efficient.html" }
+
+
+@INPROCEEDINGS{ButtyanHV-2006-pet,
+ author = {Butty\'an, Levente and Holczer, Tam\'as and Vajda, Istv\'an},
+ title = {Optimal Key-Trees for Tree-Based Private Authentication},
+ booktitle = {Workshop on Privacy Enhancing Technologies --- PET 2006},
+ pages = {332-350},
+ month = {June},
+ year = {2007},
+ address = {Cambridge, United Kingdom},
+}
+
+
+@INPROCEEDINGS{Castelluccia07Secret,
+ author = {Castelluccia, Claude and Soos, Mate},
+ title = {Secret Shuffling: A Novel Approach to {RFID} Private Identification},
+ booktitle = {{RFIDSec}'07},
+ pages = {169-180},
+ year = {2007},
+ month = {July}
+}
+Proceedings of the International Conference on RFID Security 2007
+
+@INPROCEEDINGS{breaking-lmap,
+ author = {Mihaly B\'arasz and Bal\'azs Boros and P\'eter Ligeti and Krisztina L\'oja and D\'aniel Nagy},
+ title = {Breaking {LMAP}},
+ pages = {69-78},
+ month = {July},
+ year = {2007},
+ booktitle = {Conference on RFID Security --- {RFIDSec}'07},
+ address = {Malaga, Spain},
+}
+
+@INPROCEEDINGS{Initial-SRAM,
+ author = {Daniel Holcom and Wayne Burleson and Kevin Fu.},
+ title = {Initial {SRAM} state as a Fingerprint and Source of True Random Numbers for {RFID} Tags},
+ booktitle = {{RFIDSec}'07},
+ pages = {29-40},
+ month = {July},
+ year = {2007}
+}
+Proceedings of the International Conference on RFID Security 2007
+
+@inproceedings{HBattack,
+ author = {Gilbert, Henri and Robshaw, Matt and Sibert, Herve},
+ title = {An Active Attack Against {HB}$^+$ - A Provably Secure Lightweight Authentication Protocol},
+ booktitle = {IEE Electronic Letters 41, 21},
+ year = {2005},
+ pages = {1169--1170}
+}
+
+@INPROCEEDINGS{KatzS-2006-eurocrypt,
+ author = {Katz, Jonathan and Sun Shin, Ji},
+ title = {Parallel and Concurrent Security of the {HB} and {HB}$^{+}$ Protocols},
+ booktitle = {Advances in Cryptology --- EUROCRYPT '06},
+ organization = {IACR},
+ year = {2006}
+}
+Advances in Cryptology
+publisher = {Springer-Verlag},
+
+@MISC{KatzS-2006-eprint,
+ author = {Katz, Jonathan and Smith, Adam},
+ title = {Analyzing the {HB} and {HB}+ Protocols in the ``Large Error'' Case},
+ howpublished = {Cryptology ePrint Archive, Report 2006/326},
+ organization = {IACR},
+}
+
+@inproceedings{1229319,
+ author = {Tri Van Le and Mike Burmester and Breno de Medeiros},
+ title = {Universally composable and forward-secure {RFID} authentication and authenticated key exchange},
+ booktitle = {Proceedings of the 2nd ACM symposium on Information, Computer and Communications Security --- {ASIACCS}'07},
+ year = {2007},
+ isbn = {1-59593-574-6},
+ pages = {242--252},
+ location = {Singapore},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ doi = {http://doi.acm.org/10.1145/1229285.1229319},
+}
+
+
+
+@INPROCEEDINGS{PUF-based-RNG,
+ author = {Charles W. O'Donnell and G. Edward Suh and Srinivas Devadas},
+ title = {{PUF}-Based Random Number Generation},
+ booktitle = {MIT CSAIL CSG Technical Memo 481},
+ url = {http://csg.csail.mit.edu/pubs/memos/Memo-481/Memo-481.pdf},
+ year = {2004},
+ month = {November}
+}
+
+@book{Ipatov05Spread,
+ author = {Valeri P. Ipatov},
+ year = {2005},
+ month = {May},
+ title = {Spread Spectrum and {CDMA}: {P}rinciples and Applications},
+ publisher = {John Wiley \& Sons, Ltd.},
+ ISBN = {978-0470091784},
+}
+
+@article{DBLP:journals/ijwmc/HellJM07,
+ author = {Martin Hell and
+ Thomas Johansson and
+ Willi Meier},
+ title = {Grain: a stream cipher for constrained environments},
+ journal = {IJWMC},
+ volume = {2},
+ number = {1},
+ year = {2007},
+ pages = {86-93},
+ ee = {http://dx.doi.org/10.1504/IJWMC.2007.013798},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@book{applied-crypto,
+ year= {1996},
+ ISBN ={0-8493-8523-7},
+ author={Alfred J. Menezes and Paul C. van Oorschot and Scott A. Vanstone},
+ title ={Handbook of applied cryptography},
+ publisher={CRC Press},
+ address={Boca Raton, Florida},
+}
+url={http://cacr.math.uwaterloo.ca/hac}
+
+@inproceedings{DiPietro07Information,
+ author={Roberto Di Pietro and Refik Molva},
+ title={Information confinement, privacy, and security in {RFID} systems},
+ month={September},
+ booktitle={Proceedings of the 12th European Symposium On Research In Computer Security},
+ year={2007},
+ pages={187-202},
+}
+
+@inproceedings{PerisHER-2006-rfidsec,
+ author = {Peris-Lopez, Pedro and Hernandez-Castro, Julio Cesar and Estevez-Tapiador, Juan and Ribagorda, Arturo},
+ title = {{LMAP}: A Real Lightweight Mutual Authentication Protocol for Low-cost {RFID} tags},
+ booktitle = {Proceedings of {RFIDSec}'06},
+ year = {2006},
+ month = {July},
+ address = {Graz, Austria},
+ organization = {Ecrypt},
+}
+
+@INPROCEEDINGS{BringerCD-2006-secperu,
+ author = {Bringer, Julien and Chabanne, Herv\'e and Dottax Emmanuelle},
+ title = {{HB}$^{++}$: a Lightweight Authentication Protocol Secure against Some Attacks},
+ booktitle = {{IEEE} SecPerU 2006},
+ year = {2006},
+ month = {June},
+ organization = {IEEE},
+}
+International Conference on Pervasive Services, Workshop on Security, Privacy and Trust in Pervasive and Ubiquitous Computing
+address = {Lyon, France},
+publisher = {IEEE Computer Society Press},
+
+@INPROCEEDINGS{PerisHER-2006-uic,
+ author = {Peris-Lopez, Pedro and Hernandez-Castro, Julio Cesar and Estevez-Tapiador, Juan and Ribagorda, Arturo},
+ title = {{M2AP}: A Minimalist Mutual-Authentication Protocol for Low-cost {RFID} Tags},
+ booktitle = {International Conference on Ubiquitous Intelligence and Computing --- {UIC}’06},
+ year = {2006},
+ editor = {},
+ volume = {4159},
+ pages = {912--923},
+ month = {September},
+ series = {LNCS},
+ publisher = {Springer-Verlag},
+}
+
+
+@INPROCEEDINGS{M2AP-break,
+ author={Mih\'aly B\'ar\'asz and Bal\'azs Boros and P\'eter Ligeti and Krisztina L\'oja and D\'aniel A. Nagy},
+ title={Passive Attack Against the {M2AP} Mutual Authentication Protocol for {RFID} Tags},
+ year = {2007},
+ month= {September},
+ date = {24-25},
+ booktitle={{RFID} 2007 --- The First International {EURASIP} Workshop on {RFID} Technology},
+ country = {Austria},
+ city={Vienna}
+}
+
+@INPROCEEDINGS{HBppbreak,
+ author= {Henri Gilbert and Matthew J.B. Robshaw and Yannick Seurin},
+ title={Good Variants of {HB}+ are Hard to Find},
+ year={2008},
+ month={January},
+ booktitle={Financial Cryptography},
+ publisher={Springer},
+ country={Mexico}
+}
+
+@inproceedings{MAGMA,
+ author = {Wieb Bosma and John Cannon and Graham Matthews},
+ title = {Programming with algebraic structures: design of the {MAGMA} language},
+ booktitle = {Proceedings of the international symposium on Symbolic and algebraic computation --- ISSAC '94},
+ year = {1994},
+ isbn = {0-89791-638-7},
+ pages = {52--57},
+ location = {Oxford, United Kingdom},
+ doi = {http://doi.acm.org/10.1145/190347.190362},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
+
+@inproceedings{Singular,
+ author = {Gert-Martin Greuel and Gerhard Pfister and Hans Sch\"{o}nemann},
+ title = {{SINGULAR} --- A computer algebra system for polynomial computations},
+ booktitle = {Symbolic computation and automated reasoning},
+ year = {2001},
+ isbn = {1-56881-145-4},
+ pages = {227--233},
+ publisher = {A. K. Peters, Ltd.},
+ address = {Natick, MA, USA},
+}
+
+@misc{SAGE,
+ author = {{The SAGE Group}},
+ year = {2008},
+ title = {{SAGE} Mathematics Software},
+ note = {\url{http://www.sagemath.org}},
+}
+
+@misc{new-sparse-technique,
+ author={H{\aa}vard Raddum and Igor Semae},
+ title={New Technique for Solving Sparse Equation Systems},
+ month={January},
+ year={2006},
+ note={\url{eprint.iacr.org/2006/475/}},
+}
+
+@TechReport{algebraic-DES,
+ author={Nicolas T. Courtois and Gregory V. Bard},
+ title={Algebraic Cryptanalysis of the {D}ata {E}ncryption {S}tandard},
+ year={2006},
+ institution = {IACR E-print},
+ number = {2006/402},
+ month={November},
+ booktitle={IACR E-print, \url{http://eprint.iacr.org/2006/402}},
+}
+
+
+
+@inproceedings{early-DES-algebraic,
+ author={Chaum, David and Evertse, Jan-Hendrik},
+ title={Cryptanalysis of {DES} with a Reduced Number of Rounds},
+ booktitle = {Advances in Cryptology --- {CRYPTO}'85},
+ year = {1986},
+ pages = {192--211},
+ publisher = {Springer-Verlag}
+}
+
+@InProceedings{Bofilletal2008CAV,
+ author = {M. Bofill and R. Nieuwenhuis and A. Oliveras and E. Rodr\'\i guez-Carbonell and A. Rubio},
+ title = {The {B}arcelogic {SMT} Solver},
+ pages = {294-298},
+ booktitle = {{CAV}'08},
+ year = {2008},
+ series = {LNCS},
+ volume = {5123},
+ publisher = {Springer},
+ editor = {A. Gupta and S. Malik},
+}
+
+@techreport{RSAT,
+ author = {Knot Pipatsrisawat and Adnan Darwiche},
+ institution = {Automated Reasoning Group, Computer Science},
+ title = {{RS}at 2.0: {SAT} Solver Description},
+ year = {2007},
+}
+
+@inproceedings{DBLP:conf/fse/CourtoisBW08,
+ author = {Nicolas Courtois and Gregory V. Bard and David Wagner},
+ title = {Algebraic and Slide Attacks on {K}ee{L}oq},
+ booktitle = {FSE},
+ year = {2008},
+ pages = {97-115},
+ ee = {http://dx.doi.org/10.1007/978-3-540-71039-4_6},
+ crossref = {DBLP:conf/fse/2008},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@TechReport{cryptoeprint:2008:166,
+ author = {Nicolas T. Courtois and Karsten Nohl and Sean O'Neil},
+ title = {Algebraic Attacks on the {C}rypto-1 Stream Cipher in {Mifare} {C}lassic and {O}yster Cards},
+ number = {2008/166},
+ institution = {Cryptology ePrint Archive},
+ year = {2008},
+}
+howpublished = {Cryptology ePrint Archive, Report 2008/166},
+note = {\url{http://eprint.iacr.org/}},
+
+@INPROCEEDINGS{Biere99symbolicmodel,
+ author = {Armin Biere and A. Cimatti and E. M. Clarke and M. Fujita and Y. Zhu},
+ title = {Symbolic Model Checking Using {SAT} Procedures instead of {BDDs}},
+ booktitle = {Proc. of Design Automation Conference ({DAC}'99)},
+ year = {1999},
+ pages = {317--320}
+}
+
+@INPROCEEDINGS{temporalinduction,
+ author = {E\'en, Niklas and S\"orensson, Niklas},
+ title = {Temporal Induction by Incremental {SAT} Solving},
+ booktitle={Proc. of First Intrenational Workshop on Bounded Model Checking},
+ year={2003},
+ volume={89},
+ issue={4},
+ series={ENTCS},
+ publisher={Elsevier}
+}
+
+@inproceedings{ARMS02,
+ author = {Fadi A. Aloul and Arathi Ramani and Igor Markov and Karem Sakallah},
+ title = {Generic {ILP} versus Specialized 0-1 {ILP}: an Update},
+ booktitle = {Proc. ACM/IEEE Intl. Conf. Comp.-Aided Design},
+ pages = {450 - 457},
+ month = {November},
+ year = {2002},
+ URL = {http://www.gigascale.org/pubs/190.html}
+}
+
+@inproceedings{knowledge-compiling,
+ author={Adnan Dawiche},
+ title={New advances in compiling {CNF} to decomposable negation normal form},
+ booktitle={Proc. of European Conference on Artificial Intelligence},
+ year={2004},
+ pages={328 - 332},
+}
+
+@InProceedings{S-Match,
+ author = {Fausto Giunchiglia and Pavel Shvaiko and Mikalai Yatskevich},
+ title = {S-{M}atch: an algorithm and an implementation of semantic matching},
+ booktitle = {Semantic Interoperability and Integration},
+ year = {2005},
+ number = {04391},
+ series = {Dagstuhl Seminar Proceedings},
+ ISSN = {1862-4405},
+ publisher = {IBFI},
+ note = {\url{http://drops.dagstuhl.de/opus/volltexte/2005/37}},
+ editor = {Y. Kalfoglou and M. Schorlemmer and A. Sheth and S. Staab and M. Uschold},
+}
+publisher = {Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI)},
+
+
+
+@techreport{bard-thesis,
+ author = {Gregory V. Bard},
+ title = {Algorithms for the Solution of Polynomial and Linear Systems of Equations over Finite Fields, with an Application to the Cryptanalysis of {K}ee{L}oq},
+ institution={University of Maryland Dissertation},
+ month={April},
+ year={2008},
+ note = {Ph.D. Thesis},
+}
+
+@inproceedings{Toyocrypt-nicolas-attack,
+ author={Nicolas T. Courtois},
+ title={Higher Order Correlation Attacks, {XL} algorithm and Cryptanalysis of {T}oyocrypt ({A}n updated version)},
+ booktitle={ICISC 2002},
+ series={LNCS},
+ volume={2587},
+ publisher={Springer},
+ year={2002},
+}
+
+@inproceedings{General-LFSR-attacks,
+ author={Nicolas T. Courtois and Willi Meier},
+ title={Algebraic Attacks on Stream Ciphers with Linear Feedback},
+ booktitle={Advances in Cryptology --- EUROCRYPT '03},
+ series={LNCS},
+ volume={2656},
+ pages={345–359},
+ publisher={Springer},
+ address = {Warsaw, Poland}
+}
+
+@inproceedings{Canniere06Trivium,
+ author = {Christophe De Canni{\`e}re},
+ title = {Trivium: A Stream Cipher Construction Inspired by Block Cipher Design Principles},
+ booktitle = {ISC},
+ year = {2006},
+ pages = {171-186},
+ ee = {http://dx.doi.org/10.1007/11836810_13},
+ crossref = {DBLP:conf/isw/2006},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/isw/2006,
+ editor = {Sokratis K. Katsikas and et al},
+ title = {Information Security, 9th International Conference, ISC 2006, Samos Island, Greece, August 30 - September 2, 2006, Proceedings},
+ booktitle = {ISC},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {4176},
+ year = {2006},
+ isbn = {3-540-38341-7},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+and
+Javier Lopez and
+Michael Backes and
+Stefanos Gritzalis and
+Bart Preneel
+
+@inproceedings{BiviumWithSATsolvers,
+ author = {Tobias Eibach and Enrico Pilz and Gunnar V{\"o}lkel},
+ title = {Attacking {B}ivium Using {SAT} Solvers},
+ booktitle = {SAT},
+ year = {2008},
+ pages = {63-76},
+ ee = {http://dx.doi.org/10.1007/978-3-540-79719-7_7},
+ crossref = {DBLP:conf/sat/2008},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/sat/2008,
+ editor = {Hans Kleine B{\"u}ning and Xishun Zhao},
+ title = {Theory and Applications of Satisfiability Testing - SAT 2008, 11th International Conference, SAT 2008, Guangzhou, China, May 12-15, 2008. Proceedings},
+ booktitle = {SAT},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {4996},
+ year = {2008},
+ isbn = {978-3-540-79718-0},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@TechReport{Bivium,
+ author={Havard Raddum},
+ title={Cryptanalytic results on {T}rivium},
+ institution = {ECRYPT Stream Cipher Project},
+ year={2006},
+ number={2006/039},
+ note = {\url{www.ecrypt.eu.org/stream/papersdir/2006/039.ps}},
+}
+
+@misc{using-equation-solvers,
+ author = {Havard Raddum and Igor Semaev},
+ title = {New Technique for Solving Sparse Equation Systems},
+ howpublished = {Cryptology ePrint Archive, Report 2006/475},
+ year = {2006},
+ note = {\url{http://eprint.iacr.org/}},
+}
+
+
+@TechReport{BiviumWithMiniSat,
+ author={Cameron McDonald and Chris Charnes and Josef Pieprzyk},
+ title={Attacking {B}ivium with {M}ini{S}at},
+ institution = {ECRYPT Stream Cipher Project},
+ year={2007},
+ number={2007/040}
+}
+
+@inproceedings{FaugereF5,
+ author = {Jean-Charles Faug\`{e}re},
+ title = {A new efficient algorithm for computing {G}r\"{o}bner bases without reduction to zero ({F}5)},
+ booktitle = {ISSAC '02},
+ year = {2002},
+ isbn = {1-58113-484-3},
+ pages = {75--83},
+ location = {Lille, France},
+ doi = {http://doi.acm.org/10.1145/780506.780516},
+ publisher = {ACM},
+ }
+ISSAC '02: Proceedings of the 2002 international symposium on Symbolic and algebraic computation
+address = {New York, NY, USA},
+
+
+@article{FaugereF4,
+ author = {Jean-Charles Faug\`{e}re},
+ title = {A new efficient algorithm for computing {G}r\"{o}bner bases ({F}4)},
+ journal = {Journal of Pure and Applied Algebra},
+ year = {1999},
+ month = {June},
+ pages = {61--88},
+ volume = {1},
+ number = {139},
+}
+
+@inproceedings{DismantlingMifare,
+ author = {Flavio D. Garcia and et al.},
+ title = {Dismantling {MIFARE} {C}lassic},
+ booktitle = {ESORICS},
+ year = {2008},
+ pages = {97-114},
+ ee = {http://dx.doi.org/10.1007/978-3-540-88313-5_7},
+ crossref = {DBLP:conf/esorics/2008},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+and
+Gerhard de Koning Gans and
+Ruben Muijrers and
+Peter van Rossum and
+Roel Verdult and
+Ronny Wichers Schreur and
+Bart Jacobs
+
+@proceedings{DBLP:conf/esorics/2008,
+ editor = {Sushil Jajodia and Javier L{\'o}pez},
+ title = {Computer Security - ESORICS 2008, 13th European Symposium on Research in Computer Security, M{\'a}laga, Spain, October 6-8, 2008. Proceedings},
+ booktitle = {ESORICS},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {5283},
+ year = {2008},
+ isbn = {978-3-540-88312-8},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@misc{Karsten-webpage-HiTag2,
+ author={Karsten Nohl},
+ title={Description of {H}i{T}ag2},
+ howpublished={Press release},
+ note= {\url{http://cryptolib.com/ciphers/hitag2/}},
+ month={March},
+ day = {12},
+ year={2008},
+}
+
+@InProceedings{Ouafi08Privacy,
+ address = {Berlin},
+ affiliation = {EPFL},
+ author = {Ouafi, Khaled and Phan, Raphael C.-W.},
+ booktitle = {Information {S}ecurity {P}ractice and {E}xperience, 4th {I}nternational {C}onference, {ISPEC} 2008},
+ location = {Sydney, Australia},
+ oai-id = {oai:infoscience.epfl.ch:126418},
+ oai-set = {conf; fulltext; fulltext-public},
+ pages = {263--277},
+ publisher = {Springer},
+ review = {REVIEWED},
+ series = {LNCS},
+ status = {PUBLISHED},
+ title = {Privacy of {R}ecent {RFID} {A}uthentication {P}rotocols},
+ unit = {LASEC},
+ year = {2008},
+ keywords = {RFID; authentication protocols, ; privacy; untraceability; provably secure},
+ details = {http://infoscience.epfl.ch/record/126418},
+ documenturl = {http://infoscience.epfl.ch/getfile.py?recid=126418&mode=best},
+}
+
+@INPROCEEDINGS{Ohkubo04Cryptographic,
+ author = {Miyako Ohkubo Koutarou and Koutarou Suzuki and Shingo Kinoshita},
+ title = {Cryptographic Approach to "Privacy-Friendly" Tags},
+ booktitle = {RFID Privacy Workshop},
+ year = {2003},
+ address = {MIT, Massachusetts, USA},
+ month = {November},
+}
+
+@article{Lamport81Password,
+ author = {Lamport,, Leslie},
+ title = {Password authentication with insecure communication},
+ journal = {Commun. ACM},
+ volume = {24},
+ number = {11},
+ year = {1981},
+ issn = {0001-0782},
+ pages = {770--772},
+ doi = {http://doi.acm.org/10.1145/358790.358797},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ }
+
+@InProceedings{OSK_Avoine,
+ affiliation = {EPFL},
+ author = {Avoine, Gildas and Oechslin, Philippe},
+ booktitle = {The 2nd {IEEE} {I}nternational {W}orkshop on {P}ervasive {C}omputing and {C}ommunication {S}ecurity - {P}er{S}ec 2005},
+ details = {http://infoscience.epfl.ch/record/99461},
+ documenturl = {http://infoscience.epfl.ch/getfile.py?recid=99461&mode=best},
+ keywords = {NCCR-MICS; NCCR-MICS/CL3},
+ location = {Kauai island, Hawaii, USA},
+ oai-id = {oai:infoscience.epfl.ch:99461},
+ oai-set = {conf; fulltext; fulltext-public},
+ pages = {110--114},
+ review = {REVIEWED},
+ status = {PUBLISHED},
+ title = {A {S}calable and {P}rovably {S}ecure {H}ash-{B}ased {RFID} {P}rotocol},
+ unit = {LASEC},
+ year = 2005
+}
+
+@inproceedings{Trade-off-Hellman,
+ author = {Hellman, Martin E.},
+ title = {A cryptanalytic time-memory trade off},
+ booktitle = {{IEEE} Transactions on Information Theory},
+ volume = {IT-26/4},
+ pages = {401--406},
+ year = {1980},
+}
+
+@inproceedings{Faster-crypto-time-memory,
+ author = {Oechslin, Philippe },
+ booktitle = {Advances in Cryptology --- CRYPTO 2003},
+ series = {LNCS},
+ volume = {2729},
+ publisher = {Springer},
+ pages = {617--630},
+ posted-at = {2008-07-07 15:11:06},
+ priority = {2},
+ title = {Making a Faster Cryptanalytic Time-Memory Trade-Off},
+ url = {http://www.springerlink.com/content/u9gxwd29p2tnx3wl},
+ year = {2003}
+}
+
+@inproceedings{Molnar04Keytrees,
+ address = {New York, NY, USA},
+ author = {Molnar, David and Wagner, David },
+ booktitle = {CCS '04: Proceedings of the 11th ACM conference on Computer and communications security},
+ citeulike-article-id = {202290},
+ doi = {10.1145/1030083.1030112},
+ isbn = {1581139616},
+ keywords = {libraries, privacy},
+ pages = {210--219},
+ posted-at = {2007-12-25 21:42:23},
+ priority = {5},
+ publisher = {ACM Press},
+ title = {Privacy and security in library {RFID}: issues, practices, and architectures},
+ url = {http://dx.doi.org/10.1145/1030083.1030112},
+ year = {2004}
+}
+
+@INPROCEEDINGS{NohlE-2008-sec,
+ author = {Nohl, Karsten and Evans, David},
+ title = {{Hiding in Groups: On the Expressiveness of Privacy Distributions}},
+ booktitle = {Proceedings of The Ifip Tc 11 23rd International Information Security Conference --- SEC 2008},
+ year = {2008},
+ editor = {},
+ volume = {278},
+ series = {LNCS},
+ pages = {1--15},
+ address = {Milan, Italia},
+ month = {September},
+ organization = {},
+ publisher = {Springer},
+ bibsource = {Information Security Group (GIS), UCL, Louvain-la-Neuve, Belgium},
+}
+
+@inproceedings{DBLP:conf/fse/Shamir08,
+ author = {Adi Shamir},
+ title = {{SQUASH} --- A New {MAC} with Provable Security Properties for Highly Constrained Devices Such as {RFID} Tags},
+ booktitle = {FSE},
+ year = {2008},
+ pages = {144-157},
+ ee = {http://dx.doi.org/10.1007/978-3-540-71039-4_9},
+ crossref = {DBLP:conf/fse/2008},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/fse/2008,
+ editor = {Kaisa Nyberg},
+ title = {Fast Software Encryption, 15th International Workshop, {FSE} 2008, Lausanne, Switzerland, February 10-13, 2008, Revised Selected Papers},
+ booktitle = {FSE},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {5086},
+ year = {2008},
+ isbn = {978-3-540-71038-7},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{Oren2008WIPRPublic,
+author = {Yossef Oren and Martin Feldhofer},
+title = {{WIPR} --- a Public Key Implementation on Two Grains of Sand},
+booktitle = {Workshop on RFID Security 2008},
+year = {2008},
+editor = {Sandra Dominikus},
+pages = {15 - 27},
+}
+
+@inproceedings{DBLP:conf/ctrsa/McLooneR07,
+ author = {M{\'a}ire McLoone and Matthew J. B. Robshaw},
+ title = {Public Key Cryptography and {RFID} Tags},
+ booktitle = {CT-RSA},
+ year = {2007},
+ pages = {372-384},
+ ee = {http://dx.doi.org/10.1007/11967668_24},
+ crossref = {DBLP:conf/ctrsa/2007},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/ctrsa/2007,
+ editor = {Masayuki Abe},
+ title = {Topics in Cryptology - CT-RSA 2007, The Cryptographers' Track at the RSA Conference 2007, San Francisco, CA, USA, February 5-9, 2007, Proceedings},
+ booktitle = {CT-RSA},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {4377},
+ year = {2006},
+ isbn = {3-540-69327-0},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+
+
+@proceedings{DBLP:conf/eurocrypt/91,
+ editor = {Donald W. Davies},
+ title = {Advances in Cryptology --- EUROCRYPT '91, Workshop on the Theory and Application of of Cryptographic Techniques, Brighton, UK, April 8-11, 1991, Proceedings},
+ booktitle = {Advances in Cryptology --- EUROCRYPT '91},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {547},
+ year = {1991},
+ isbn = {3-540-54620-0},
+}
+
+@inproceedings{DBLP:conf/eurocrypt/Girault91,
+ author = {Marc Girault},
+ title = {Self-Certified Public Keys},
+ booktitle = {Advances in Cryptology --- EUROCRYPT '91},
+ year = {1991},
+ pages = {490-497},
+ ee = {http://link.springer.de/link/service/series/0558/bibs/0547/05470490.htm},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{DBLP:conf/cardis/Girault00,
+ author = {Marc Girault},
+ title = {Low-Size Coupons for Low-Cost {IC} Cards},
+ booktitle = {CARDIS},
+ year = {2000},
+ pages = {39-50},
+ crossref = {DBLP:conf/cardis/2000},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/cardis/2000,
+ editor = {Josep Domingo-Ferrer and David Chan and Anthony Watson},
+ title = {Smart Card Research and Advanced Applications, Proceedings of the Fourth Working Conference on Smart Card Research and Advanced Applications, CARDIS 2000, September 20-22, 2000, Bristol, UK},
+ booktitle = {CARDIS},
+ publisher = {Kluwer},
+ series = {IFIP Conference Proceedings},
+ volume = {180},
+ year = {2000},
+ isbn = {0-7923-7953-5},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{Secure-human-ID,
+ author = {Hopper,, Nicholas J. and Blum,, Manuel},
+ title = {Secure Human Identification Protocols},
+ booktitle = {ASIACRYPT '01: Proceedings of the 7th International Conference on the Theory and Application of Cryptology and Information Security},
+ year = {2001},
+ isbn = {3-540-42987-5},
+ pages = {52--66},
+ publisher = {Springer-Verlag},
+ address = {London, UK},
+}
+
+@ARTICLE{Inherent-intracability,
+title={On the inherent intractability of certain coding problems (Corresp.)},
+author={ Berlekamp, E. and McEliece, R. and van Tilborg, H.},
+journal={Information Theory, IEEE Transactions on},
+year={1978},
+month={May},
+volume={24},
+number={3},
+pages={ 384-386},
+keywords={null Decoding, Linear codes},
+doi={},
+ISSN={0018-9448},
+}
+
+@article{Noise-tolerant-learning,
+ author = {Blum,, Avrim and Kalai,, Adam and Wasserman,, Hal},
+ title = {Noise-tolerant learning, the parity problem, and the statistical query model},
+ journal = {J. ACM},
+ volume = {50},
+ number = {4},
+ year = {2003},
+ issn = {0004-5411},
+ pages = {506--519},
+ doi = {http://doi.acm.org/10.1145/792538.792543},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
+
+
+@INPROCEEDINGS{To06anovel,
+ author = {Marc P. C. Fossorier and Miodrag J. Mihaljević and Hideki Imai and Yang Cui and Kanta Matsuura},
+ title = {A Novel Algorithm for Solving the {LPN} Problem and Its Applicatio to Security Evaluation of the {HB} Protocol for {RFID} Authentication},
+ booktitle = {INDOCRYPT},
+ editor = {Rana Barua and Tanja Lange},
+ volume = {4329},
+ series = {LNCS},
+ year = {2006},
+ pages = {48--62},
+ publisher = {Springer}
+}
+
+@INPROCEEDINGS{Levieil_animproved,
+ author = {Éric Levieil and Pierre-Alain Fouque},
+ title = {An improved {LPN} algorithm},
+ editor = {Roberto De Prisco and Moti Yung},
+ booktitle = {Security and Cryptography for Networks --- SCN},
+ volume = {4116},
+ series = {LNCS},
+ year = {2006},
+ pages = {348--359},
+ Publisher = {Springer Berlin / Heidelberg},
+ ISSN = {0302-9743},
+}
+
+@INPROCEEDINGS{HBpp,
+title={{HB}$^{++}$: a Lightweight Authentication Protocol Secure against Some Attacks},
+author={Bringer, J. and Chabanne, H. and Dottax, E.},
+booktitle={Security, Privacy and Trust in Pervasive and Ubiquitous Computing, 2006 --- SecPerU 2006},
+year={2006},
+month={June},
+volume={},
+number={},
+pages={28--33},
+doi={10.1109/SECPERU.2006.10},
+}
+
+@inproceedings{DBLP:conf/eurocrypt/GilbertRS08,
+ author = {Henri Gilbert and Matthew J. B. Robshaw and Yannick Seurin},
+ title = {{HB}$^{\mbox{\#}}$: Increasing the Security and Efficiency of {HB}$^{\mbox{+}}$},
+ booktitle = {Advances in Cryptology --- EUROCRYPT '08},
+ year = {2008},
+ pages = {361-378},
+ ee = {http://dx.doi.org/10.1007/978-3-540-78967-3_21},
+ crossref = {DBLP:conf/eurocrypt/2008},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/eurocrypt/2008,
+ editor = {Nigel P. Smart},
+ title = {Advances in Cryptology --- EUROCRYPT 2008, 27th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Istanbul, Turkey, April 13-17, 2008. Proceedings},
+ booktitle = {Advances in Cryptology --- EUROCRYPT '08},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {4965},
+ year = {2008},
+ isbn = {978-3-540-78966-6},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/fse/2001,
+ editor = {Mitsuru Matsui},
+ title = {Fast Software Encryption, 8th International Workshop, FSE 2001 Yokohama, Japan, April 2-4, 2001, Revised Papers},
+ booktitle = {FSE},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {2355},
+ year = {2002},
+ isbn = {3-540-43869-6},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@techreport{Rabin79Digitalized,
+ author = {Rabin, M. O.},
+ title = {Digitalized Signatures and Public-Key Functions as Intractable as Factorization},
+ year = {1979},
+ institution = {Massachusetts Institute of Technology},
+ address = {Cambridge, MA, USA},
+ }
+
+@article{HBmp,
+ author = {Munilla,, J. and Peinado,, A.},
+ title = {{HB}-{MP}: A further step in the HB-family of lightweight authentication protocols},
+ journal = {Comput. Netw.},
+ volume = {51},
+ number = {9},
+ year = {2007},
+ issn = {1389-1286},
+ pages = {2262--2267},
+ doi = {http://dx.doi.org/10.1016/j.comnet.2007.01.011},
+ publisher = {Elsevier North-Holland, Inc.},
+ address = {New York, NY, USA},
+ }
+
+@article{HBstar,
+ author={D.N. Duc and K. Kim},
+ title={Securing {HB}$^+$ Against {GRS} Man-in-the-Middle Attack},
+ journal={Institute of Electronics, Information and Communication Engineers, Symposium on Cryptography and Information, Security},
+ date = {January 23--26},
+ year = {2007},
+}
+
+@INPROCEEDINGS{OuafiOV-2008-asiacrypt,
+ author = {Ouafi, Khaled and Overbeck, Raphael and Vaudenay, Serge},
+ title = {On the Security of {HB\#} against a Man-in-the-Middle Attack},
+ booktitle = {Advances in Cryptology --- Asiacrypt 2008},
+ year = {2008},
+ editor = {},
+ volume = {5350},
+ series = {LNCS},
+ pages = {108--124},
+ address = {Melbourne, Australia},
+ month = {December},
+ organization = {},
+ publisher = {Springer},
+ bibsource = {Information Security Group (GSI), UCL, Louvain-la-Neuve, Belgium},
+}
+
+@INPROCEEDINGS{PRESENT,
+ author = {Bogdanov, Andrey and Knudsen, Lars Ramkilde and Leander, Gregor and Paar, Christof and Poschmann, Axel and Robshaw, Matthew J.B. and Seurin, Yannick and Vikkelsoe, C.},
+ title = {{PRESENT}: An Ultra-Lightweight Block Cipher},
+ booktitle = {Workshop on Cryptographic Hardware and Embedded Systems --- CHES 2007},
+ year = {2007},
+ editor = {Paillier, Pascal and Verbauwhede, Ingrid},
+ volume = {4727},
+ series = {LNCS},
+ pages = {450--466},
+ address = {Vienna, Austria},
+ month = {September},
+ organization = {},
+ publisher = {Springer-Verlag},
+ bibsource = {Information Security Group (GSI), UCL, Louvain-la-Neuve, Belgium},
+}
+
+@INPROCEEDINGS{ChoiKKK-2006-isce,
+ author = {Choi, Yongje and Kim, Mooseop and Kim, Taesung and Kim, Howon},
+ title = {Low power implementation of {SHA}-1 algorithm for {RFID} system},
+ booktitle = {IEEE Tenth International Symposium on Consumer Electronics --- ISCE '06},
+ year = {2006},
+ editor = {},
+ volume = {},
+ series = {},
+ pages = {1--5},
+ address = {St.Petersburg, Russia},
+ month = {September},
+ organization = {},
+ publisher = {},
+ bibsource = {Information Security Group (GSI), UCL, Louvain-la-Neuve, Belgium},
+}
+
+@INPROCEEDINGS{DES-RFID-implement,
+ author = {Axel Poschmann and Gregor Le and Kai Schramm and Christof Paar},
+ title = {A Family of Light-Weight Block Ciphers Based on {DES} Suited for {RFID} Applications},
+ booktitle = {Proceedings of FSE 2007, LNCS},
+ year = {2006},
+ publisher = {Springer-Verlag}
+}
+
+@article{4253019,
+title={Strong Crypto for {RFID} Tags - A Comparison of Low-Power Hardware Implementations},
+author={Feldhofer, M. and Wolkerstorfer, J.},
+journal={Circuits and Systems, 2007. ISCAS 2007. IEEE International Symposium on},
+year={2007},
+month={May},
+volume={},
+number={},
+pages={1839-1842},
+keywords={cryptographic protocols, radiofrequency identificationAES-128, ECC-192, MD5, SHA-1, SHA-256, implementation efficiency, passive RFID tags, security protocols, standardized cryptographic algorithms, strong cryptography},
+doi={10.1109/ISCAS.2007.378272},
+ISSN={},
+}
+
+@techreport{PUF-optical,
+ author= {P. Ravinkanth},
+ title= {Physical One-Way Functions},
+ note = {Ph.D. Thesis},
+ institution = {MIT},
+ year={2001}
+}
+
+@inproceedings{PUF-silicon,
+ author={B. Gassend and D. Clarke and M. van Dijk and S. Devadas},
+ title = {Controlled Physical Random Functions},
+ booktitle = {Proceedings of the 18th Annual Computer Security Applications Conference --- ACSAC '02},
+ year = {2002},
+ ISBN = {0-7695-1828-1},
+ page = {149},
+ publisher = {IEEE},
+}
+
+@article{PUF-circ-secret-key,
+ author = {D. Lim and J. W. Lee and B. Gassend and G. E. Suh and M. van Dijk and S. Devadas},
+ title = {Extracting Secret Keys From Integrated Circuits},
+ journal = {IEEE Transactions on Very Large Scale Integration (VLSI) Systems},
+ pages = {1200--1205},
+ year = {2005},
+ issue = {13 (10)},
+}
+
+
+@INPROCEEDINGS{Li99equivalencyreasoning,
+ author = {Chu Min Li},
+ title = {Equivalency reasoning to solve a class of hard {SAT} problems},
+ booktitle = {Information Processing Letters},
+ year = {1999},
+ pages = {76--1}
+}
+
+@INPROCEEDINGS{Silva96conflictanalysis,
+ author = {Joo P. Marques and Silva Karem and A. Sakallah},
+ title = {Conflict analysis in search algorithms for propositional satisfiability},
+ booktitle = {Proc. of the IEEE Intl. Conf. on Tools with Artificial Intelligence},
+ year = {1996}
+}
+
+@article{Chaff01,
+ author = {Sharad Malik and Ying Zhao and Conor F. Madigan and Lintao Zhang and Matthew W. Moskewicz},
+ title = {Chaff: Engineering an Efficient {SAT} Solver},
+ journal ={Design Automation Conference},
+ year = {2001},
+ pages = {530-535},
+ doi = {http://doi.ieeecomputersociety.org/10.1109/DAC.2001.935565},
+ publisher = {IEEE Computer Society},
+ address = {Los Alamitos, CA, USA},
+}
+volume = {0},
+isbn = {},
+
+@article{visualizingDPLL,
+ author = {Sinz, Carsten},
+ title = {Visualizing {SAT} Instances and Runs of the {DPLL} Algorithm},
+ journal = {J. Autom. Reason.},
+ volume = {39},
+ number = {2},
+ year = {2007},
+ issn = {0168-7433},
+ pages = {219--243},
+ doi = {http://dx.doi.org/10.1007/s10817-007-9074-1},
+ publisher = {Kluwer Academic Publishers},
+ address = {Hingham, MA, USA},
+ }
+
+@inproceedings{nicolas.linear_feedback,
+ author={Nicolas T. Courtois},
+ title={Fast Algebraic Attacks on Stream Ciphers with Linear Feedback},
+ booktitle={Advances in Cryptology --- {CRYPTO} 2003},
+ year={2003},
+ pages={176-194},
+ volume={2729/2003},
+ series={LNCS},
+ publisher={Springer},
+}
+
+@misc{Karsten-webpage-Cyrpto-1,
+ author={Karsten Nohl},
+ title={Cryptanalysis of {C}rypto-1},
+ howpublished={Press release},
+ month={March},
+ day = {12},
+ year={2008},
+ note= {\url{http://www.cs.virginia.edu/~kn5f/Mifare.Cryptanalysis.htm}}
+}
+
+@Misc{Radboud-Mifare-press,
+ author = {{Digital {S}ecurity group, {R}adboud {U}niversity {N}ijmegen}},
+ title = {Security Flaw in {M}ifare {C}lassic},
+ howpublished = {Press release},
+ month = {March},
+ day = {12},
+ year = {2008},
+ note = {\url{http://www.ru.nl/english/general/radboud_university/vm/security_flaw_in/}},
+}
+
+@ARTICLE{Massacci00logicalcryptanalysis,
+ author = {Fabio Massacci and Laura Marraro},
+ title = {Logical cryptanalysis as a {SAT}-problem: Encoding and analysis},
+ journal = {Journal of Automated Reasoning},
+ year = {2000},
+ volume = {24},
+ pages = {165--203}
+}
+
+@article{Monte-Carlo-method,
+ abstract = {We shall present here the motivation and a general description of a method dealing with a class of problems in mathematical physics. The method is, essentially, a statistical approach to the study of differential equations, or more generally, of integro-differential equations that occur in various branches of the natural sciences.},
+ author = {Metropolis, Nicholas and Ulam, S. },
+ citeulike-article-id = {1886002},
+ doi = {10.2307/2280232},
+ journal = {Journal of the American Statistical Association},
+ keywords = {random, sampling},
+ number = {247},
+ pages = {335--341},
+ posted-at = {2009-04-12 22:32:37},
+ priority = {2},
+ title = {The {M}onte {C}arlo Method},
+ url = {http://dx.doi.org/10.2307/2280232},
+ volume = {44},
+ year = {1949}
+}
+
+@article{Rabin-primality-test,
+ author = {Rabin, Michael O. },
+ citeulike-article-id = {1505894},
+ doi = {10.1016/0022-314X(80)90084-0},
+ journal = {J. Number Theory},
+ mrnumber = {MR566880},
+ number = {1},
+ pages = {128--138},
+ posted-at = {2007-07-27 00:11:40},
+ priority = {2},
+ title = {Probabilistic algorithm for testing primality},
+ url = {http://dx.doi.org/10.1016/0022-314X(80)90084-0},
+ volume = {12},
+ year = {1980}
+}
+
+@article{Mersenne-Twister,
+ address = {New York, NY, USA},
+ author = {Matsumoto, Makoto and Nishimura, Takuji },
+ citeulike-article-id = {611171},
+ doi = {10.1145/272991.272995},
+ issn = {1049-3301},
+ journal = {ACM Trans. Model. Comput. Simul.},
+ keywords = {algorithm},
+ month = {January},
+ number = {1},
+ pages = {3--30},
+ posted-at = {2008-10-26 00:03:42},
+ priority = {0},
+ publisher = {ACM Press},
+ title = {Mersenne twister: a 623-dimensionally equidistributed uniform pseudo-random number generator},
+ url = {http://dx.doi.org/10.1145/272991.272995},
+ volume = {8},
+ year = {1998}
+}
+
+@inproceedings{L'Ecuyer98randomnumber,
+ author = {Pierre L'Ecuyer and Peter Hellekalek},
+ title = {Random Number Generators: Selection Criteria and Testing},
+ booktitle = {Random and Quasi-Random Point Sets},
+ series = {Lecture Notes in Statistics},
+ volume = {138},
+ publisher = {Springer-Verlag},
+ address = {New York},
+ pages = {223--266},
+ year = {1998},
+}
+
+@inproceedings{DBLP:conf/sat/SinzD05,
+ author = {Carsten Sinz and Edda-Maria Dieringer},
+ title = {{DP}vis --- {A} Tool to Visualize the Structure of {SAT} Instances},
+ booktitle = {SAT},
+ year = {2005},
+ pages = {257-268},
+ ee = {http://dx.doi.org/10.1007/11499107_19},
+ crossref = {DBLP:conf/sat/2005},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+
+@article{gomes00heavytailed,
+ author = {Carla P. Gomes and Bart Selman and Nuno Crato and Henry A. Kautz},
+ title = {Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems},
+ journal = {Journal of Automated Reasoning},
+ volume = {24},
+ number = {1/2},
+ pages = {67--100},
+ year = {2000},
+ url = {citeseer.ist.psu.edu/article/gomes99heavytailed.html}
+}
+
+@article{Mandelbrot60Pareto,
+ author = {Benoît B. Mandelbrot},
+ title = {The Pareto-Lévy law and the distribution of income},
+ journal = {Internat. Econom. Rev.},
+ volume = {1},
+ year = {1960},
+ pages = {79--106}
+}
+
+@inproceedings{Moura07tutorial,
+ author = {Leonardo de Moura, Bruno Dutertre and Natarajan Shankar},
+ title = {A Tutorial on Satisfiability Modulo Theories},
+ series = {LNCS},
+ publisher = {Springer Berlin / Heidelberg},
+ issn = {0302-9743},
+ volume = {4590/2007},
+ year = {2007},
+ isbn = {978-3-540-73367-6},
+ pages = {20--36},
+ booktitle = {Computer Aided Verification},
+}
+ doi = {10.1007/978-3-540-73368-3},
+
+@article{Karnaugh53Logic,
+ author = {Karnaugh, Maurice},
+ year = {1953},
+ month = {November},
+ title = {The Map Method for Synthesis of Combinational Logic Circuits},
+ journal = {Transactions of American Institute of Electrical Engineers part I},
+ volume = {72},
+ number = {9},
+ pages = {593--599},
+}
+
+@inproceedings{Li00Integrating,
+ author = {Li, Chu Min},
+ title = {Integrating Equivalency Reasoning into Davis-Putnam Procedure},
+ booktitle = {Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence},
+ year = {2000},
+ isbn = {0-262-51112-6},
+ pages = {291--296},
+ publisher = {AAAI Press / The MIT Press},
+}
+
+@article{Warners99TwoPhase,
+ author = {Joost P. Warners and Hans Van Maaren},
+ title = {A Two Phase Algorithm for Solving a Class of Hard Satisfiability Problems},
+ journal = {Operations Research Letters},
+ year = {1999},
+ volume = {23},
+ number = {3--5},
+ pages = {81--88}
+}
+
+@inproceedings{Massacci00Taming,
+ author = {Peter Baumgartner and Fabio Massacci},
+ title = {The Taming of the {(X)OR}},
+ series = {LNCS},
+ publisher = {Springer Berlin / Heidelberg},
+ ISSN = {0302-9743},
+ volume = {1861/2000},
+ booktitle = {Computational Logic — CL 2000},
+ doi = {10.1007/3-540-44957-4},
+ year = {2000},
+ isbn = {978-3-540-67797-0},
+ pages = {508--522},
+}
+
+@inproceedings{Massacci99Using,
+ author = {Fabio Massacci},
+ title = {Using {W}alk-{SAT} and {R}el-sat for cryptographic key search},
+ booktitle = {Proc. of IJCAI-99},
+ year = {1999},
+ editor = {Morgan Kaufmann},
+ pages = {290--295},
+}
+
+@inproceedings{Girault04Public,
+author = {Marc Girault and David Lefranc},
+title = {Public Key Authentication with One (Online) Single Addition},
+series = {LNCS},
+bublisher = {Springer Berlin / Heidelberg},
+ISSN = {0302-9743},
+volume = {3156/2004},
+booktitle = {Cryptographic Hardware and Embedded Systems - CHES 2004},
+doi ={10.1007/b99451},
+year = {2004},
+isbn = {978-3-540-22666-6},
+pages = {967--984}
+}
+
+@article{Hsieh72OnOptimal,
+ author = {Hsieh, H. Y. and Ghausi, M. S.},
+ title = {On optimal-pivoting algorithms in sparse matrices},
+ journal = {IEEE Trans. Circuit Theory},
+ volume = {CT-19},
+ pages = {93--96},
+ month = {January},
+ year = {1972}
+}
+
+@article{HerasetalJAIR2008,
+ author = {Federico Heras and Javier Larrosa and Albert Oliveras},
+ title = {{MiniMaxSAT: An efficient Weighted Max-SAT Solver}},
+ journal = {Journal of Artificial Intelligence Research},
+ volume = {31},
+ year = {2008},
+ pages = {1--32}
+ }
+
+@techreport{Wieringa07MiniMarch,
+ title = {{M}ini{M}arch --- {E}mbedding lookahead direction heuristics in a conflict driven solver},
+ author = {Siert Wieringa},
+ institution = {Technische Universiteit Delft},
+ note = {Research Report},
+ year = {2007},
+ url = {http://www.st.ewi.tudelft.nl/sat/theses/minimarch.pdf},
+}
+
+techreport{OSI-MIT-Licence,
+url = {http://www.opensource.org/licenses/mit-license.php}
+
+
+@techreport{eStream,
+ title = {The e{STREAM} Portfolio},
+ author = {Steve Babbage and Christophe De Canniere and Anne Canteaut and Carlos Cid and Henri Gilbert and Thomas Johansson and Christof Paar and Matthew Parker and Bart Preneel and Vincent Rijmen and Matt Robshaw and Hongjun Wu},
+ url = {http://www.ecrypt.eu.org/stream/portfolio.pdf},
+ institution = {eStream Project},
+ year = {2008},
+ month = {September},
+ day = {8},
+}
+
+@techreport{Kibria08MiniSat,
+ author = {Raihan Kibria},
+ title = {Midi{S}AT - {A}n extension of {M}ini{SAT}},
+ institution = {Department of Electrical and Computer Engineering, Darmstadt University of Technology},
+ year = {2005},
+ month = {April},
+ day = {26},
+ url = {www.lri.fr/~simon/contest/results/descriptions/solvers/midisat_static.pdf},
+}
+
+@incollection{DaemenR05Rijndael,
+ author = {Joan Daemen and Vincent Rijmen},
+ title = {Rijndael/AES},
+ booktitle = {Encyclopedia of Cryptography and Security},
+ year = {2005},
+ ee = {http://dx.doi.org/10.1007/0-387-23483-7_358},
+ crossref = {DBLP:reference/crypt/2005},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@book{DBLP:reference/crypt/2005,
+ editor = {Henk C. A. van Tilborg},
+ title = {Encyclopedia of Cryptography and Security},
+ publisher = {Springer},
+ year = {2005},
+ isbn = {978-0-387-23473-1},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@article{Strassen69Gaussian,
+ author = {Volker Strassen},
+ title = {Gaussian Elimination is Not Optimal},
+ journal = {Numerische Mathematik},
+ volume = {13},
+ pages = {354--356},
+ year = {1969}
+}
+
+@techreport{Crawford94TheMinimal,
+ author = {Crawford, J. M. and Kearns, M. J. and Shapire, R. E.},
+ title = {The Minimal Disagreement Parity Problem as a Hard Satisfiability Problem},
+ institution = {Computational Intelligence Research Laboratory and {AT\&T} {B}ell {L}abs},
+ month = {February},
+ year = {1994},
+}
+
+@inproceedings{OuafiV09Smashing,
+ author = {Khaled Ouafi and Serge Vaudenay},
+ title = {Smashing {SQUASH}-0},
+ volume = {5479},
+ crossref = {DBLP:conf/eurocrypt/2009},
+}
+
+@inproceedings{ShamirRFIDSecLecture,
+author = {Adi Shamir},
+title = {{SQUASH}: {A} new one-way hash function with provable security properties for higley contrained devices such as {RFID} tags},
+booktitle = {Invited lecture to the RFID Securty 2007 Workshop},
+year = {2007},
+}
+
+@misc{DES77,
+ author = {{National Bureau of Standards}},
+ year = {1977},
+ title = {Data {E}ncryption {S}tandard},
+ institution = {U. S. Department of Commerce, National Bureau of Standards, Standards Publication (FIPS PUB) 46},
+ address = {Washington, DC},
+}s
+
+@INPROCEEDINGS{Tsudik06Yet,
+ author = {Tsudik, Gene},
+ title = {{YA-TRAP}: Yet Another Trivial {RFID} Authentication Protocol},
+ booktitle = {International Conference on Pervasive Computing and Communications --- PerCom 2006},
+ year = {2006},
+ editor = {},
+ volume = {},
+ series = {},
+ pages = {640--643},
+ address = {Pisa, Italy},
+ month = {March},
+ organization = {IEEE},
+ publisher = {IEEE Computer Society Press},
+ bibsource = {Information Security Group (GSI), UCL, Louvain-la-Neuve, Belgium},
+}
+
+
+@INPROCEEDINGS{Conti07RIPP,
+ author = {Conti, Mauro and Pietro, Roberto~Di and Mancini, Luigi~Vincenzo and Spognardi, Angelo},
+ title = {{RIPP-FS}: an {RFID} Identification, Privacy Preserving Protocol with Forward Secrecy},
+ booktitle = {International Workshop on Pervasive Computing and Communication Security --- PerSec '07},
+ year = {2007},
+ editor = {},
+ volume = {},
+ series = {},
+ pages = {229--234},
+ address = {New York City, New York, USA},
+ month = {March},
+ organization = {IEEE},
+ publisher = {IEEE Computer Society Press},
+ bibsource = {Information Security Group (GSI), UCL, Louvain-la-Neuve, Belgium},
+}
+
+@INPROCEEDINGS{Burmester06Provably,
+ author = {Burmester, Mike and Le, Tri van and Medeiros, Breno de},
+ title = {Provably Secure Ubiquitous Systems: Universally Composable {RFID} Authentication Protocols},
+ booktitle = {Conference on Security and Privacy for Emerging Areas in Communication Networks --- SecureComm '06},
+ year = {2006},
+ editor = {},
+ volume = {},
+ series = {},
+ pages = {},
+ address = {Baltimore, Maryland, USA},
+ month = {August-September},
+ organization = {IEEE},
+ publisher = {},
+ bibsource = {Information Security Group (GSI), UCL, Louvain-la-Neuve, Belgium},
+}
+
+@misc{ISO14443-standard,
+ author = {ISO/IEC},
+ title = {14443-3 --- {I}dentification cards -- {C}ontactless integrated circuit(s) cards -- {P}roximity cards -- {P}art 3: {I}nitialization and anticollision},
+ year = {2001, Stage: 90.92 --- 2007-12-11},
+ institution = {International Organization for Standardization},
+ address = {Geneva, Switzerland},
+ url = {http://www.isotopicmaps.org/sam/sam-model/YYYY-MM-DD/},
+}
+
+@INPROCEEDINGS{Bailey05Shoehorning,
+ author = {Bailey, Daniel and Juels, Ari},
+ title = {{Shoehorning Security into the EPC Standard}},
+ booktitle = {International Conference on Security in Communication Networks --- SCN 2006},
+ year = {2006},
+ editor = {De~Prisco, Roberto and Yung, Moti},
+ volume = {4116},
+ series = {LNCS},
+ pages = {303--320},
+ address = {Maiori, Italy},
+ month = {September},
+ organization = {},
+ publisher = {Springer-Verlag},
+ bibsource = {Information Security Group (GSI), UCL, Louvain-la-Neuve, Belgium},
+}
+
+@INPROCEEDINGS{Soos08Analysing,
+ author = {Soos, Mate},
+ title = {{Analysing the {M}olva and {D}i {P}ietro Private {RFID} Authentication Scheme}},
+ booktitle = {Workshop on RFID Security --- RFIDSec'08},
+ year = {2008},
+ editor = {},
+ volume = {},
+ series = {},
+ pages = {},
+ address = {Budapest, Hungary},
+ month = {July},
+ organization = {},
+ publisher = {},
+}
+
+@inproceedings{DBLP:conf/ccs/BurmesterMM08,
+ author = {Mike Burmester and Breno de Medeiros and Rossana Motta},
+ title = {Robust, anonymous {RFID} authentication with constant key-lookup},
+ booktitle = {ASIACCS},
+ year = {2008},
+ pages = {283-291},
+ ee = {http://doi.acm.org/10.1145/1368310.1368351},
+ crossref = {DBLP:conf/ccs/2008asia},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/ccs/2008asia,
+ editor = {Masayuki Abe and Virgil D. Gligor},
+ title = {Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security, ASIACCS 2008, Tokyo, Japan, March 18-20, 2008},
+ booktitle = {ASIACCS},
+ publisher = {ACM},
+ year = {2008},
+ isbn = {978-1-59593-979-1},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@INPROCEEDINGS{Blass09Ff,
+ author = {Blass, Erik-Oliver and Kurmus, Anil and Molva, Refik and Noubir, Guevara and Shikfa, Abdullatif},
+ title = {{The {F}f-Family of Protocols for {RFID}-Privacy and Authentication}},
+ booktitle = {Workshop on RFID Security --- RFIDSec'09},
+ year = {2009},
+ editor = {},
+ volume = {},
+ series = {},
+ pages = {},
+ address = {Leuven, Belgium},
+ month = {July},
+ organization = {},
+ publisher = {},
+ bibsource = {Information Security Group (GSI), UCL, Louvain-la-Neuve, Belgium},
+}
+
+@inproceedings{DBLP:conf/cardis/CastellucciaA06,
+ author = {Claude Castelluccia and Gildas Avoine},
+ title = {Noisy Tags: {A} Pretty Good Key Exchange Protocol for {RFID} Tags},
+ booktitle = {CARDIS},
+ year = {2006},
+ pages = {289-299},
+ ee = {http://dx.doi.org/10.1007/11733447_21},
+ crossref = {DBLP:conf/cardis/2006},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/cardis/2006,
+ editor = {Josep Domingo-Ferrer and
+ Joachim Posegga and
+ Daniel Schreckling},
+ title = {Smart Card Research and Advanced Applications, 7th IFIP
+ WG 8.8/11.2 International Conference, CARDIS 2006, Tarragona,
+ Spain, April 19-21, 2006, Proceedings},
+ booktitle = {CARDIS},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {3928},
+ year = {2006},
+ isbn = {3-540-33311-8},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+
+@inproceedings{DBLP:conf/ches/SavryPDRR07,
+ author = {O. Savry and F. Pebay-Peyroula and F. Dehmas and G. Robert and J. Reverdy},
+ title = {{RFID} Noisy Reader --- {H}ow to Prevent from Eavesdropping on the Communication?},
+ booktitle = {CHES},
+ year = {2007},
+ pages = {334-345},
+ ee = {http://dx.doi.org/10.1007/978-3-540-74735-2_23},
+ crossref = {DBLP:conf/ches/2007},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/ches/2007,
+ editor = {Pascal Paillier and Ingrid Verbauwhede},
+ title = {Cryptographic Hardware and Embedded Systems --- {CHES} 2007,
+ 9th International Workshop, Vienna, Austria, September 10-13,
+ 2007, Proceedings},
+ booktitle = {CHES},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {4727},
+ year = {2007},
+ isbn = {978-3-540-74734-5},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@article{Hancke07Modulating,
+ author = {G. Hancke},
+ title = {Modulating a noisy carrier signal for eavesdropping-resistant {HF RFID}},
+ journal = {e\&i --- Elektrotechnik und Informationstechnik},
+ year = {2007},
+ volume = {124},
+ number = {11},
+ month = {November},
+ pages = {404--408},
+ publisher = {Springer Wien},
+ ISSN = {0932-383X},
+ DOI = {10.1007/s00502-007-0479-7}
+}
+
+@inproceedings{1423361,
+ author = {Babbage, Steve and Dodd, Matthew},
+ title = {The {MICKEY} Stream Ciphers},
+ booktitle = {New Stream Cipher Designs: The e{STREAM} Finalists},
+ year = {2008},
+ isbn = {978-3-540-68350-6},
+ pages = {191--209},
+ doi = {http://dx.doi.org/10.1007/978-3-540-68351-3_15},
+ publisher = {Springer-Verlag},
+ address = {Berlin, Heidelberg},
+ }
+
+@inproceedings{DBLP:conf/wistp/DeursenMR08,
+ author = {Ton van Deursen and Sjouke Mauw and Sasa Radomirovic},
+ title = {Untraceability of {RFID} Protocols},
+ booktitle = {WISTP},
+ year = {2008},
+ pages = {1-15},
+ ee = {http://dx.doi.org/10.1007/978-3-540-79966-5_1},
+ crossref = {DBLP:conf/wistp/2008},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/wistp/2008,
+ editor = {Jose Antonio Onieva and Damien Sauveron and Serge Chaumette and Dieter Gollmann and Constantinos Markantonakis},
+ title = {Information Security Theory and Practices. Smart Devices, Convergence and Next Generation Networks, Second {IFIP WG} 11.2 International Workshop, {WISTP} 2008, Seville, Spain, May 13-16, 2008. Proceedings},
+ booktitle = {WISTP},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {5019},
+ year = {2008},
+ isbn = {978-3-540-79965-8},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@misc{A51,
+ author = {Ross Anderson},
+ title = {A5 (was: Hacking digital phones)},
+ howpublished = {Newsgroup Communication},
+ year = {1994},
+}
+
+@inproceedings{DBLP:conf/cardis/GansHG08,
+ author = {Gerhard de Koning Gans and Jaap-Henk Hoepman and Flavio D. Garcia},
+ title = {A Practical Attack on the {MIFARE} {C}lassic},
+ booktitle = {CARDIS},
+ year = {2008},
+ pages = {267-282},
+ ee = {http://dx.doi.org/10.1007/978-3-540-85893-5_20},
+ crossref = {DBLP:conf/cardis/2008},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/cardis/2008,
+ editor = {Gilles Grimaud and Fran\c{c}ois-Xavier Standaert},
+ title = {Smart Card Research and Advanced Applications, 8th IFIP WG 8.8/11.2 International Conference, CARDIS 2008, London, UK, September 8-11, 2008. Proceedings},
+ booktitle = {CARDIS},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {5189},
+ year = {2008},
+ isbn = {978-3-540-85892-8},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{DBLP:conf/ima/CourtoisB07,
+ author = {Nicolas T. Courtois and Gregory V. Bard},
+ title = {Algebraic Cryptanalysis of the {D}ata {E}ncryption {S}tandard},
+ booktitle = {{IMA} Int. Conf.},
+ year = {2007},
+ pages = {152-169},
+ ee = {http://dx.doi.org/10.1007/978-3-540-77272-9_10},
+ crossref = {DBLP:conf/ima/2007},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/ima/2007,
+ editor = {Steven D. Galbraith},
+ title = {Cryptography and Coding, 11th IMA International Conference, Cirencester, UK, December 18-20, 2007, Proceedings},
+ booktitle = {IMA Int. Conf.},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {4887},
+ year = {2007},
+ isbn = {978-3-540-77271-2},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@book{Bard-algebraic,
+ title = {Algebraic Cryptanalysis},
+ author = {Gregory V. Bard},
+ year = {2009},
+ pages = {392},
+ volume = {XXXIV},
+ series = {Security and Cryptology},
+ ISBN = {978-0-387-88756-2},
+ publisher = {Springer},
+}
+
+@inproceedings{Graphviz,
+ author = {John Ellson and Emden R. Gansner and Eleftherios Koutsofios and Stephen C. North and Gordon Woodhull},
+ year = {2001},
+ title = {Graphviz --- open source graph drawing tools},
+ pages = {483--484},
+ crossref = {DBLP:conf/gd/2001},
+}
+
+@proceedings{DBLP:conf/gd/2001,
+ editor = {Petra Mutzel and Michael J{\"u}nger and Sebastian Leipert},
+ title = {Graph Drawing, 9th International Symposium, GD 2001 Vienna, Austria, September 23--26, 2001, Revised Papers},
+ booktitle = {Graph Drawing},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {2265},
+ year = {2002},
+ isbn = {3-540-43309-0},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{Borghoff09Mixed,
+ booktitle = {WEWoRC --- Western European Workshop on Research in Cryptology},
+ title = {Bivium as a Mixed-0-1 Linear Programming Problem},
+ author = {Julia Borghoff and Lars R. Knudsen and Mathias Stolpe},
+ month = {July},
+ year = {2009},
+ address = {Graz, Austria},
+}
+
+@inproceedings{DBLP:conf/eurocrypt/DinurS09,
+ author = {Itai Dinur and Adi Shamir},
+ title = {Cube Attacks on Tweakable Black Box Polynomials},
+ booktitle = {EUROCRYPT},
+ year = {2009},
+ pages = {278--299},
+ ee = {http://dx.doi.org/10.1007/978-3-642-01001-9_16},
+ crossref = {DBLP:conf/eurocrypt/2009},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/eurocrypt/2009,
+ editor = {Antoine Joux},
+ title = {Advances in Cryptology --- EUROCRYPT 2009, 28th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Cologne, Germany, April 26--30, 2009. Proceedings},
+ booktitle = {EUROCRYPT},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {5479},
+ year = {2009},
+ isbn = {978-3-642-01000-2},
+ ee = {http://dx.doi.org/10.1007/978-3-642-01001-9},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@book{eStreamFinalists,
+ title = {The e{STREAM} Finalists},
+ editor = {Matthew Robshaw and Olivier Billet},
+ series = {LNCS},
+ subseries = {Security and Cryptology},
+ volume = {4986},
+ year = {2008},
+ pages = {295},
+ isbn = {978-3-540-68350-6},
+ publisher = {Springer},
+}
+
+@article{diffie76new,
+ author = "Whitfield Diffie and Martin E. Hellman",
+ title = "New Directions in Cryptography",
+ journal = "IEEE Transactions on Information Theory",
+ volume = "IT-22",
+ number = "6",
+ pages = "644--654",
+ date = "November 1976",
+ year = "1976",
+ url = "citeseer.ist.psu.edu/diffie76new.html"
+}
+
+@ARTICLE{Rivest78amethod,
+ author = {Ron L. Rivest and Adi Shamir and Leonard Max Adleman},
+ title = {A Method for Obtaining Digital Signatures and Public-Key Cryptosystems},
+ journal = {Communications of the ACM},
+ year = {1978},
+ volume = {21},
+ pages = {120--126}
+}
+
+@inproceedings{Pfizmann01Anonimity,
+ author = {Andreas Pfitzmann and Marit Köhntopp},
+ title = {Anonymity, Unobservability, and Pseudonymity --- {A} Proposal for Terminology},
+ series = {LNCS},
+ publisher = {Springer Berlin / Heidelberg},
+ issn = {0302-9743},
+ volume = {2009},
+ year = {2001},
+ booktitle = {Designing Privacy Enhancing Technologies},
+ doi = {10.1007/3-540-44702-4},
+ isbn = {978-3-540-41724-8},
+ pages = {1--9},
+}
+
+@misc{Bard07efficientmethods,
+ author = {Gregory V. Bard and Nicolas T. Courtois and Chris Jefferson},
+ title = {Efficient Methods for Conversion and Solution of Sparse Systems of Low-Degree Multivariate Polynomials over {GF}(2) via {SAT}-Solvers},
+ howpublished = {Cryptology ePrint Archive, Report 2007/024, \url{http://eprint.iacr.org/2007/024}},
+ year = {2007},
+ organization = {IACR},
+}
+
+@inproceedings{DBLP:conf/sat/SoosNC09,
+ author = {Mate Soos and
+ Karsten Nohl and
+ Claude Castelluccia},
+ title = {Extending {SAT} Solvers to Cryptographic Problems},
+ booktitle = {SAT},
+ year = {2009},
+ pages = {244--257},
+ ee = {http://dx.doi.org/10.1007/978-3-642-02777-2_24},
+ crossref = {DBLP:conf/sat/2009},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{DBLP:conf/cav/GaneshD07,
+ author = {Vijay Ganesh and
+ David L. Dill},
+ title = {A Decision Procedure for Bit-Vectors and Arrays},
+ booktitle = {CAV},
+ year = {2007},
+ pages = {519-531},
+ ee = {http://dx.doi.org/10.1007/978-3-540-73368-3_52},
+ crossref = {DBLP:conf/cav/2007},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/cav/2007,
+ editor = {Werner Damm and
+ Holger Hermanns},
+ title = {Computer Aided Verification, 19th International Conference,
+ CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings},
+ booktitle = {CAV},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {4590},
+ year = {2007},
+ isbn = {978-3-540-73367-6},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@misc{Logic2CNF,
+ author = {Edd Barrett},
+ title = {Logic2{CNF} Logic Solver and Converter},
+ note = {\url{http://projects.cs.kent.ac.uk/projects/logic2cnf/trac/wiki/WikiStart}},
+ year = {2010},
+ month = {March},
+}
+
+@misc{CryptoMiniSat,
+ author = {Mate Soos},
+ title = {Crypto{M}ini{S}at --- a {SAT} solver for cryptographic problems},
+ note = {\url{http://planete.inrialpes.fr/~soos/CryptoMiniSat/index.html}},
+ year = {2009},
+}
+
+@inproceedings{DBLP:conf/sat/EenB05,
+ author = {Niklas E{\'e}n and
+ Armin Biere},
+ title = {Effective Preprocessing in {SAT} Through Variable and Clause
+ Elimination},
+ booktitle = {SAT},
+ year = {2005},
+ pages = {61-75},
+ ee = {http://dx.doi.org/10.1007/11499107_5},
+ crossref = {DBLP:conf/sat/2005},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{glucose,
+ author = {Gilles Audemard and Laurent Simon},
+ title = {{GLUCOSE}: a solver that predicts learnt clauses quality},
+ booktitle = {SAT 2009 competitive events booklet},
+ year = {2009},
+ pages = {7--8},
+}
+
+@inproceedings{precosat,
+ author = {Armin Biere},
+ title = {P\{re,i\}coSAT@SC’09},
+ booktitle = {SAT 2009 competitive events booklet},
+ year = {2009},
+ pages = {41--42},
+}
+
+@inproceedings{DBLP:conf/sat/HeuleM04a,
+ author = {Marijn Heule and
+ Hans van Maaren},
+ title = {Aligning {CNF}- and Equivalence-Reasoning},
+ booktitle = {SAT (Selected Papers},
+ year = {2004},
+ pages = {145--156},
+ ee = {http://dx.doi.org/10.1007/11527695_12},
+ crossref = {DBLP:conf/sat/2004lncs},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/sat/2004lncs,
+ editor = {Holger H. Hoos and
+ David G. Mitchell},
+ title = {Theory and Applications of Satisfiability Testing, 7th International
+ Conference, SAT 2004, Vancouver, BC, Canada, May 10-13,
+ 2004, Revised Selected Papers},
+ booktitle = {SAT (Selected Papers)},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {3542},
+ year = {2005},
+ isbn = {3-540-27829-X},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@techreport{Heule-thesis,
+ author = {Marijn Heule},
+ title = {{m}arch: Towards a lookahead Sat solver for general purposes},
+ institution={Technische Universiteit Delft},
+ month={February},
+ year={2004},
+}
+
+@techreport{Heule-phd,
+ author = {Marijn J.H. Heule},
+ title = {Smart solving: Tool and techniques for satisfiability solvers},
+ institution={Technische Universiteit Delft},
+ year={2008},
+}
+
+@article{DBLP:journals/amai/JeroslowW90,
+ author = {Robert G. Jeroslow and
+ Jinchang Wang},
+ title = {Solving Propositional Satisfiability Problems},
+ journal = {Ann. Math. Artif. Intell.},
+ volume = {1},
+ year = {1990},
+ pages = {167-187},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{DBLP:conf/sat/PipatsrisawatD07,
+ author = {Knot Pipatsrisawat and
+ Adnan Darwiche},
+ title = {A Lightweight Component Caching Scheme for Satisfiability
+ Solvers},
+ booktitle = {SAT},
+ year = {2007},
+ pages = {294-299},
+ ee = {http://dx.doi.org/10.1007/978-3-540-72788-0_28},
+ crossref = {DBLP:conf/sat/2007},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/sat/2007,
+ editor = {Jo{\~a}o Marques-Silva and
+ Karem A. Sakallah},
+ title = {Theory and Applications of Satisfiability Testing --- SAT
+ 2007, 10th International Conference, Lisbon, Portugal, May
+ 28-31, 2007, Proceedings},
+ booktitle = {SAT},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {4501},
+ year = {2007},
+ isbn = {978-3-540-72787-3},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{DBLP:conf/ijcai/AudemardS09,
+ author = {Gilles Audemard and
+ Laurent Simon},
+ title = {Predicting Learnt Clauses Quality in Modern {SAT} Solvers},
+ booktitle = {IJCAI},
+ year = {2009},
+ pages = {399-404},
+ ee = {http://ijcai.org/papers09/Papers/IJCAI09-074.pdf},
+ crossref = {DBLP:conf/ijcai/2009},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/ijcai/2009,
+ editor = {Craig Boutilier},
+ title = {IJCAI 2009, Proceedings of the 21st International Joint
+ Conference on Artificial Intelligence, Pasadena, California,
+ USA, July 11-17, 2009},
+ booktitle = {IJCAI},
+ year = {2009},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+
+@inproceedings{DBLP:conf/tacas/JarvisaloBH10,
+ author = {Matti J{\"a}rvisalo and
+ Armin Biere and
+ Marijn Heule},
+ title = {Blocked Clause Elimination},
+ booktitle = {TACAS},
+ year = {2010},
+ pages = {129-144},
+ ee = {http://dx.doi.org/10.1007/978-3-642-12002-2_10},
+ crossref = {DBLP:conf/tacas/2010},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/tacas/2010,
+ editor = {Javier Esparza and
+ Rupak Majumdar},
+ title = {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},
+ booktitle = {TACAS},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {6015},
+ year = {2010},
+ isbn = {978-3-642-12001-5},
+ ee = {http://dx.doi.org/10.1007/978-3-642-12002-2},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@article{DBLP:journals/dam/Li03,
+ author = {Chu Min Li},
+ title = {Equivalent literal propagation in the {DLL} procedure},
+ journal = {Discrete Applied Mathematics},
+ volume = {130},
+ number = {2},
+ year = {2003},
+ pages = {251-276},
+ ee = {http://dx.doi.org/10.1016/S0166-218X(02)00407-9},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@misc{Grid5000,
+ author = {{The Grid'5000 team}},
+ title = {The {G}rid'5000 project},
+ note = {\url{https://www.grid5000.fr}},
+}
+ year = {2008},
+
+@article{DBLP:journals/endm/Berre01,
+ author = {Daniel Le Berre},
+ title = {Exploiting the real power of unit propagation lookahead},
+ journal = {Electronic Notes in Discrete Mathematics},
+ volume = {9},
+ year = {2001},
+ pages = {59-80},
+ ee = {http://dx.doi.org/10.1016/S1571-0653(04)00314-2},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{DBLP:conf/sat/GershmanS05,
+ author = {Roman Gershman and Ofer Strichman},
+ title = {Cost-Effective Hyper-Resolution for Preprocessing {CNF} Formulas},
+ booktitle = {SAT},
+ year = {2005},
+ pages = {423-429},
+ ee = {http://dx.doi.org/10.1007/11499107_34},
+ crossref = {DBLP:conf/sat/2005},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+
+@inproceedings{DBLP:conf/sat/HeuleJB11,
+ author = {Marijn Heule and
+ Matti J{\"a}rvisalo and
+ Armin Biere},
+ title = {Efficient {CNF} Simplification Based on Binary Implication
+ Graphs},
+ booktitle = {SAT},
+ year = {2011},
+ pages = {201-215},
+ ee = {http://dx.doi.org/10.1007/978-3-642-21581-0_17},
+ crossref = {DBLP:conf/sat/2011},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@proceedings{DBLP:conf/sat/2011,
+ editor = {Karem A. Sakallah and
+ Laurent Simon},
+ title = {Theory and Applications of Satisfiability Testing - SAT
+ 2011 - 14th International Conference, SAT 2011, Ann Arbor,
+ MI, USA, June 19-22, 2011. Proceedings},
+ booktitle = {SAT},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {6695},
+ year = {2011},
+ isbn = {978-3-642-21580-3},
+ ee = {http://dx.doi.org/10.1007/978-3-642-21581-0},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+
+@inproceedings{DBLP:conf/ecai/PietteHS08,
+ author = {C{\'e}dric Piette and
+ Youssef Hamadi and
+ Lakhdar Sais},
+ title = {Vivifying Propositional Clausal Formulae},
+ booktitle = {ECAI},
+ year = {2008},
+ pages = {525-529},
+ ee = {http://dx.doi.org/10.3233/978-1-58603-891-5-525},
+ crossref = {DBLP:conf/ecai/2008},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@proceedings{DBLP:conf/ecai/2008,
+ editor = {Malik Ghallab and
+ Constantine D. Spyropoulos and
+ Nikos Fakotakis and
+ Nikolaos M. Avouris},
+ title = {ECAI 2008 - 18th European Conference on Artificial Intelligence,
+ Patras, Greece, July 21-25, 2008, Proceedings},
+ booktitle = {ECAI},
+ publisher = {IOS Press},
+ series = {Frontiers in Artificial Intelligence and Applications},
+ volume = {178},
+ year = {2008},
+ isbn = {978-1-58603-891-5},
+ ee = {http://www.booksonline.iospress.nl/Content/View.aspx?piid=9905},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{DBLP:conf/sat/HanS09,
+ author = {HyoJung Han and
+ Fabio Somenzi},
+ title = {On-the-Fly Clause Improvement},
+ booktitle = {SAT},
+ year = {2009},
+ pages = {209-222},
+ ee = {http://dx.doi.org/10.1007/978-3-642-02777-2_21},
+ crossref = {DBLP:conf/sat/2009},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+
+@inproceedings{DBLP:conf/sat/SorenssonB09,
+ author = {Niklas S{\"o}rensson and
+ Armin Biere},
+ title = {Minimizing Learned Clauses},
+ booktitle = {SAT},
+ year = {2009},
+ pages = {237-243},
+ ee = {http://dx.doi.org/10.1007/978-3-642-02777-2_23},
+ crossref = {DBLP:conf/sat/2009},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{DBLP:conf/sat/BacchusW03,
+ author = {Fahiem Bacchus and
+ Jonathan Winter},
+ title = {Effective Preprocessing with Hyper-Resolution and Equality
+ Reduction},
+ booktitle = {SAT},
+ year = {2003},
+ pages = {341-355},
+ ee = {http://dx.doi.org/10.1007/978-3-540-24605-3_26},
+ crossref = {DBLP:conf/sat/2003},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@proceedings{DBLP:conf/sat/2003,
+ editor = {Enrico Giunchiglia and
+ Armando Tacchella},
+ title = {Theory and Applications of Satisfiability Testing, 6th International
+ Conference, SAT 2003. Santa Margherita Ligure, Italy, May
+ 5-8, 2003 Selected Revised Papers},
+ booktitle = {SAT},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {2919},
+ year = {2004},
+ isbn = {3-540-20851-8},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/sat/2005,
+ editor = {Fahiem Bacchus and
+ Toby Walsh},
+ title = {Theory and Applications of Satisfiability Testing, 8th International
+ Conference, SAT 2005, St. Andrews, UK, June 19-23, 2005,
+ Proceedings},
+ booktitle = {SAT},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {3569},
+ year = {2005},
+ isbn = {3-540-26276-8},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/sat/2009,
+ editor = {Oliver Kullmann},
+ title = {Theory and Applications of Satisfiability Testing - SAT
+ 2009, 12th International Conference, SAT 2009, Swansea,
+ UK, June 30 - July 3, 2009. Proceedings},
+ booktitle = {SAT},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ volume = {5584},
+ year = {2009},
+ isbn = {978-3-642-02776-5},
+ ee = {http://dx.doi.org/10.1007/978-3-642-02777-2},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{DBLP:conf/hvc/MantheyHB12,
+ author = {Norbert Manthey and
+ Marijn Heule and
+ Armin Biere},
+ title = {Automated Reencoding of Boolean Formulas},
+ booktitle = {Haifa Verification Conference},
+ year = {2012},
+ pages = {102-117},
+ ee = {http://dx.doi.org/10.1007/978-3-642-39611-3_14},
+ crossref = {DBLP:conf/hvc/2012},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/hvc/2012,
+ editor = {Armin Biere and
+ Amir Nahir and
+ Tanja E. J. Vos},
+ title = {Hardware and Software: Verification and Testing - 8th International
+ Haifa Verification Conference, HVC 2012, Haifa, Israel,
+ November 6-8, 2012. Revised Selected Papers},
+ booktitle = {Haifa Verification Conference},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ volume = {7857},
+ year = {2013},
+ isbn = {978-3-642-39610-6},
+ ee = {http://dx.doi.org/10.1007/978-3-642-39611-3},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
\ No newline at end of file diff --git a/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/splncs03.bst b/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/splncs03.bst new file mode 100644 index 000000000..327916917 --- /dev/null +++ b/cryptominisat5/cryptominisat-5.6.3/docs/satcomp14-pdf/splncs03.bst @@ -0,0 +1,1519 @@ +%% BibTeX bibliography style `splncs03'
+%%
+%% BibTeX bibliography style for use with numbered references in
+%% Springer Verlag's "Lecture Notes in Computer Science" series.
+%% (See Springer's documentation for llncs.cls for
+%% more details of the suggested reference format.) Note that this
+%% file will not work for author-year style citations.
+%%
+%% Use \documentclass{llncs} and \bibliographystyle{splncs03}, and cite
+%% a reference with (e.g.) \cite{smith77} to get a "[1]" in the text.
+%%
+%% This file comes to you courtesy of Maurizio "Titto" Patrignani of
+%% Dipartimento di Informatica e Automazione Universita' Roma Tre
+%%
+%% ================================================================================================
+%% This was file `titto-lncs-02.bst' produced on Wed Apr 1, 2009
+%% Edited by hand by titto based on `titto-lncs-01.bst' (see below)
+%%
+%% CHANGES (with respect to titto-lncs-01.bst):
+%% - Removed the call to \urlprefix (thus no "URL" string is added to the output)
+%% ================================================================================================
+%% This was file `titto-lncs-01.bst' produced on Fri Aug 22, 2008
+%% Edited by hand by titto based on `titto.bst' (see below)
+%%
+%% CHANGES (with respect to titto.bst):
+%% - Removed the "capitalize" command for editors string "(eds.)" and "(ed.)"
+%% - Introduced the functions titto.bbl.pages and titto.bbl.page for journal pages (without "pp.")
+%% - Added a new.sentence command to separate with a dot booktitle and series in the inproceedings
+%% - Commented all new.block commands before urls and notes (to separate them with a comma)
+%% - Introduced the functions titto.bbl.volume for handling journal volumes (without "vol." label)
+%% - Used for editors the same name conventions used for authors (see function format.in.ed.booktitle)
+%% - Removed a \newblock to avoid long spaces between title and "In: ..."
+%% - Added function titto.space.prefix to add a space instead of "~" after the (removed) "vol." label
+%% ================================================================================================
+%% This was file `titto.bst',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% merlin.mbs (with options: `vonx,nm-rvvc,yr-par,jttl-rm,volp-com,jwdpg,jwdvol,numser,ser-vol,jnm-x,btit-rm,bt-rm,edparxc,bkedcap,au-col,in-col,fin-bare,pp,ed,abr,mth-bare,xedn,jabr,and-com,and-com-ed,xand,url,url-blk,em-x,nfss,')
+%% ----------------------------------------
+%% *** Tentative .bst file for Springer LNCS ***
+%%
+%% Copyright 1994-2007 Patrick W Daly
+ % ===============================================================
+ % IMPORTANT NOTICE:
+ % This bibliographic style (bst) file has been generated from one or
+ % more master bibliographic style (mbs) files, listed above.
+ %
+ % This generated file can be redistributed and/or modified under the terms
+ % of the LaTeX Project Public License Distributed from CTAN
+ % archives in directory macros/latex/base/lppl.txt; either
+ % version 1 of the License, or any later version.
+ % ===============================================================
+ % Name and version information of the main mbs file:
+ % \ProvidesFile{merlin.mbs}[2007/04/24 4.20 (PWD, AO, DPC)]
+ % For use with BibTeX version 0.99a or later
+ %-------------------------------------------------------------------
+ % This bibliography style file is intended for texts in ENGLISH
+ % This is a numerical citation style, and as such is standard LaTeX.
+ % It requires no extra package to interface to the main text.
+ % The form of the \bibitem entries is
+ % \bibitem{key}...
+ % Usage of \cite is as follows:
+ % \cite{key} ==>> [#]
+ % \cite[chap. 2]{key} ==>> [#, chap. 2]
+ % where # is a number determined by the ordering in the reference list.
+ % The order in the reference list is alphabetical by authors.
+ %---------------------------------------------------------------------
+
+ENTRY
+ { address
+ author
+ booktitle
+ chapter
+ edition
+ editor
+ eid
+ howpublished
+ institution
+ journal
+ key
+ month
+ note
+ number
+ organization
+ pages
+ publisher
+ school
+ series
+ title
+ type
+ url
+ volume
+ year
+ }
+ {}
+ { label }
+INTEGERS { output.state before.all mid.sentence after.sentence after.block }
+FUNCTION {init.state.consts}
+{ #0 'before.all :=
+ #1 'mid.sentence :=
+ #2 'after.sentence :=
+ #3 'after.block :=
+}
+STRINGS { s t}
+FUNCTION {output.nonnull}
+{ 's :=
+ output.state mid.sentence =
+ { ", " * write$ }
+ { output.state after.block =
+ { add.period$ write$
+% newline$
+% "\newblock " write$ % removed for titto-lncs-01
+ " " write$ % to avoid long spaces between title and "In: ..."
+ }
+ { output.state before.all =
+ 'write$
+ { add.period$ " " * write$ }
+ if$
+ }
+ if$
+ mid.sentence 'output.state :=
+ }
+ if$
+ s
+}
+FUNCTION {output}
+{ duplicate$ empty$
+ 'pop$
+ 'output.nonnull
+ if$
+}
+FUNCTION {output.check}
+{ 't :=
+ duplicate$ empty$
+ { pop$ "empty " t * " in " * cite$ * warning$ }
+ 'output.nonnull
+ if$
+}
+FUNCTION {fin.entry}
+{ duplicate$ empty$
+ 'pop$
+ 'write$
+ if$
+ newline$
+}
+
+FUNCTION {new.block}
+{ output.state before.all =
+ 'skip$
+ { after.block 'output.state := }
+ if$
+}
+FUNCTION {new.sentence}
+{ output.state after.block =
+ 'skip$
+ { output.state before.all =
+ 'skip$
+ { after.sentence 'output.state := }
+ if$
+ }
+ if$
+}
+FUNCTION {add.blank}
+{ " " * before.all 'output.state :=
+}
+
+
+FUNCTION {add.colon}
+{ duplicate$ empty$
+ 'skip$
+ { ":" * add.blank }
+ if$
+}
+
+FUNCTION {date.block}
+{
+ new.block
+}
+
+FUNCTION {not}
+{ { #0 }
+ { #1 }
+ if$
+}
+FUNCTION {and}
+{ 'skip$
+ { pop$ #0 }
+ if$
+}
+FUNCTION {or}
+{ { pop$ #1 }
+ 'skip$
+ if$
+}
+STRINGS {z}
+FUNCTION {remove.dots}
+{ 'z :=
+ ""
+ { z empty$ not }
+ { z #1 #1 substring$
+ z #2 global.max$ substring$ 'z :=
+ duplicate$ "." = 'pop$
+ { * }
+ if$
+ }
+ while$
+}
+FUNCTION {new.block.checka}
+{ empty$
+ 'skip$
+ 'new.block
+ if$
+}
+FUNCTION {new.block.checkb}
+{ empty$
+ swap$ empty$
+ and
+ 'skip$
+ 'new.block
+ if$
+}
+FUNCTION {new.sentence.checka}
+{ empty$
+ 'skip$
+ 'new.sentence
+ if$
+}
+FUNCTION {new.sentence.checkb}
+{ empty$
+ swap$ empty$
+ and
+ 'skip$
+ 'new.sentence
+ if$
+}
+FUNCTION {field.or.null}
+{ duplicate$ empty$
+ { pop$ "" }
+ 'skip$
+ if$
+}
+FUNCTION {emphasize}
+{ skip$ }
+FUNCTION {tie.or.space.prefix}
+{ duplicate$ text.length$ #3 <
+ { "~" }
+ { " " }
+ if$
+ swap$
+}
+FUNCTION {titto.space.prefix} % always introduce a space
+{ duplicate$ text.length$ #3 <
+ { " " }
+ { " " }
+ if$
+ swap$
+}
+
+
+FUNCTION {capitalize}
+{ "u" change.case$ "t" change.case$ }
+
+FUNCTION {space.word}
+{ " " swap$ * " " * }
+ % Here are the language-specific definitions for explicit words.
+ % Each function has a name bbl.xxx where xxx is the English word.
+ % The language selected here is ENGLISH
+FUNCTION {bbl.and}
+{ "and"}
+
+FUNCTION {bbl.etal}
+{ "et~al." }
+
+FUNCTION {bbl.editors}
+{ "eds." }
+
+FUNCTION {bbl.editor}
+{ "ed." }
+
+FUNCTION {bbl.edby}
+{ "edited by" }
+
+FUNCTION {bbl.edition}
+{ "edn." }
+
+FUNCTION {bbl.volume}
+{ "vol." }
+
+FUNCTION {titto.bbl.volume} % for handling journals
+{ "" }
+
+FUNCTION {bbl.of}
+{ "of" }
+
+FUNCTION {bbl.number}
+{ "no." }
+
+FUNCTION {bbl.nr}
+{ "no." }
+
+FUNCTION {bbl.in}
+{ "in" }
+
+FUNCTION {bbl.pages}
+{ "pp." }
+
+FUNCTION {bbl.page}
+{ "p." }
+
+FUNCTION {titto.bbl.pages} % for journals
+{ "" }
+
+FUNCTION {titto.bbl.page} % for journals
+{ "" }
+
+FUNCTION {bbl.chapter}
+{ "chap." }
+
+FUNCTION {bbl.techrep}
+{ "Tech. Rep." }
+
+FUNCTION {bbl.mthesis}
+{ "Master's thesis" }
+
+FUNCTION {bbl.phdthesis}
+{ "Ph.D. thesis" }
+
+MACRO {jan} {"Jan."}
+
+MACRO {feb} {"Feb."}
+
+MACRO {mar} {"Mar."}
+
+MACRO {apr} {"Apr."}
+
+MACRO {may} {"May"}
+
+MACRO {jun} {"Jun."}
+
+MACRO {jul} {"Jul."}
+
+MACRO {aug} {"Aug."}
+
+MACRO {sep} {"Sep."}
+
+MACRO {oct} {"Oct."}
+
+MACRO {nov} {"Nov."}
+
+MACRO {dec} {"Dec."}
+
+MACRO {acmcs} {"ACM Comput. Surv."}
+
+MACRO {acta} {"Acta Inf."}
+
+MACRO {cacm} {"Commun. ACM"}
+
+MACRO {ibmjrd} {"IBM J. Res. Dev."}
+
+MACRO {ibmsj} {"IBM Syst.~J."}
+
+MACRO {ieeese} {"IEEE Trans. Software Eng."}
+
+MACRO {ieeetc} {"IEEE Trans. Comput."}
+
+MACRO {ieeetcad}
+ {"IEEE Trans. Comput. Aid. Des."}
+
+MACRO {ipl} {"Inf. Process. Lett."}
+
+MACRO {jacm} {"J.~ACM"}
+
+MACRO {jcss} {"J.~Comput. Syst. Sci."}
+
+MACRO {scp} {"Sci. Comput. Program."}
+
+MACRO {sicomp} {"SIAM J. Comput."}
+
+MACRO {tocs} {"ACM Trans. Comput. Syst."}
+
+MACRO {tods} {"ACM Trans. Database Syst."}
+
+MACRO {tog} {"ACM Trans. Graphic."}
+
+MACRO {toms} {"ACM Trans. Math. Software"}
+
+MACRO {toois} {"ACM Trans. Office Inf. Syst."}
+
+MACRO {toplas} {"ACM Trans. Progr. Lang. Syst."}
+
+MACRO {tcs} {"Theor. Comput. Sci."}
+
+FUNCTION {bibinfo.check}
+{ swap$
+ duplicate$ missing$
+ {
+ pop$ pop$
+ ""
+ }
+ { duplicate$ empty$
+ {
+ swap$ pop$
+ }
+ { swap$
+ pop$
+ }
+ if$
+ }
+ if$
+}
+FUNCTION {bibinfo.warn}
+{ swap$
+ duplicate$ missing$
+ {
+ swap$ "missing " swap$ * " in " * cite$ * warning$ pop$
+ ""
+ }
+ { duplicate$ empty$
+ {
+ swap$ "empty " swap$ * " in " * cite$ * warning$
+ }
+ { swap$
+ pop$
+ }
+ if$
+ }
+ if$
+}
+FUNCTION {format.url}
+{ url empty$
+ { "" }
+% { "\urlprefix\url{" url * "}" * }
+ { "\url{" url * "}" * } % changed in titto-lncs-02.bst
+ if$
+}
+
+INTEGERS { nameptr namesleft numnames }
+
+
+STRINGS { bibinfo}
+
+FUNCTION {format.names}
+{ 'bibinfo :=
+ duplicate$ empty$ 'skip$ {
+ 's :=
+ "" 't :=
+ #1 'nameptr :=
+ s num.names$ 'numnames :=
+ numnames 'namesleft :=
+ { namesleft #0 > }
+ { s nameptr
+ "{vv~}{ll}{, jj}{, f{.}.}"
+ format.name$
+ bibinfo bibinfo.check
+ 't :=
+ nameptr #1 >
+ {
+ namesleft #1 >
+ { ", " * t * }
+ {
+ s nameptr "{ll}" format.name$ duplicate$ "others" =
+ { 't := }
+ { pop$ }
+ if$
+ "," *
+ t "others" =
+ {
+ " " * bbl.etal *
+ }
+ { " " * t * }
+ if$
+ }
+ if$
+ }
+ 't
+ if$
+ nameptr #1 + 'nameptr :=
+ namesleft #1 - 'namesleft :=
+ }
+ while$
+ } if$
+}
+FUNCTION {format.names.ed}
+{
+ 'bibinfo :=
+ duplicate$ empty$ 'skip$ {
+ 's :=
+ "" 't :=
+ #1 'nameptr :=
+ s num.names$ 'numnames :=
+ numnames 'namesleft :=
+ { namesleft #0 > }
+ { s nameptr
+ "{f{.}.~}{vv~}{ll}{ jj}"
+ format.name$
+ bibinfo bibinfo.check
+ 't :=
+ nameptr #1 >
+ {
+ namesleft #1 >
+ { ", " * t * }
+ {
+ s nameptr "{ll}" format.name$ duplicate$ "others" =
+ { 't := }
+ { pop$ }
+ if$
+ "," *
+ t "others" =
+ {
+
+ " " * bbl.etal *
+ }
+ { " " * t * }
+ if$
+ }
+ if$
+ }
+ 't
+ if$
+ nameptr #1 + 'nameptr :=
+ namesleft #1 - 'namesleft :=
+ }
+ while$
+ } if$
+}
+FUNCTION {format.authors}
+{ author "author" format.names
+}
+FUNCTION {get.bbl.editor}
+{ editor num.names$ #1 > 'bbl.editors 'bbl.editor if$ }
+
+FUNCTION {format.editors}
+{ editor "editor" format.names duplicate$ empty$ 'skip$
+ {
+ " " *
+ get.bbl.editor
+% capitalize
+ "(" swap$ * ")" *
+ *
+ }
+ if$
+}
+FUNCTION {format.note}
+{
+ note empty$
+ { "" }
+ { note #1 #1 substring$
+ duplicate$ "{" =
+ 'skip$
+ { output.state mid.sentence =
+ { "l" }
+ { "u" }
+ if$
+ change.case$
+ }
+ if$
+ note #2 global.max$ substring$ * "note" bibinfo.check
+ }
+ if$
+}
+
+FUNCTION {format.title}
+{ title
+ duplicate$ empty$ 'skip$
+ { "t" change.case$ }
+ if$
+ "title" bibinfo.check
+}
+FUNCTION {output.bibitem}
+{ newline$
+ "\bibitem{" write$
+ cite$ write$
+ "}" write$
+ newline$
+ ""
+ before.all 'output.state :=
+}
+
+FUNCTION {n.dashify}
+{
+ 't :=
+ ""
+ { t empty$ not }
+ { t #1 #1 substring$ "-" =
+ { t #1 #2 substring$ "--" = not
+ { "--" *
+ t #2 global.max$ substring$ 't :=
+ }
+ { { t #1 #1 substring$ "-" = }
+ { "-" *
+ t #2 global.max$ substring$ 't :=
+ }
+ while$
+ }
+ if$
+ }
+ { t #1 #1 substring$ *
+ t #2 global.max$ substring$ 't :=
+ }
+ if$
+ }
+ while$
+}
+
+FUNCTION {word.in}
+{ bbl.in capitalize
+ ":" *
+ " " * }
+
+FUNCTION {format.date}
+{
+ month "month" bibinfo.check
+ duplicate$ empty$
+ year "year" bibinfo.check duplicate$ empty$
+ { swap$ 'skip$
+ { "there's a month but no year in " cite$ * warning$ }
+ if$
+ *
+ }
+ { swap$ 'skip$
+ {
+ swap$
+ " " * swap$
+ }
+ if$
+ *
+ remove.dots
+ }
+ if$
+ duplicate$ empty$
+ 'skip$
+ {
+ before.all 'output.state :=
+ " (" swap$ * ")" *
+ }
+ if$
+}
+FUNCTION {format.btitle}
+{ title "title" bibinfo.check
+ duplicate$ empty$ 'skip$
+ {
+ }
+ if$
+}
+FUNCTION {either.or.check}
+{ empty$
+ 'pop$
+ { "can't use both " swap$ * " fields in " * cite$ * warning$ }
+ if$
+}
+FUNCTION {format.bvolume}
+{ volume empty$
+ { "" }
+ { bbl.volume volume tie.or.space.prefix
+ "volume" bibinfo.check * *
+ series "series" bibinfo.check
+ duplicate$ empty$ 'pop$
+ { emphasize ", " * swap$ * }
+ if$
+ "volume and number" number either.or.check
+ }
+ if$
+}
+FUNCTION {format.number.series}
+{ volume empty$
+ { number empty$
+ { series field.or.null }
+ { output.state mid.sentence =
+ { bbl.number }
+ { bbl.number capitalize }
+ if$
+ number tie.or.space.prefix "number" bibinfo.check * *
+ series empty$
+ { "there's a number but no series in " cite$ * warning$ }
+ { bbl.in space.word *
+ series "series" bibinfo.check *
+ }
+ if$
+ }
+ if$
+ }
+ { "" }
+ if$
+}
+
+FUNCTION {format.edition}
+{ edition duplicate$ empty$ 'skip$
+ {
+ output.state mid.sentence =
+ { "l" }
+ { "t" }
+ if$ change.case$
+ "edition" bibinfo.check
+ " " * bbl.edition *
+ }
+ if$
+}
+INTEGERS { multiresult }
+FUNCTION {multi.page.check}
+{ 't :=
+ #0 'multiresult :=
+ { multiresult not
+ t empty$ not
+ and
+ }
+ { t #1 #1 substring$
+ duplicate$ "-" =
+ swap$ duplicate$ "," =
+ swap$ "+" =
+ or or
+ { #1 'multiresult := }
+ { t #2 global.max$ substring$ 't := }
+ if$
+ }
+ while$
+ multiresult
+}
+FUNCTION {format.pages}
+{ pages duplicate$ empty$ 'skip$
+ { duplicate$ multi.page.check
+ {
+ bbl.pages swap$
+ n.dashify
+ }
+ {
+ bbl.page swap$
+ }
+ if$
+ tie.or.space.prefix
+ "pages" bibinfo.check
+ * *
+ }
+ if$
+}
+FUNCTION {format.journal.pages}
+{ pages duplicate$ empty$ 'pop$
+ { swap$ duplicate$ empty$
+ { pop$ pop$ format.pages }
+ {
+ ", " *
+ swap$
+ n.dashify
+ pages multi.page.check
+ 'titto.bbl.pages
+ 'titto.bbl.page
+ if$
+ swap$ tie.or.space.prefix
+ "pages" bibinfo.check
+ * *
+ *
+ }
+ if$
+ }
+ if$
+}
+FUNCTION {format.journal.eid}
+{ eid "eid" bibinfo.check
+ duplicate$ empty$ 'pop$
+ { swap$ duplicate$ empty$ 'skip$
+ {
+ ", " *
+ }
+ if$
+ swap$ *
+ }
+ if$
+}
+FUNCTION {format.vol.num.pages} % this function is used only for journal entries
+{ volume field.or.null
+ duplicate$ empty$ 'skip$
+ {
+% bbl.volume swap$ tie.or.space.prefix
+ titto.bbl.volume swap$ titto.space.prefix
+% rationale for the change above: for journals you don't want "vol." label
+% hence it does not make sense to attach the journal number to the label when
+% it is short
+ "volume" bibinfo.check
+ * *
+ }
+ if$
+ number "number" bibinfo.check duplicate$ empty$ 'skip$
+ {
+ swap$ duplicate$ empty$
+ { "there's a number but no volume in " cite$ * warning$ }
+ 'skip$
+ if$
+ swap$
+ "(" swap$ * ")" *
+ }
+ if$ *
+ eid empty$
+ { format.journal.pages }
+ { format.journal.eid }
+ if$
+}
+
+FUNCTION {format.chapter.pages}
+{ chapter empty$
+ 'format.pages
+ { type empty$
+ { bbl.chapter }
+ { type "l" change.case$
+ "type" bibinfo.check
+ }
+ if$
+ chapter tie.or.space.prefix
+ "chapter" bibinfo.check
+ * *
+ pages empty$
+ 'skip$
+ { ", " * format.pages * }
+ if$
+ }
+ if$
+}
+
+FUNCTION {format.booktitle}
+{
+ booktitle "booktitle" bibinfo.check
+}
+FUNCTION {format.in.ed.booktitle}
+{ format.booktitle duplicate$ empty$ 'skip$
+ {
+% editor "editor" format.names.ed duplicate$ empty$ 'pop$ % changed by titto
+ editor "editor" format.names duplicate$ empty$ 'pop$
+ {
+ " " *
+ get.bbl.editor
+% capitalize
+ "(" swap$ * ") " *
+ * swap$
+ * }
+ if$
+ word.in swap$ *
+ }
+ if$
+}
+FUNCTION {empty.misc.check}
+{ author empty$ title empty$ howpublished empty$
+ month empty$ year empty$ note empty$
+ and and and and and
+ key empty$ not and
+ { "all relevant fields are empty in " cite$ * warning$ }
+ 'skip$
+ if$
+}
+FUNCTION {format.thesis.type}
+{ type duplicate$ empty$
+ 'pop$
+ { swap$ pop$
+ "t" change.case$ "type" bibinfo.check
+ }
+ if$
+}
+FUNCTION {format.tr.number}
+{ number "number" bibinfo.check
+ type duplicate$ empty$
+ { pop$ bbl.techrep }
+ 'skip$
+ if$
+ "type" bibinfo.check
+ swap$ duplicate$ empty$
+ { pop$ "t" change.case$ }
+ { tie.or.space.prefix * * }
+ if$
+}
+FUNCTION {format.article.crossref}
+{
+ key duplicate$ empty$
+ { pop$
+ journal duplicate$ empty$
+ { "need key or journal for " cite$ * " to crossref " * crossref * warning$ }
+ { "journal" bibinfo.check emphasize word.in swap$ * }
+ if$
+ }
+ { word.in swap$ * " " *}
+ if$
+ " \cite{" * crossref * "}" *
+}
+FUNCTION {format.crossref.editor}
+{ editor #1 "{vv~}{ll}" format.name$
+ "editor" bibinfo.check
+ editor num.names$ duplicate$
+ #2 >
+ { pop$
+ "editor" bibinfo.check
+ " " * bbl.etal
+ *
+ }
+ { #2 <
+ 'skip$
+ { editor #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" =
+ {
+ "editor" bibinfo.check
+ " " * bbl.etal
+ *
+ }
+ {
+ bbl.and space.word
+ * editor #2 "{vv~}{ll}" format.name$
+ "editor" bibinfo.check
+ *
+ }
+ if$
+ }
+ if$
+ }
+ if$
+}
+FUNCTION {format.book.crossref}
+{ volume duplicate$ empty$
+ { "empty volume in " cite$ * "'s crossref of " * crossref * warning$
+ pop$ word.in
+ }
+ { bbl.volume
+ capitalize
+ swap$ tie.or.space.prefix "volume" bibinfo.check * * bbl.of space.word *
+ }
+ if$
+ editor empty$
+ editor field.or.null author field.or.null =
+ or
+ { key empty$
+ { series empty$
+ { "need editor, key, or series for " cite$ * " to crossref " *
+ crossref * warning$
+ "" *
+ }
+ { series emphasize * }
+ if$
+ }
+ { key * }
+ if$
+ }
+ { format.crossref.editor * }
+ if$
+ " \cite{" * crossref * "}" *
+}
+FUNCTION {format.incoll.inproc.crossref}
+{
+ editor empty$
+ editor field.or.null author field.or.null =
+ or
+ { key empty$
+ { format.booktitle duplicate$ empty$
+ { "need editor, key, or booktitle for " cite$ * " to crossref " *
+ crossref * warning$
+ }
+ { word.in swap$ * }
+ if$
+ }
+ { word.in key * " " *}
+ if$
+ }
+ { word.in format.crossref.editor * " " *}
+ if$
+ " \cite{" * crossref * "}" *
+}
+FUNCTION {format.org.or.pub}
+{ 't :=
+ ""
+ address empty$ t empty$ and
+ 'skip$
+ {
+ t empty$
+ { address "address" bibinfo.check *
+ }
+ { t *
+ address empty$
+ 'skip$
+ { ", " * address "address" bibinfo.check * }
+ if$
+ }
+ if$
+ }
+ if$
+}
+FUNCTION {format.publisher.address}
+{ publisher "publisher" bibinfo.warn format.org.or.pub
+}
+
+FUNCTION {format.organization.address}
+{ organization "organization" bibinfo.check format.org.or.pub
+}
+
+FUNCTION {article}
+{ output.bibitem
+ format.authors "author" output.check
+ add.colon
+ new.block
+ format.title "title" output.check
+ new.block
+ crossref missing$
+ {
+ journal
+ "journal" bibinfo.check
+ "journal" output.check
+ add.blank
+ format.vol.num.pages output
+ format.date "year" output.check
+ }
+ { format.article.crossref output.nonnull
+ format.pages output
+ }
+ if$
+% new.block
+ format.url output
+% new.block
+ format.note output
+ fin.entry
+}
+FUNCTION {book}
+{ output.bibitem
+ author empty$
+ { format.editors "author and editor" output.check
+ add.colon
+ }
+ { format.authors output.nonnull
+ add.colon
+ crossref missing$
+ { "author and editor" editor either.or.check }
+ 'skip$
+ if$
+ }
+ if$
+ new.block
+ format.btitle "title" output.check
+ crossref missing$
+ { format.bvolume output
+ new.block
+ new.sentence
+ format.number.series output
+ format.publisher.address output
+ }
+ {
+ new.block
+ format.book.crossref output.nonnull
+ }
+ if$
+ format.edition output
+ format.date "year" output.check
+% new.block
+ format.url output
+% new.block
+ format.note output
+ fin.entry
+}
+FUNCTION {booklet}
+{ output.bibitem
+ format.authors output
+ add.colon
+ new.block
+ format.title "title" output.check
+ new.block
+ howpublished "howpublished" bibinfo.check output
+ address "address" bibinfo.check output
+ format.date output
+% new.block
+ format.url output
+% new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {inbook}
+{ output.bibitem
+ author empty$
+ { format.editors "author and editor" output.check
+ add.colon
+ }
+ { format.authors output.nonnull
+ add.colon
+ crossref missing$
+ { "author and editor" editor either.or.check }
+ 'skip$
+ if$
+ }
+ if$
+ new.block
+ format.btitle "title" output.check
+ crossref missing$
+ {
+ format.bvolume output
+ format.chapter.pages "chapter and pages" output.check
+ new.block
+ new.sentence
+ format.number.series output
+ format.publisher.address output
+ }
+ {
+ format.chapter.pages "chapter and pages" output.check
+ new.block
+ format.book.crossref output.nonnull
+ }
+ if$
+ format.edition output
+ format.date "year" output.check
+% new.block
+ format.url output
+% new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {incollection}
+{ output.bibitem
+ format.authors "author" output.check
+ add.colon
+ new.block
+ format.title "title" output.check
+ new.block
+ crossref missing$
+ { format.in.ed.booktitle "booktitle" output.check
+ format.bvolume output
+ format.chapter.pages output
+ new.sentence
+ format.number.series output
+ format.publisher.address output
+ format.edition output
+ format.date "year" output.check
+ }
+ { format.incoll.inproc.crossref output.nonnull
+ format.chapter.pages output
+ }
+ if$
+% new.block
+ format.url output
+% new.block
+ format.note output
+ fin.entry
+}
+FUNCTION {inproceedings}
+{ output.bibitem
+ format.authors "author" output.check
+ add.colon
+ new.block
+ format.title "title" output.check
+ new.block
+ crossref missing$
+ { format.in.ed.booktitle "booktitle" output.check
+ new.sentence % added by titto
+ format.bvolume output
+ format.pages output
+ new.sentence
+ format.number.series output
+ publisher empty$
+ { format.organization.address output }
+ { organization "organization" bibinfo.check output
+ format.publisher.address output
+ }
+ if$
+ format.date "year" output.check
+ }
+ { format.incoll.inproc.crossref output.nonnull
+ format.pages output
+ }
+ if$
+% new.block
+ format.url output
+% new.block
+ format.note output
+ fin.entry
+}
+FUNCTION {conference} { inproceedings }
+FUNCTION {manual}
+{ output.bibitem
+ author empty$
+ { organization "organization" bibinfo.check
+ duplicate$ empty$ 'pop$
+ { output
+ address "address" bibinfo.check output
+ }
+ if$
+ }
+ { format.authors output.nonnull }
+ if$
+ add.colon
+ new.block
+ format.btitle "title" output.check
+ author empty$
+ { organization empty$
+ {
+ address new.block.checka
+ address "address" bibinfo.check output
+ }
+ 'skip$
+ if$
+ }
+ {
+ organization address new.block.checkb
+ organization "organization" bibinfo.check output
+ address "address" bibinfo.check output
+ }
+ if$
+ format.edition output
+ format.date output
+% new.block
+ format.url output
+% new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {mastersthesis}
+{ output.bibitem
+ format.authors "author" output.check
+ add.colon
+ new.block
+ format.btitle
+ "title" output.check
+ new.block
+ bbl.mthesis format.thesis.type output.nonnull
+ school "school" bibinfo.warn output
+ address "address" bibinfo.check output
+ format.date "year" output.check
+% new.block
+ format.url output
+% new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {misc}
+{ output.bibitem
+ format.authors output
+ add.colon
+ title howpublished new.block.checkb
+ format.title output
+ howpublished new.block.checka
+ howpublished "howpublished" bibinfo.check output
+ format.date output
+% new.block
+ format.url output
+% new.block
+ format.note output
+ fin.entry
+ empty.misc.check
+}
+FUNCTION {phdthesis}
+{ output.bibitem
+ format.authors "author" output.check
+ add.colon
+ new.block
+ format.btitle
+ "title" output.check
+ new.block
+ bbl.phdthesis format.thesis.type output.nonnull
+ school "school" bibinfo.warn output
+ address "address" bibinfo.check output
+ format.date "year" output.check
+% new.block
+ format.url output
+% new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {proceedings}
+{ output.bibitem
+ editor empty$
+ { organization "organization" bibinfo.check output
+ }
+ { format.editors output.nonnull }
+ if$
+ add.colon
+ new.block
+ format.btitle "title" output.check
+ format.bvolume output
+ editor empty$
+ { publisher empty$
+ { format.number.series output }
+ {
+ new.sentence
+ format.number.series output
+ format.publisher.address output
+ }
+ if$
+ }
+ { publisher empty$
+ {
+ new.sentence
+ format.number.series output
+ format.organization.address output }
+ {
+ new.sentence
+ format.number.series output
+ organization "organization" bibinfo.check output
+ format.publisher.address output
+ }
+ if$
+ }
+ if$
+ format.date "year" output.check
+% new.block
+ format.url output
+% new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {techreport}
+{ output.bibitem
+ format.authors "author" output.check
+ add.colon
+ new.block
+ format.title
+ "title" output.check
+ new.block
+ format.tr.number output.nonnull
+ institution "institution" bibinfo.warn output
+ address "address" bibinfo.check output
+ format.date "year" output.check
+% new.block
+ format.url output
+% new.block
+ format.note output
+ fin.entry
+}
+
+FUNCTION {unpublished}
+{ output.bibitem
+ format.authors "author" output.check
+ add.colon
+ new.block
+ format.title "title" output.check
+ format.date output
+% new.block
+ format.url output
+% new.block
+ format.note "note" output.check
+ fin.entry
+}
+
+FUNCTION {default.type} { misc }
+READ
+FUNCTION {sortify}
+{ purify$
+ "l" change.case$
+}
+INTEGERS { len }
+FUNCTION {chop.word}
+{ 's :=
+ 'len :=
+ s #1 len substring$ =
+ { s len #1 + global.max$ substring$ }
+ 's
+ if$
+}
+FUNCTION {sort.format.names}
+{ 's :=
+ #1 'nameptr :=
+ ""
+ s num.names$ 'numnames :=
+ numnames 'namesleft :=
+ { namesleft #0 > }
+ { s nameptr
+ "{ll{ }}{ ff{ }}{ jj{ }}"
+ format.name$ 't :=
+ nameptr #1 >
+ {
+ " " *
+ namesleft #1 = t "others" = and
+ { "zzzzz" * }
+ { t sortify * }
+ if$
+ }
+ { t sortify * }
+ if$
+ nameptr #1 + 'nameptr :=
+ namesleft #1 - 'namesleft :=
+ }
+ while$
+}
+
+FUNCTION {sort.format.title}
+{ 't :=
+ "A " #2
+ "An " #3
+ "The " #4 t chop.word
+ chop.word
+ chop.word
+ sortify
+ #1 global.max$ substring$
+}
+FUNCTION {author.sort}
+{ author empty$
+ { key empty$
+ { "to sort, need author or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { author sort.format.names }
+ if$
+}
+FUNCTION {author.editor.sort}
+{ author empty$
+ { editor empty$
+ { key empty$
+ { "to sort, need author, editor, or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { editor sort.format.names }
+ if$
+ }
+ { author sort.format.names }
+ if$
+}
+FUNCTION {author.organization.sort}
+{ author empty$
+ { organization empty$
+ { key empty$
+ { "to sort, need author, organization, or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { "The " #4 organization chop.word sortify }
+ if$
+ }
+ { author sort.format.names }
+ if$
+}
+FUNCTION {editor.organization.sort}
+{ editor empty$
+ { organization empty$
+ { key empty$
+ { "to sort, need editor, organization, or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { "The " #4 organization chop.word sortify }
+ if$
+ }
+ { editor sort.format.names }
+ if$
+}
+FUNCTION {presort}
+{ type$ "book" =
+ type$ "inbook" =
+ or
+ 'author.editor.sort
+ { type$ "proceedings" =
+ 'editor.organization.sort
+ { type$ "manual" =
+ 'author.organization.sort
+ 'author.sort
+ if$
+ }
+ if$
+ }
+ if$
+ " "
+ *
+ year field.or.null sortify
+ *
+ " "
+ *
+ title field.or.null
+ sort.format.title
+ *
+ #1 entry.max$ substring$
+ 'sort.key$ :=
+}
+ITERATE {presort}
+SORT
+STRINGS { longest.label }
+INTEGERS { number.label longest.label.width }
+FUNCTION {initialize.longest.label}
+{ "" 'longest.label :=
+ #1 'number.label :=
+ #0 'longest.label.width :=
+}
+FUNCTION {longest.label.pass}
+{ number.label int.to.str$ 'label :=
+ number.label #1 + 'number.label :=
+ label width$ longest.label.width >
+ { label 'longest.label :=
+ label width$ 'longest.label.width :=
+ }
+ 'skip$
+ if$
+}
+EXECUTE {initialize.longest.label}
+ITERATE {longest.label.pass}
+FUNCTION {begin.bib}
+{ preamble$ empty$
+ 'skip$
+ { preamble$ write$ newline$ }
+ if$
+ "\begin{thebibliography}{" longest.label * "}" *
+ write$ newline$
+ "\providecommand{\url}[1]{\texttt{#1}}"
+ write$ newline$
+ "\providecommand{\urlprefix}{URL }"
+ write$ newline$
+}
+EXECUTE {begin.bib}
+EXECUTE {init.state.consts}
+ITERATE {call.type$}
+FUNCTION {end.bib}
+{ newline$
+ "\end{thebibliography}" write$ newline$
+}
+EXECUTE {end.bib}
+%% End of customized bst file
+%%
+%% End of file `titto.bst'.
+
+
|