発表時間：[C1] 25分、[C2] 20分、[C3] 2時間、[C4] 50分、[招待講演] 1時間 （いずれも質疑応答含む）
SAT ソルバーの求解性能が 2000 年以降飛躍的に向上している． さらに近年は単純に命題論理式の充足解を求めるだけでなく， 充足解が存在しない場合に，非充足となるような命題論理式の部分集合 (UNSAT コアと呼ばれる) を計算するなどの高度な機能も研究されている．
本サーベイ・チュートリアル発表では， SAT ソルバーに興味がある人， SATソルバーを使ってみたいと考えている人を対象に， SAT ソルバーの最新の動向および SAT 符号化，インクリメンタル SAT， Counterexample Guided Abstraction Refinement (CEGAR)， UNSAT コアなど SAT ソルバーを利用するための技術を例を交えながら紹介する． 本発表を通じて SAT ソルバーを利用する面白さを共有できればと考えている．
本発表では，仮想マシン(VM)稼動させたまま別の物理マシンへと移動させるライブ VM 移送の実現技術とその最新動向について，およびライブ VM 移送技術とプログラミング言語分野との接点に迫ることで，新たな研究課題の発見を試みる．VM とは，VM モニタと呼ばれるソフトウェアによって提供される仮想的なハードウェアであり，これらを 1 台の物理マシンで複数作成することで複数の OS を同時に稼動できる．ライブ VM 移送は，VM を停止させることなく別のマシンへ移動できるため，VM の再配置による負荷分散や消費電力削減に効果的であることが知られている．技術的に興味深い部分が多く，著者を含め世界中の大学や企業において盛んに研究されている技術のひとつである．ライブ VM 移送の性能は VM の上で稼働しているプログラムの挙動に大きく依存しており，その挙動の把握や動作保証，最適化はライブ VM 移送の効率化および高機能化に大きく寄与するため，プログラミング言語分野で培われた手法はライブ VM 移送技術を発展させる可能性がある．
NOTICE: PPL aims to function as an informal workshop series, which gives researchers an opportunity to disseminate their preliminary work and get feedback from the participants without precluding publication elsewhere. It encourages submissions of revised versions of the work to international conferences or refereed journals.
The second category of PPL ([C2] in the program above) is intended to help researchers disseminate their research to the domestic community by providing an opportunity to present their papers that have already been accepted by international conferences or journals (but not presented in Japan before). Therefore, presentations in this category, which are informal, should not be considered republication or results of double submissions of any kind.