\documentclass[a4j,9.5pt]{article}
\usepackage{graphicx}
\usepackage{picins}
\usepackage{fancyhdr}
\usepackage[]{multicol}
\usepackage{listings}
%\pagestyle{fancy}
\lhead{\parpic{\includegraphics[height=1\zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部工学科知能情報コース 中間発表予稿}
\rhead{}
\cfoot{}

\setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
\setlength{\headheight}{0mm}
\setlength{\headsep}{5mm}
\setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
\setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
\setlength{\textwidth}{181mm}
\setlength{\textheight}{261mm}
\setlength{\footskip}{0mm}
\pagestyle{empty}
\usepackage[top=20mm, bottom=20mm, left=10mm, right=10mm]{geometry}
% 特殊文字の表示に必要
\usepackage{luatexja}
\usepackage{fontspec}
\setmainfont{STIX Math}%
\setmonofont{STIXGeneralBol}[
	Scale=MatchLowercase
]


\lstset{
  frame=single,
  keepspaces=true,
  stringstyle={\ttfamily},
  commentstyle={\ttfamily},
  identifierstyle={\ttfamily},
  keywordstyle={\ttfamily},
  basicstyle={\ttfamily},
  breaklines=true,
  xleftmargin=0\zw,
  xrightmargin=0\zw,
  framerule=.3pt,
  columns=[l]{fullflexible},
  numbers=left,
  stepnumber=1,
%  numberstyle={\scriptsize},
  numbersep=5pt,
  language={},
  tabsize=4,
  lineskip=-0.1\zw,
  escapechar={@},
}

\usepackage{indentfirst}
\usepackage{url}
\usepackage{amssymb}

%\bibliographystyle{plain}
%\bibliography{soto}
\usepackage[backend=biber, style=numeric]{biblatex}
\nocite{*}
\addbibresource{soto.bib}
%\bibliography{soto} %hoge.bibから拡張子を外した名前
%\bibliographystyle{junsrt} %参考文献出力スタイル

\setlength{\columnsep}{5mm}

\begin{document}
\ltjsetparameter{jacharrange={-3}}
\title{\LARGE Continuation based C による RedBlackTree の Hoare Logic を用いた検証 \\ \Large Verification of red-black tree implemented in Continuation based C using Hoare Logic}
\author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治}
\date{}
\maketitle
\thispagestyle{fancy}

% 要旨
\input{./tex/abstract.tex}

% 2段組開始
\begin{multicols*}{2}
    \input{tex/intro.tex} % 研究目的
    \input{tex/cbc.tex} % CbC の説明
    \input{tex/agda.tex} % agda の説明
    \input{tex/hoare.tex} % Hoare Logic の説明
	\input{tex/rbtree.tex} % 赤黒木の説明
    \input{tex/spec.tex}% 手法
    \input{tex/future.tex}% 今後の課題
	
% 参考文献	
% \begin{thebibliography}{9}
% \bibitem{cbc} 
% 	cbc-gcc - 並列信頼研 mercurial repository. \\
% 	\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}. 2020/09/10.
% \bibitem{ryokka} 
% 	Continuation based C での Hoare Logic を用いた仕様記述と検証. Master's thesis,\\
% 	琉球大学 大学院理工学研究科 情報工学専攻, 2020. 
% \bibitem{hoare} 
% 	C. A. R. Hoare. An axiomatic basis for computer programming. \\
% 	Commun. ACM, Vol. 12, No. 10, p. 576–580, October 1969.
% \bibitem{agda-wiki} 
% 	The agda wiki.  \\
% 	\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}. 2020/09/10.
% \bibitem{agda-doc} 
% 	Welcome to agda’s documentation!. \\ 
% 	\url{http://agda.readthedocs.io/en/latest/}. 2020/09/10.
% \bibitem{agda-book} 
% 	Aaron Stump. Verified Functional Programming in Agda. 
% 	Association for Computing Machinery and Morgan; Claypool, New York, NY, USA, 2016.
% \bibitem{atton} 
% 	比嘉健太. メタ計算を用いた continuation based c の検証手法. Master's thesis, \\
% 	琉球大学 大学院理工学研究科 情報工学専攻, 2017.
% \bibitem{meta} 
% 	徳森海斗. Llvm clang 上の continuation based c コンパイラ の改良. Master's thesis, \\
% 	琉球大学 大学院理工学研究科 情報工学専攻, 2016.
% \bibitem{rbtree} 
% 	渡邉敏正. データ構造と基本アルゴリズム. \\
% 	共立出版株式会社, 2015.
% \end{thebibliography}
% \printbibliography[title=参考文献]
	\printbibliography
\end{multicols*}

\end{document}