diff --git a/_config.yml b/_config.yml
index 75cc416..7b43000 100644
--- a/_config.yml
+++ b/_config.yml
@@ -9,4 +9,3 @@ github_username:  rucs-uoft
 # Build settings
 markdown: kramdown
 permalink: /:title
-highlighter: rouge
\ No newline at end of file
diff --git a/_includes/2019/issue.html b/_includes/2019/issue.html
deleted file mode 100644
index 0ea7937..0000000
--- a/_includes/2019/issue.html
+++ /dev/null
@@ -1,58 +0,0 @@
-<div class="current-issue">
-
-  <div class="hide-on-small-and-down"><img src="assets/2019/banner.png"/></div>
-  <div class="hide-on-med-and-up show-on-small"><img src="assets/2019/banner-small.png"/></div>
-
-
-    <ul class="collapsible" data-collapsible="accordion">
-      <li>
-        <div class="collapsible-header toc-title">Letter From the Editor</div>
-        <div class="collapsible-body">
-          <!--content-->
-          {% include 2019/letter.html %}
-        </div>
-      </li>
-      <li>
-        <div class="collapsible-header toc-title">Our Team</div>
-        <div class="collapsible-body">
-          <!--content-->
-          {% include 2019/team.html %}
-        </div>
-      </li>
-    </ul>
-
-  <ul class="collection submissions-list with-header">
-        <a href="/automated-program-synthesis" class="submission" target="_blank">
-          <div class="submission-number">1</div>
-          <div class="submission-info">
-            <div class="submission-category">Software Engineering</div>
-            <div class="submission-title">Automated Program Synthesis</div>
-            <div class="submission-author">Yizhe Cheng and Bence Weisz</div>
-          </div>
-        </a>
-        <a href="/aiutare-a-modular-benchmarking-framework" class="submission" target="_blank">
-          <div class="submission-number">2</div>
-          <div class="submission-info">
-            <div class="submission-category">Software Engineering</div>
-            <div class="submission-title">Aiutare: A Modular Benchmarking Framework</div>
-            <div class="submission-author">Lukas Finnbarr O'Callahan and David Tang</div>
-          </div>
-        </a>
-        <a href="/layer-wise-contrastive-unsupervised-representation-learning" class="submission" target="_blank">
-          <div class="submission-number">3</div>
-          <div class="submission-info">
-            <div class="submission-category">Machine Learning</div>
-            <div class="submission-title">Layer-Wise Contrastive Unsupervised Representation Learning</div>
-            <div class="submission-author">Stephen Zhao</div>
-          </div>
-        </a>
-        <a href="/expediting-verification-of-assertions-in-loops-by-isolation" class="submission" target="_blank">
-          <div class="submission-number">4</div>
-          <div class="submission-info">
-            <div class="submission-category">Verification, Software Engineering</div>
-            <div class="submission-title">Expediting Verification of Assertions in Loops by Isolation</div>
-            <div class="submission-author">Murad Akhundov and Federico Mora</div>
-          </div>
-        </a>
-      </ul>
-</div>
diff --git a/_includes/2019/letter.html b/_includes/2019/letter.html
deleted file mode 100644
index 6a44d31..0000000
--- a/_includes/2019/letter.html
+++ /dev/null
@@ -1,19 +0,0 @@
-<p>Dear reader,</p>
-
-    <p>
-        I will not dedicate this letter to addressing for the $nth$ time "the unprecedented times" that we all find ourselves in, except  
-    in passing. For many of us, including myself, it has been a disorienting year. If we have the privilege of having loved ones, hobbies, and intellectual pursuits in our lives,
-    we should by all means enjoy them, and remind ourselves that these are the things that ultimately anchor our lives, not the changeable circumstances we happen to find ourselves in.
-    </p>
-    <p>
-        We will be bringing you a reduced number of articles this year - this is by no means a statement on their quality. I am happy to have read each of these works
-        and I hope that you will be as well. It's great to see that research still continues on at U of T, and that many undergrads are continuing to lend their ideas, work ethic, and fresh perspectives to the department.
-    </p>
-    <p>
-        I would also like to thank the team that made this issue possible - thank you for your hard work. I would also like to thank Sam Toueg for his guidance, as well as Danya Lette and John Chen for their tireless support
-        and guidance. It's heartening to think that so many people who have led RUCS in the past continue to be involved. Though things haven't gone the way that I intended this year, I plan to continue to be involved in RUCS 
-        in the future as well, and I hope that those who have submitted their work have also been encouraged to do research, or expand their horizons.
-    </p>
-<p> <br/> <br/> Emmy Liu <br/>
-    <em>2019-2020 Editor-in-Chief</em>, <br/> RUCS
-</p>
diff --git a/_includes/2019/team.html b/_includes/2019/team.html
deleted file mode 100644
index 3a8c0ea..0000000
--- a/_includes/2019/team.html
+++ /dev/null
@@ -1,63 +0,0 @@
-
-<div class="container">
-	<div class="row team-member-row">
-		<div class="team-member" style="text-align:center;">
-			<img class="responsive-img" src="/resources/team_photos/emmy_photo.jpg" style="max-width:250px;">
-		</div>
-		<div class="team-member" >
-			<h4>Emmy Liu</h4>
-			<h6>Editor-in-Chief</h6>
-			<p>Emmy is a computer science specialist and cognitive science major in her fourth year. She has worked in several labs on work ranging from computational linguistics to human-computer interaction to machine learning. Outside of school and work, she enjoys listening to audiobooks, playing video games, and taking long walks.</p>
-		</div>
-	</div>
-	<div class="row team-member-row">
-		<div class="team-member" style="text-align:center;">
-			<img class="responsive-img" src="/resources/team_photos/danya_photo.png" style="max-width:250px;">
-		</div>
-		<div class="team-member" >
-			<h4>Danya Lette</h4>
-			<h6>Senior Advisor</h6>
-			<p>Danya is a computer science specialist with an interest in theory and programming languages. She has an eclectic background, and formerly completed a degree in philosophy at U of T. Danya spends her free time playing with her dog, reading novels, eating popcorn, and thinking about thinking.</p>
-		</div>
-	</div>
-	<div class="row team-member-row">
-		<div class="team-member" style="text-align:center;">
-			<img class="responsive-img" src="/resources/team_photos/arif_photo.jpg" style="max-width:250px;">
-		</div>
-		<div class="team-member" >
-			<h4>Arif Aulakh</h4>
-			<h6>Editor</h6>
-			<p>Arif Aulakh is a Mathematics and Computer Science student entering his 2nd year. He is passionate about topics in Computer Science as Artificial Intelligence, Data Science, and Algorithms. In his free time, Arif likes to go biking, play poker, and watch basketball.</p>
-		</div>
-	</div>
-	<div class="row team-member-row">
-		<div class="team-member" style="text-align:center;">
-			<img class="responsive-img" src="/resources/team_photos/evan_photo.jpg" style="max-width:250px;">
-		</div>
-		<div class="team-member" >
-			<h4>Evan Kanter</h4>
-			<h6>Editor</h6>
-			<p>Evan Kanter is a Computer Science Specialist (AI Focus) and Ethics, Society, and Law Major at the University of Toronto, in his 3rd academic year. Evan is passionate about Artificial Intelligence, in particular, the intersection between AI, Ethics, and Law. Evan has volunteered as an editor of RUCS to contribute to Computer Science research, learn more about the publishing process, and help fellow CS students publish their work. Outside of school, Evan enjoys playing guitar, skiing, reading, volunteering on political campaigns, competing in Mock Trial and Moot competitions, and following baseball.</p>
-		</div>
-	</div>
-	<div class="row team-member-row">
-		<div class="team-member" style="text-align:center;">
-			<img class="responsive-img" src="/resources/team_photos/fiona_photo.jpg" style="max-width:250px;">
-		</div>
-		<div class="team-member" >
-			<h4>Qiyuan He</h4>
-			<h6>Editor</h6>
-			<p>Qiyuan He is a computer science specialist with a focus in artificial intelligence. With mathematics and statistical science backgrounds, she loves learning new things and turning ideas into reality. In her free time, Qiyuan enjoys traveling, drinking coffee, and listening to Bach.</p>
-		</div>
-	</div>
-	<div class="row team-member-row">
-		<div class="team-member" style="text-align:center;">
-			<img class="responsive-img" src="/resources/team_photos/yaseen_photo.jpg" style="max-width:250px;">
-		</div>
-		<div class="team-member" >
-			<h4>Yaseen Hoque</h4>
-			<h6>Social Media Coordinator</h6>
-			<p>I am a computer science major at UTM that loves to make robots and stuff.I watch music and listen to anime like a weeb. Listen to me on soundcloud if you are true to the streets. Peace out.</p>
-		</div>
-	</div>
-</div>
diff --git a/_includes/archive.html b/_includes/archive.html
index 4c060aa..1a2627e 100644
--- a/_includes/archive.html
+++ b/_includes/archive.html
@@ -3,8 +3,7 @@
 		<h3>Past Issues</h3>
 	</div>
 	<ul>
-	<li><a href="{{ site.baseurl }}/archive_2018"><b>2018-2019</b></a></li>
-	<li><a href="{{ site.baseurl }}/archive_2017"><b>2017-2018</b></a></li>
+		<li><a href="{{ site.baseurl }}/archive_2017"><b>2017-2018</b></a></li>
   	<li><a href="{{ site.baseurl }}/archive_2016"><b>2016-2017</b></a></li>
   	<li><a href="{{ site.baseurl }}/archive_2015"><b>2015-2016</b></a></li>
 	<ul>
diff --git a/_includes/head.html b/_includes/head.html
index 2fca47f..8b3e603 100644
--- a/_includes/head.html
+++ b/_includes/head.html
@@ -48,8 +48,6 @@
   <link href="{{ site.baseurl }}/css/post.css" type="text/css" rel="stylesheet" media="screen,projection" />
   {% endif %}
 
-  <!-- Rouge Syntax Highlighting -->
-  <link href="{{ site.baseurl }}/css/syntax.css" rel="stylesheet" />
   <!-- MathJax -->
 <script type="text/x-mathjax-config">
   MathJax.Hub.Config({
diff --git a/_includes/partials/download-button.html b/_includes/partials/download-button.html
deleted file mode 100644
index ed09c32..0000000
--- a/_includes/partials/download-button.html
+++ /dev/null
@@ -1,6 +0,0 @@
-<a class="btn-link" href="{{ include.link }}" download>
-    <button type="button">
-      <img src="/assets/icons/download.svg" alt="Download paper PDF">
-      Get the PDF
-    </button>
-  </a>
\ No newline at end of file
diff --git a/_includes/table_of_contents.html b/_includes/table_of_contents.html
index 35f2b27..7105a99 100644
--- a/_includes/table_of_contents.html
+++ b/_includes/table_of_contents.html
@@ -65,7 +65,7 @@
 
 
         <div class="toc-chapter-content" id="current-issue">
-          {% include 2019/issue.html %}
+          {% include 2018/issue.html %}
         </div>
 
         <div class="toc-chapter-content" id="archive">
@@ -120,7 +120,7 @@
           <div class="collapsible-header toc-title">Current Issue</div>
           <div class="collapsible-body">
               <!--content-->
-              {% include 2019/issue.html %}
+              {% include 2018/issue.html %}
           </div>
       </li>
 
diff --git a/_posts/2019/2019-08-13-Y-Cheng.md b/_posts/2019/2019-08-13-Y-Cheng.md
deleted file mode 100644
index 93ea1cc..0000000
--- a/_posts/2019/2019-08-13-Y-Cheng.md
+++ /dev/null
@@ -1,107 +0,0 @@
----
-layout: post
-title: "Automated Program Synthesis"
-author: "Yizhe Cheng and Bence Weisz"
-supervisors: "Victor Nicolet, Anthony Vandikas, and Azadeh Farzan"
-category: "Software Engineering"
-permalink: /automated-program-synthesis
-year: "2020"
-
----
-
-1 Introduction
-============
-
-Writing a correct computer program can be both difficult and tedious. To simplify the work of software developers, program synthesizers are used to aid with this. Synthesizers are themselves programs that automatically generate programs for developers based on some specifications. Previously, researchers have used syntactic guided methods for synthesizing programs whereby a rough skeleton of the program code---a syntactic template---is provided by a user to aid in finding a correct program. Unfortunately, in many practical cases it is hard for a user to provide a template [1]. We introduce a method for automated program synthesis, where the synthesis algorithm generates a program through an iterative process. For the purpose of this project, the specification consists of a precondition, a postcondition, and a list of program statements. 
-
-2 Background
-==========
-
- A trace is a sequence of program statements in the order that they are executed in a program run. A program can be represented as a set of traces; together these traces represent all possible executions of that program. Moreover, a trace is correct if and only if assuming the precondition, the program variables satisfy the postcondition after the execution of the trace.
-
- In order to verify the correctness of a program, there are two important properties that need to be checked, safety and liveness. A program satisfies the safety property if all traces of the program are correct. A program satisfies the liveness property if the program eventually terminates for all possible inputs.
-
- We denote the set of programs by $\mathscr{L}(P)$. A program is well-formed if the program is constructed according to the syntax rules. $\mathscr{L}(P)$ is constructed to only represent the sets of traces that are well-formed programs. In simplified terms, a set of traces is a well-formed program if a syntactically valid program can be constructed from the set of traces.
-
- Another important concept in our approach is the representation of correct programs. We denote the set of correct traces $\Pi$. From $\Pi$, we use power set construction described in [3] to compute $\mathscr{P}(\Pi)$, the power set of $\Pi$. $\mathscr{P}(\Pi)$ consists of all subsets of the traces in $\Pi$. If a program whose set of all possible executions is a set of traces in $\mathscr{P}(\Pi)$, then that program must be safe because every trace of that program is also in $\Pi$ by definition. However, not every set of traces in $\mathscr{P}(\Pi)$ is a well-formed program. We also define the set $\Omega$ to contain the set of all terminating traces which can intuitively be grouped to form a terminating program.
-
-3 Approach
-========
-
-We use a counterexample Guided Abstraction Refinement or CEGAR loop approach as first described in [2], where we take counterexamples — in the form of a trace — and generalize from them to improve our proofs. Generalizing a trace involves deriving similar traces which are correct for the same reason as the given trace is. We will first show our methods for synthesizing safe programs. Next, we will shows ways in which our methods can be extended to synthesize safe and terminating programs.
-
-To synthesize safe programs, we need to find correct traces until the algorithm finds a program that is well-formed and satisfies the safety property. To find correct traces, we take a set of traces in $\overline{\Pi}$, which consist of traces whose correctness is unknown, as counterexamples. Then, using Satisfiability Modulo Theorems or SMT solver, we generate interpolants from the counterexamples and generalize $\Pi$ from the interpolants [5]. Next, we compute $\mathscr{L}(P)\cap\mathscr{P}(\Pi)$, which contains only sets of traces that are safe, well-formed programs, and check its emptiness [6]. In the case that $\mathscr{L}(P)\cap\mathscr{P}(\Pi)$ is empty, more counterexamples are taken from $\overline{\Pi}$, and interpolants are computed from them to generalize $\Pi$ until $\mathscr{L}(P)\cap\mathscr{P}(\Pi)$ is no longer empty, in which case a safe program can be extracted from $\mathscr{L}(P)\cap\mathscr{P}(\Pi)$. This concept is illustrated in Figure 1. In the diagram below, $CE$ denotes counterexample.
-
-#### Figure 1: The CEGAR loop for synthesizing safe programs.
-<p style="text-align: center;">
-	<img align="middle" style="margin:50" height="75%" width="75%" src="{{ site.baseurl }}/assets/2019/Cheng-1.png"/>
-</p>
-
-#### Figure 2: The CEGAR loop for synthesizing programs that satisfy the liveness and safety properties.
-
-<p style="text-align: center;">
-	<img align="middle" style="margin:50" height="75%" width="75%" src="{{ site.baseurl }}/assets/2019/Cheng-2.png"/>
-</p>
-
-To ensure the generated program also satisfies the liveness property, the approach simultaneously shows that there is a non-empty set of terminating traces. As defined earlier, this set will be denoted by $\Omega$. $\Omega$ is modified using a similar CEGAR approach as was used for generating programs that satisfy the safety property. In this modified approach, counterexamples are taken from the set which is the intersection of the traces in $inf(\Pi)$ and the traces which have not already been added to $\Omega$, expressed as $\overline{L(\Omega)}$. The traces in $inf(\Pi)$ are traces whose prefixes have correct extensions in $\Pi$. On the other hand, the traces in the set $\overline{L(\Omega)}$ are traces which have not been verified to be terminating yet. Then the traces in the intersected set,  $inf(\Pi) \cap \overline{L(\Omega)}$, are counterexamples which are correct extensions to their prefixes, and ones that have not been analyzed for termination. The analysis of these traces is explained bellow. An example of these traces is shown in Figure 3. The automaton in the diagram will accept any trace that increments $i$ as long as $i<n$, and the trace must be finitely long since eventually, $i$ will be greater or equal to $n$.
-
-#### Figure 3: An infinite counterexample.
-
-<p style="text-align: center;">
-	<img align="middle" style="margin:50" height="75%" width="75%" src="{{ site.baseurl }}/assets/2019/Cheng-3.png"/>
-</p>
-
-To verify the termination of these unchecked counterexamples, a method described in [4] is used. Terminating counterexamples are added to $\Omega$, along with their generalized counterexamples. The purpose of generalizing traces in $\Omega$ is to add additional traces to $\Omega$ which are also terminating. These traces are terminating for the same reason that the counterexamples of interest were in the termination analysis.
-
-To synthesize a terminating program, the terminating traces in $\Omega$, are grouped together into combinations of traces. As described earlier, $\mathscr{L}(P) \cap \mathscr{P}(\Pi)$ is the set of well-formed programs which are correct. In processes of generating a program which also terminates, the set of terminating programs $P(\Omega)$, is also intersected with the two sets. This way, if the overall set is non-empty, then there is a well-formed program which is correct and terminating. This process can been seen in Figure 2.
-
-4 Analysis
-========
-
-First, we consider a special case of synthesis known as verification. This involves taking a program, along with encodings of a set of pre-conditions and post-conditions, and verifying that this program satisfies both of those sets. In this special case, $\mathscr{L}(P)$ contains a single program. Our goal is to verify the safety property of the program using our synthesis loop. We believe the worst-case time complexity for our algorithm is in NP, but We are able to verify in 560s that the program in Figure 4 indeed finds the largest element in an array. 
-
-#### Figure 4: A program that finds the largest element in the array A.
-
-<p style="text-align: center;">
-	<img align="middle" style="margin:50" height="50%" width="50%" src="{{ site.baseurl }}/assets/2019/Cheng-4.png"/>
-</p>
-
-Next, using the loop in Figure 2, we attempt to synthesize a terminating program that increments the variable $i$ until $i$ equals to the variable $n$. However, the generalization procedure for $\Omega$ is not functioning as intended so, instead, the set of traces represented by the automaton in Figure 5a is passed in as $\Omega$. Eventually, the program in Figure 5b is synthesized in 382s, but we believe the worst-case time complexity for this algorithm is also in NP.
-
-#### Figure 5
-
-<div class="row" style="display:flex; align-items:center;">
-  <div class="column" width="50%" style="display:flex; flex-direction:column;">
-    <p style="text-align: center;">
-        <img align="middle" src="{{ site.baseurl }}/assets/2019/Cheng-5-a.png"/>
-    </p>
-    <p style="text-align:center;font-size:0.95rem"><b>(a) </b>A representation of infinite traces that must eventually terminate.</p>
-  </div>
-  <div class="column" width="50%" style="display:flex; flex-direction:column;">
-    <p style="text-align: center;">
-        <img align="middle" src="{{ site.baseurl }}/assets/2019/Cheng-5-b.png"/>
-    </p>
-    <p style="text-align:center;font-size:0.95rem"><b>(b) </b>A synthesized program that increases i until i reaches n. i is initially 0 and n is greater than 0.</p>
-  </div>
-</div>
-
-5 Conclusion 
-===
-
-Automated programming tools will be an invaluable tool to programmers in the future. Unfortunately, as outlined in the analysis, these methods seem wildly slow even for trivial algorithms. The complexity of most of the set operations as well as the generalization operations lead to an exponential or worse blow up in complexity. As a result, the development of efficient algorithms for each of these tasks will be vital if progress is to be made on improving the CEGAR synthesis approach.
-
-### References
-
-1. Allessandro Abate et al. "Counterexample guided inductive synthesis modulo theories", In *Computer Aided Verification*. H. Chockler and G. Weissenbacher, Eds. Cham: Springer International Publishing, 2018. pp.270-288.
-
-2. E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, "Counterexample-Guided Abstraction Refinement", in *Computer Aided Verification*. E. A. Emerson and A. P. Sistla, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2000. pp.154-169. 
-
-3. Azadeh Farzan and Anthony Vandikas. "Automated Hypersafety Verification", in *Computer Aided Verification*. I. Dillig and S. Tasiran, Eds. Cham: Springer International Publishing, 2019. pp.200-218.
-
-4. M. Heizmann, H. Jochen, P. Andreas., "Termination Analysis by Learning Terminating Programs", in *Computer Aided Verification*, A. Biere and R. Bloem, Eds. Cham: Springer International Publishing, 2014. pp. 797-813.
-
-5. M. Heizmann, J. Hoenicke, and A. Podelski., "Refinement of Trace Abstraction", in *Static Analysis*. J. Palsberg and Z. Su, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009. 2009. pp. 69-85.
-
-6. Moshe Y. Vardi and Pierre Wolper, "Automata-Theoretic Techniques for Modal Logics of Programs", *Journal of Computer and System Sciences*, vol. 32, pp. 183-221, 1986.
-
-{% include partials/download-button.html link="/assets/2019/pdf/Cheng_2020.pdf"%}
\ No newline at end of file
diff --git a/_posts/2019/2019-08-15-L-OCallahan.md b/_posts/2019/2019-08-15-L-OCallahan.md
deleted file mode 100644
index 7832446..0000000
--- a/_posts/2019/2019-08-15-L-OCallahan.md
+++ /dev/null
@@ -1,161 +0,0 @@
----
-layout: post
-title: "Aiutare: A Modular Benchmarking Framework"
-author: "Lukas Finnbarr O'Callahan and David Tang"
-supervisors: "Marsha Chechik and Frederico Mora"
-category: "Software Engineering"
-permalink: /aiutare-a-modular-benchmarking-framework
-year: "2020"
-
----
-
-1 Introduction
-============
-
-The process of benchmarking software on numerous queries can produce a large amount of information, such as program execution runtimes and properties of each input query. Effectively using this information to gain new insights into program performance and correctness is challenging. In response to this difficulty, we developed Aiutare: a modular benchmarking framework that runs on a set of user-defined programs and their input benchmark files. Aiutare helps researchers by abstracting the benchmarking and data storage processes, allowing users to easily manipulate output for visualization, plotting, and testing. In this paper, we introduce
-the framework and demonstrate its flexibility by applying it to find bugs in the solutions generated by popular SMT solvers. 
-
-
-
-2 Description of Aiutare
-==========
-
-Aiutare is a Python program outlined in Fig. 1 and detailed below. We chose Python for the project as all University of Toronto computer science students are familiar with the language.
-
-## 2.1 Inputs
-The user provides Aiutare with a file named config.py which consists of a dictionary containing the following items:
-<ol>
-  <li>A set of $P$ <b>programs</b> (1.1), provided as a list of filepaths to the program executables, including any command-line arguments.</li>
-  <li>A set of $F$ <b>input files</b> (1.2), provided as a list of filepaths. All $P$ programs provided should be able to run these input files and print output to the console.</li>
-  <li>A set of $P$ <b>schemas</b> (1.3), provided as a list of filepaths to Python files. We provide default schemas to record program runtime and answers, but the user can optionally write a custom schema in the form of a Python function for each program.</li>
-</ol>
-
-### Figure 1: Aiutare framework architecture.
-<p style="text-align: center;">
-	<img align="middle" style="margin:50" height="80%" width="80%" src="{{ site.baseurl }}/assets/2019/OCallahan-1.png"/>
-</p>
-
-## 2.2 Subprocess Manager
-
-The Subprocess Manager (2) uses Python’s subprocess module to run every program on every input file in parallel. The `Popen` interface is used to execute child programs; each invocation consists of a filepath to the program executable (1.1) including any desired command-line arguments, and the filepath of the input file (1.2). A complete invocation should be able to run directly in the terminal and have the format:
-
-```sh
-path/to/program_exe -arg=true test_input_file.txt
-```
-
-## 2.3 Output Parser
-
-After terminating, each child program spawned by the Subprocess Manager (2) has its console output redirected to the Output Parser (3). Here, the appropriate program-specific schema (1.3) provided by the user is called to parse this output text into a dictionary of variables describing the performance and results of the child program. This dictionary is then written to Aiutare’s MongoDB database (4) as a MongoEngine schema object [2].
-
-## 2.4 MongoDB Database
-
-Once the Output Parser (3) finishes writing all results to the MongoDB database (4), Aiutare terminates and prints a summary of the benchmarking to the console. The results of the database can then be easily queried as MongoEngine objects or by using any compatible library or application, such as the MongoDB Compass GUI [1]. MongoDB was chosen as the database for Aiutare because it requires no adherence to fixed schemas or knowledge of SQL.
-
-3 Evaluation
-========
-
-We use a domain-specific instantiation of Aiutare to evaluate its effectiveness. We aim to answer <b>RQ1</b>: given a research question $RQ_D$ in domain D, can Aiutare be adapted to generate meaningful results to aid in answering $RQ_D$?
-
-We selected satisfiability modulo theories (SMT) solvers as our domain and asked the research question $RQ_{SMT}$ : can we develop a method to systematically validate the solutions produced by SMT solvers in order to catch bugs in these tools?
-
-To the best of our knowledge, no systematic validation of SMT solver solutions exists in the literature, making our bug identification method a useful contribution to the field of SMT solver
-research.
-
-## 3.1 Domain: SMT Solvers
-
-SMT solvers take SMT queries as input; a query is in the form of a set of variables and a set of constraints on these variables, as seen in Fig. 2.
-
-The solver outputs the answer SAT if all constraints can be satisfied simultaneously, or UNSAT otherwise. If the solver answers SAT, then it also provides a solution: an SMT query with a concrete value assigned to each variable, as shown in Fig. 3.
-
-SMT queries and SMT solver outputs are also easy to manipulate without modification due to standardization under SMT-LIB [3]; this consistency allowed us to provide Aiutare with a single schema to handle output from all SMT solvers, simplifying our development process.
-
-### Figure 2: Example SMT Query.
-
-<p style="text-align: center;">
-	<img align="middle" style="margin:50" height="80%" width="80%" src="{{ site.baseurl }}/assets/2019/OCallahan-2.png"/>
-</p>
-
-### Figure 3: Example SMT Solution.
-
-<p style="text-align: center;">
-	<img align="middle" style="margin:50" height="55%" width="55%" src="{{ site.baseurl }}/assets/2019/OCallahan-3.png"/>
-</p>
-
-## 3.2 Setup
-
-Our approach to answer $RQ_{SMT}$ consists of two calls to Aiutare and a database parsing procedure.
-
-In the first Aiutare call, the user inputs are:
-
-<ol>
-  <li><b>programs </b>= an arbitrary number of SMT solvers.</li>
-  <li><b>input files </b>= an arbitrary number of SMT queries.</li>
-  <li><b>schemas </b>= modified Python functions that also write solver-produced solutions to the database every time a solver returns SAT.</li>
-</ol>
-
-Next, the second Aiutare call takes as inputs:
-
-<ol>
-  <li><b>programs </b>= all SMT solvers.</li>
-  <li><b>input files </b>= all solver-produced solutions stored in the database after the first Aiutare call.</li>
-  <li><b>schemas </b>= default schemas to record answers of SAT/UNSAT.</li>
-</ol>
-
-Once Aiutare has populated the database with these results, the remainder of the approach filters through the data, highlighting each program run where a solver called on an SMT query produced an erroneous answer and/or solution (Fig. 4). One bug type occurs when a solver answers UNSAT but a counterexample in the form of a supported solution disproves this answer. Another bug type occurs when a solution is deemed UNSAT by one or more solvers.
-
-### Figure 4: Two Types of Bugs.
-
-<p style="text-align: center;">
-	<img align="middle" style="margin:50" height="75%" width="75%" src="{{ site.baseurl }}/assets/2019/OCallahan-4.png"/>
-</p>
-
-We selected three versions of Z3 and CVC4 to evaluate:
-
-<ul>
-  <li><b>z3_seq </b>- Z3 using *seq*, the default string solver.</li>
-  <li><b>z3_str3 </b>- Z3 using *Z3str3* [4], a new alternative string solver.</li>
-  <li><b>cvc4 </b>- CVC4 using the default string solver [5].</li>
-</ul>
-
-We ran these solvers on 17,936 SMT queries generated by the Kudzu symbolic execution framework [6].
-We implemented our approach in less than 200 lines of Python, and ran the configuration of Aiutare located at [https://github.com/FinnbarrOC/aiutare](https://github.com/FinnbarrOC/aiutare) on a machine running 64-bit Ubuntu 18.04.Most of the script interacts with well-documented MongoDB APIs, requiring no knowledge of the inner workings of Aiutare. This level of abstraction combined with reliance on common MongoDB libraries ensures that Aiutare is easy to modify and use.
-
-
-## 3.3 Results
-
-We were able to systematically find nine bugs: three unsupported solutions and four disproven answers of UNSAT with z3_seq, and two unsupported solutions with cvc4.
-
-An example bug taken from the test set of queries is shown in Fig. 5. This subtle bug is hard to catch because z3_seq gave the correct result, SAT, but provided the wrong solution.
-
-<p style="text-align: center;">
-	<img align="middle" style="margin:50" height="75%" width="75%" src="{{ site.baseurl }}/assets/2019/OCallahan-5.png"/>
-</p>
-
-Therefore, we positively answer $RQ_{SMT}$ and <b>RQ1</b>.
-
-4 Summary and Future Work
-===
-
-Overall, we adapted Aiutare to analyze SMT solvers and answer a domain-specific research question, showcasing the flexibility of our framework. Our case study demonstrated that Aiutare can be used to find real-world bugs in current industrial software.
-
-In the future, we plan to apply Aiutare to analyze the runtime performance of SMT and SAT solvers, test verification tools and equivalence checkers, and generate plots and regression models to describe program performance metrics.
-
-## Acknowledgements
-
-We thank Professor Marsha Chechik, Federico Mora, and the UofT Modeling Group for their mentorship and feedback. This research was supported by NSERC.
-
-### References
-
-1. [n.d.]. Compass. [https://www.mongodb.com/products/compass](https://www.mongodb.com/products/compass)
-
-2. [n.d.]. MongoEngine. [http://mongoengine.org/](http://mongoengine.org/)
-
-3. Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2017. The SMT-LIB Standard: Version 2.6.Technical Report. Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org.
-
-4. M. Berzish, V. Ganesh, and Y. Zheng. 2017. Z3str3: A String Solver with Theory-aware Heuristics. In 2017 Formal Methods in Computer Aided Design (FMCAD). 55–59.
-
-5. Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, and Morgan Deters. 2016. An Efficient SMT Solver for String Constraints. Formal Methods in System Design 48, 3 (June 2016), 206–234. https://doi.org/10.1007/s10703-016-0247-6
-
-6. Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen McCamant, and Dawn Song. [n.d.. A Symbolic Execution Framework for JavaScript.
-
-{% include partials/download-button.html link="/assets/2019/pdf/OCallahan_2020.pdf"%}
\ No newline at end of file
diff --git a/_posts/2019/2019-08-16-S-Zhao.md b/_posts/2019/2019-08-16-S-Zhao.md
deleted file mode 100644
index e196551..0000000
--- a/_posts/2019/2019-08-16-S-Zhao.md
+++ /dev/null
@@ -1,89 +0,0 @@
----
-layout: post
-title: "Layer-Wise Contrastive Unsupervised Representation Learning"
-author: "Stephen Zhao"
-supervisors: "Silviu Pitis"
-category: "Artificial Intelligence/Machine Learning"
-permalink: /layer-wise-contrastive-unsupervised-representation-learning
-year: "2020"
-
----
-
-1 Introduction 
-===
-
-Existing machine learning models typically require large amounts of labeled data, which can be costly to obtain. Feature representations learned in an unsupervised manner let us leverage existing unlabeled data, with immediate applications in transfer learning, such as weight initialization for faster learning, or better performance if labeled data for the downstream task is scarce. Representations learned in an unsupervised manner are also likely better than those from a supervised task if the downstream task focuses on features irrelevant to the upstream supervised training task. In this work, we focus on the set of unsupervised learning approaches that Arora et al. (2019) [1] call “contrastive unsupervised representation learning”. We use a layer-wise adaptation, starting within the context of images. We train feature representations of semantically similar images (i.e. nearby patches within the same image) to be closer than that of unrelated images (e.g. random patches), to learn convolutional neural network filters from unlabeled data.
-
-We hypothesize our layer-wise approach will be faster than end-to-end training, particularly if we only transfer a few layers. Works such as Yosinski et al. (2014) [10] demonstrate that in certain multi-layer neural network architectures, the first few layers learn more “general” features that are most transferable, suggesting that we only need to learn and transfer a few layers. Grinberg et al. (2019) [5] demonstrate that local Hebbian learning of first-layer filters can be almost as good as end-to-end learning, but at a much faster training speed. Motivated by these results, we believe we can achieve similar performance in the transfer learning setting to end-to-end learning but with faster training time.
-
-2 Related Work 
-===
-
-<b>Unsupervised Representation Learning </b>Arora et al. (2019) [1] use the term “Contrastive Learning” for methods that contrast pairs of semantically similar text or images with negative (for example, random) samples. In the context of unsupervised representation learning, the objective is for representations of the positive (similar) pair to be closer to each other than the negative pair. Their theoretical framework involves first drawing from a distribution of latent classes (unobserved semantically meaningful categories), and then drawing from an associated distribution of possible inputs (e.g.images) conditional on the latent class. In this setup, the loss in contrastive unsupervised representation learning is an upper bound on the lowest possible loss on a downstream supervised task involving the same set of latent classes. Thus, the feature representations that minimize loss on the unsupervised task are useful for the supervised task.
-
-Contrastive learning with visual data is often done by comparing image patches. Wang & Gupta (2015) [8] work with videos, generating samples by tracking patches of motion. The first and last tracked frames become the positive pair, and can be contrasted with a random patch. Patches are passed through a siamese-triplet network involving both convolutional and fully-connected layers, and loss is based on the cosine distance of final feature representations. Doersch et al. (2015) [3] instead consider two input image patches, a center patch and one of eight possible neighbour patches; the training task is to classify the spatial location of the neighbouring patch.
-
-Dosovitskiy et al. (2014) [4] approach the idea of extracting information from semantically similar image patches by applying a series of transformations (translation, scaling, rotation, contrast) to a sample patch to generate a class. Generated classes then form a batch to which classification algorithms can be applied.
-
-<b>Layer-Wise Learning </b>Compared to standard end-to-end learning, layer-wise learning can provide faster training. Grinberg et al. (2019) [5] use a local Hebbian learning rule for unsupervised learning of the first layer weights. They achieve almost as good results on transfer learning tasks with much less wall-clock training time, concluding that general features, learned independently from lower layers, work well for the first layer.
-
-<b>Transfer Learning </b>Works such as Yosinski et al. (2014) [10] and Lee et al. (2017) [7]demonstrate that, at least in certain convolutional network architectures, the first few layers contain general features that are most useful for transfer, and that transferring a few lower layers is almost as good as transferring all layers for fine-tuning. This suggests that a fast layer-wise training algorithm could achieve additional time savings in transfer learning.
-
-3 Methodology
-===
-
-<b>Implementation Details </b>Given a dataset of images, we sample adjacent patches (overlapping, drawn from a larger patch) and pass them through a single layer of convolutional filters, followed by max-pooling. The resulting embeddings are passed through a triplet loss function, where the contrastive distance is based on either a cosine similarity or Euclidean norm metric. (Code is available at [https://github.com/Silent-Zebra/shallow-conv](https://github.com/Silent-Zebra/shallow-conv))
-
-We found that small patches, such as the minimum 7x7 for a 6x6 filter with 2x2 max-pooling, worked as well for the first layer as larger patch sizes, such as 10x10. This is consistent with an interpretation of our patch sampling method as similar (in expectation) to applying a convolutional layer on a larger patch. Max-pooling is essential for learning filters such as edge detectors, as it provides translation invariance.
-
-<b>Preliminary Results </b>Using CIFAR-100, with labels removed, as the unsupervised learning training set, we learn first-layer 6x6 convolutional filters that look similar to those learned from supervised training (compare Figure 1 and Figure 2 in the appendix). We test these filters in a transfer learning setting, training a simple classifier (2 convolutional layers and 2 fully connected layers) on CIFAR-10, where the first layer filters are the ones learned in the unsupervised setting, and are either 1) frozen or 2) fine-tuned. In the fine-tuning setting, the filters outperform random initialization (Figure 3). It would probably be difficult to beat supervised transfer in this case given that features useful for CIFAR-100 are likely also useful for CIFAR-10.
-
-
-### Figure 1: Unsupervised Filters
-<p style="text-align: center;">
-	<img align="middle" style="margin:50" height="65%" width="65%" src="{{ site.baseurl }}/assets/2019/Zhao-1.PNG"/>
-</p>
-
-### Figure 2: Supervised Filters
-<p style="text-align: center;">
-	<img align="middle" style="margin:50" height="65%" width="65%" src="{{ site.baseurl }}/assets/2019/Zhao-2.PNG"/>
-</p>
-
-### Figure 3: Performance on CIFAR-10.
-<p style="text-align: center;">
-	<img align="middle" style="margin:50" height="65%" width="65%" src="{{ site.baseurl }}/assets/2019/Zhao-3.PNG"/>
-</p>
-<p style="text-align:center;font-size:0.95rem">The learning rate is 0.001 for the first two-thirds of the training, and is 0.0001 afterwards. Results are averaged over 3 independent runs for each line (keeping transferred filters constant across runs, but allowing for fine-tuning).</p>
-
-
-<b>Next Steps </b>Respectable performance in this simple environment motivates us to look at more complex datasets, as well as deeper, wider, or more modern network architectures. Regarding network architecture, the current state-of-the-art on CIFAR-10 appears to be an AmoebaNet-B (18, 512) architecture achieving 99.0% accuracy [6]. ResNets are also very popular, providing competitive results for example in [9] and [2]. We could start with common architectures used for testing unsupervised representation learning in the past such as AlexNet (e.g. in [8]) and VGG (e.g. in [3], also used by Arora et al. [1]), before moving on to more modern architectures.
-
-Other important next steps include multiple layers of layer-wise training and transfer, as well as comparison with end-to-end unsupervised learning. Additional future directions could include extensions to auxiliary tasks, looking at layer-wise supervised representation learning, extension to a semi-supervised learning setup, and possibly an extension beyond images to more general settings where we can define notions of semantic similarity.
-
-## Acknowledgements
-
-Thanks to Silviu Pitis for guidance, advice, and mentorship throughout this project.
-
-### References
-
-1. S. Arora, H. Khandeparkar, M. Khodak, O. Plevrakis, and N. Saunshi. A theoretical analysis of contrastive unsupervised representation learning, 2019.
-
-2. T. DeVries and G. W. Taylor. Improved regularization of convolutional neural networks with cutout, 2017.
-
-3. C. Doersch, A. Gupta, and A. A. Efros. Unsupervised visual representation learning by context prediction. *2015 IEEE International Conference on Computer Vision (ICCV)*, pages 1422–1430, 2015.
-
-4. A. Dosovitskiy, P. Fischer, J. T. Springenberg, M. A. Riedmiller, and T. Brox. Discriminative unsupervised feature learning with exemplar convolutional neural networks. *IEEE Transactions on Pattern Analysis and Machine Intelligence*, 38:1734–1747, 2014.
-
-5. L. Grinberg, J. Hopfield, and D. Krotov. Local unsupervised learning for image analysis. *arXiv preprint arXiv:1908.08993*, 2019.
-
-6. Y. Huang, Y. Cheng, A. Bapna, O. Firat, M. X. Chen, D. Chen, H. Lee, J. Ngiam, Q. V. Le, Y. Wu, and Z. Chen. Gpipe: Efficient training of giant neural networks using pipeline parallelism, 2018.
-
-7. J. Y. Lee, F. Dernoncourt, and P. Szolovits. Transfer learning for named-entity recognition with neural networks. *arXiv preprint arXiv:1705.06273*, 2017.
-
-8. X. Wang and A. Gupta. Unsupervised learning of visual representations using videos. 2015 *IEEE International Conference on Computer Vision (ICCV)*, pages 2794–2802, 2015.
-
-9. Y. Yamada, M. Iwamura, T. Akiba, and K. Kise. Shakedrop regularization for deep residual learning, 2018.
-
-10. J. Yosinski, J. Clune, Y. Bengio, and H. Lipson. How transferable are features in deep neural networks? In *NIPS*, 2014.
-
-{% include partials/download-button.html link="/assets/2019/pdf/Zhao_2020.pdf"%}
\ No newline at end of file
diff --git a/_posts/2019/2020-08-13-M-Akhundov.md b/_posts/2019/2020-08-13-M-Akhundov.md
deleted file mode 100644
index e74a631..0000000
--- a/_posts/2019/2020-08-13-M-Akhundov.md
+++ /dev/null
@@ -1,130 +0,0 @@
----
-layout: post
-title: "Expediting Verification of Assertions in Loops by Isolation"
-author: "Murad Akhundov and Federico Mora"
-supervisors: "Marsha Chechik"
-category: "Software Engineering/Software Verification"
-permalink: /expediting-verification-of-assertions-in-loops-by-isolation
-year: "2020"
-
----
-
-1 Introduction
-============
-Program verification engines, or verifiers, are tools that take in a program with assertions, and attempt to prove that the assertions always hold. In this paper, we will focus on Bounded Model Checking, a popular verification technique. Bounded Model Checkers (BMCs) [3], often struggle to check assertions in unbounded loops, loops with high bounds, or nested loops. This is because, for unbounded loops, no number of loop unrollings is sufficient; with high loop bounds, a large number of loop unrollings is required; and with nested loops, even a small number of loop unrolling results in a large SAT encoding. Consider the example in Listing 1. A BMC needs to unroll the loops $\mathcal{O}{(SIZE)^2}$ times to prove the assertion, when `SIZE = 200`, a state-of-the-art BMC, CBMC [4] takes over 10 minutes. In this paper, we propose a novel technique that proves the same assertion in under 10 seconds, and improves the performance of CBMC on many other similar cases while incurring a manageable overhead cost.
-
-#### Listing 1: Nested Loop
-```c
-void two_sum_prev(int *arr, int s){ //check if two elements in arr add to s
-    for (int i = 0; i < SIZE; i++){ //SIZE is some fixed number
-       for (int j = 0; j < i; j++){
-           assert(j < SIZE);
-           if(arr[j] + arr[i] == s) printf("found!"); }}}
-```
-
-The key observation that our technique exploits is that inner segments of the program-under-test are often sufficient to prove that an assertion always holds. As seen in Listing 1, the information needed to prove the assertion is entirely contained in the body of the outer loop and its condition. Specifically, to prove that `j < SIZE`, it is sufficient to know that `j < i` and `i < SIZE`, and that the loop will terminate (i.e., `j` is eventually `i`). We propose a technique to find these segments and expedite verification. Our tool, Qicc finds and isolates these segments so that they can be verified individually, quickly, and concurrently.
-
-2 Background
-==========
-This section introduces *control-flow graphs (CFGs)*, which we use to model programs, and *extracted loops*, which are the isolated components of control-flow-graphs that Qicc verifies individually.
-
-A *CFG* is a directed graph representing flow-of-control between statements in programs [1]. We say that a sub-graph $G'$ of a graph $G$ has a *single entry* (respectively, exit) if there is only one edge coming into (respectively, leaving) $G'$ from (respectively, to) the rest of graph $G$. $G'$ is *local* if it has a single entry and exit.  We say $G'$  is a *loop* if every node in $G'$ can be reached from every other node in $G'$, and if $G'$ contains at least two nodes. $G'$ is a *local loop* if it is local and a loop, and if its single entry is its single exit. We call the entry/exit node the *root* of the local loop. We call the sub-graph of a local loop without its root the *body* of the local loop. A local loop is *extracted* when all nodes in its body are moved to a new function.
-
-3 Our Approach
-========
-
-Qicc speeds up verification of nested assertions by extracting local loops and calling the verification tool on the new functions. Qicc uses CBMC [4] but the same approach can be used with other tools. 
-
-Qicc takes three steps: it finds local loops, extracts them, and checks them individually. For each individual check, Qicc executes the verifier as a child process, to allow for concurrent solving. If the verifier succeeds, Qicc labels the function/node as successfully verified otherwise, Qicc attempts verification on the caller/parent of that function. Qicc reports success if all assertions have been verified; Qicc reports failure if it finds a function with no parent that cannot be verified.
-
-#### Listing 2: Original Code
-```c
-void main(){
-    int n, x = 1;
-    
-    while (n < 1000){
-        assert(x == 1);
-        n += x; }}
-```
-#### Listing 3: After Extraction
-```c
-void main(){
-    int n, x = 1;
-    while (n < 1000) e1(&n, x);}
-
-int e1(int *n, int x){
-    assume(*n < 1000);
-    assert(x == 1);
-    *n += x;}
-```
-
-Listings 2 and 3 show the result of a single extraction. Qicc extracts the loop condition and inserts it into the extracted function, `e1`, that can be also used for checking any assertions in the loop. As shown in the listings, the assertion in `e1` cannot be shown to always hold with the information present from `e1`, as `x` is taken as parameter. In such cases, the underlying verifier will fail and Qicc will execute that tool on the caller of `e1` (in this case, that is the main function).
-
-To find local loops, we first identify all *Strongly Connected Components (SCCs)* in the CFG using Tarjan's Algorithm [6]. By definition, every node in an SCC can be reached from every other node, and each SCC contains all such nodes [1] [6]. To find nested loops, we remove the root of the loop and apply the algorithm to the rest of the SCC, this process will break apart the SCC and will reveal any nested loops. Once the loops are identified, each loop is checked for locality by using depth-first search on the root. We implemented the identification and extraction algorithms in OCaml using CIL [5]. Tool source is available with supplementary material [2].
-
-4 Evaluation
-========
-
-Since Qicc was designed to take advantage of cases when loop bodies are sufficient to prove the assertion, we say that Qicc *hits* when that is the case and *misses* otherwise. We had the following research questions: How much faster is Qicc when it hits? How costly are misses?
-
-We compared performance of Qicc to CBMC on 10 benchmarks selected to cover a broad range of cases; we highlight four in Table 1. The `2 Sum fixed` examples are the motivating example in Section 1; `variable` accepts arrays with arbitrary bounds instead; `Factorial Sum` has an unbounded loop but its body is sufficient to prove the assertion.
-
-The `2 Sum fixed` examples are cases where Qicc hits; however, with small input size Qicc's overhead is larger than CBMC's running time. With large input size, however, Qicc's performance is much better than that of CBMC, as the number of unrollings required grows much faster with nested loops. These examples also illustrate that Qicc's performance scales very well with input size, as the increase in Qicc's running time is minimal. We argue that the overhead is manageable when considering the performance boost gained for loops with large bounds. Qicc was also able to quickly check examples like `Factorial Sum`, where CBMC timed-out. For `variable` loops where Qicc misses, both tools timed-out. We did not study how frequent hits and misses are in the real world, and this is a threat to validity. We plan to study this in the future.
-
-#### Table 1: Benchmark Results
-<div style="overflow-x:auto">
-<table>
-    <tr>
-        <th class="space" colspan="1"></th>
-        <th>Time (seconds)</th>
-        <th class="space" colspan="1"></th>
-    </tr>
-    <tr>
-        <th width="50%">Test/Tool</th>
-        <th width="25%">CBMC</th>
-        <th width="25%">Qicc (CBMC)</th>
-    </tr>
-    <tr>
-        <td>2 Sum - fixed 10</td>        
-        <td>0.7</td>
-        <td>4.9</td>
-    </tr>
-    <tr>
-        <td>2 Sum - fixed 100</td>        
-        <td>98.8</td>
-        <td>5.8</td>
-    </tr>
-    <tr>
-        <td>2 Sum - variable</td>        
-        <td>>10m</td>
-        <td>>10m</td>
-    </tr>
-    <tr>
-        <td>Factorial Sum</td>        
-        <td>>10m</td>
-        <td>8.4</td>
-    </tr>
-</table>
-</div>
-
-
-5 Conclusion and Future Work
-========
-
-Loops with high or arbitrary bounds are very common in programs, and it can often be helpful to verify assertions in them. BMCs like CBMC struggle with such loops due to the number of required unrollings. As demonstrated in this abstract, isolated segments can be sufficient to prove assertions and the proof can be done quickly. Qicc builds on these ideas and is able to considerably improve performance of CBMC for such cases, while introducing only a manageable overhead. In the future, we intend to benchmark Qicc on real-world programs to find the frequency of hits and misses.
-
-### References
-
-1. Alfred V Aho, Monica S Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, techniques, and tools second edition. Pearson Education Addison Wesley New York, 2007.
-
-2. Murad Akhundov. Qicc. <https://github.com/MuradAkh/Qicc>, 2019.
-
-3. Armin Biere, Alessandro Cimatti, Edmund M Clarke, Ofer Strichman, Yunshan Zhu, et al. Bounded model checking. Advances in computers, 58(11):117–148, 2003.
-
-4. Daniel Kroening and Michael Tautschnig. Cbmc–c bounded model checker. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 389–391. Springer, 2014.
-
-5. George C Necula, Scott McPeak, Shree P Rahul, and Westley Weimer. Cil: Intermediate language and tools for analysis and transformation of C programs. In International Conference on Compiler Construction, pages 213–228. Springer, 2002.
-
-6. Robert Tarjan. Depth-first search and linear graph algorithms. SIAM journal on computing, 1(2):146–160, 1972.
-
-{% include partials/download-button.html link="/assets/2019/pdf/Akhundov_2020.pdf"%}
\ No newline at end of file
diff --git a/_sass/post.scss b/_sass/post.scss
index b08f5dc..b132577 100644
--- a/_sass/post.scss
+++ b/_sass/post.scss
@@ -98,23 +98,6 @@
 			}
 			padding-left: 40px !important;
 		}
-
-		.btn-link {
-			display: flex;
-			justify-content: center;
-			padding: 2em;
-
-			button {
-				display: flex;
-				flex-direction: row;
-				justify-content: space-evenly;
-				color: black;
-				width: 30%;
-				border-radius: 10px;
-				background-color: transparent;
-				height: 75px;
-			}
-		}
 	}
 }
 
diff --git a/_sass/style.scss b/_sass/style.scss
index b7df381..2d32790 100644
--- a/_sass/style.scss
+++ b/_sass/style.scss
@@ -48,9 +48,9 @@ $background: url("../resources/backgroundweb2017.svg");
 $toc-height: 570px;
 $toc-width: 896px;
 
-//html * {
-	//font-family: $post-font;
-//}
+html * {
+	font-family: $post-font;
+}
 
 img, figure {
 	max-width: 100%;
diff --git a/archive_2018.html b/archive_2018.html
deleted file mode 100644
index b348c42..0000000
--- a/archive_2018.html
+++ /dev/null
@@ -1,8 +0,0 @@
----
-layout: default
-title: "2018-2019"
-permalink: /archive_2018
----
-<div class="container" style="padding: 20px; margin-top: 30px">
-{% include 2018/issue.html %}
-</div>
\ No newline at end of file
diff --git a/assets/2019/Cheng-1.png b/assets/2019/Cheng-1.png
deleted file mode 100644
index ed90d6c..0000000
Binary files a/assets/2019/Cheng-1.png and /dev/null differ
diff --git a/assets/2019/Cheng-2.png b/assets/2019/Cheng-2.png
deleted file mode 100644
index d6af247..0000000
Binary files a/assets/2019/Cheng-2.png and /dev/null differ
diff --git a/assets/2019/Cheng-3.png b/assets/2019/Cheng-3.png
deleted file mode 100644
index 0ab5ea4..0000000
Binary files a/assets/2019/Cheng-3.png and /dev/null differ
diff --git a/assets/2019/Cheng-4.png b/assets/2019/Cheng-4.png
deleted file mode 100644
index 721978c..0000000
Binary files a/assets/2019/Cheng-4.png and /dev/null differ
diff --git a/assets/2019/Cheng-5-a.png b/assets/2019/Cheng-5-a.png
deleted file mode 100644
index d383a25..0000000
Binary files a/assets/2019/Cheng-5-a.png and /dev/null differ
diff --git a/assets/2019/Cheng-5-b.png b/assets/2019/Cheng-5-b.png
deleted file mode 100644
index 80bf9bd..0000000
Binary files a/assets/2019/Cheng-5-b.png and /dev/null differ
diff --git a/assets/2019/OCallahan-1.png b/assets/2019/OCallahan-1.png
deleted file mode 100644
index f0b5e85..0000000
Binary files a/assets/2019/OCallahan-1.png and /dev/null differ
diff --git a/assets/2019/OCallahan-2.png b/assets/2019/OCallahan-2.png
deleted file mode 100644
index f74488f..0000000
Binary files a/assets/2019/OCallahan-2.png and /dev/null differ
diff --git a/assets/2019/OCallahan-3.png b/assets/2019/OCallahan-3.png
deleted file mode 100644
index 97a7f8f..0000000
Binary files a/assets/2019/OCallahan-3.png and /dev/null differ
diff --git a/assets/2019/OCallahan-4.png b/assets/2019/OCallahan-4.png
deleted file mode 100644
index f17de4e..0000000
Binary files a/assets/2019/OCallahan-4.png and /dev/null differ
diff --git a/assets/2019/OCallahan-5.png b/assets/2019/OCallahan-5.png
deleted file mode 100644
index f5693fc..0000000
Binary files a/assets/2019/OCallahan-5.png and /dev/null differ
diff --git a/assets/2019/Zhao-1.PNG b/assets/2019/Zhao-1.PNG
deleted file mode 100644
index e6a1db7..0000000
Binary files a/assets/2019/Zhao-1.PNG and /dev/null differ
diff --git a/assets/2019/Zhao-2.PNG b/assets/2019/Zhao-2.PNG
deleted file mode 100644
index 4e9e5f7..0000000
Binary files a/assets/2019/Zhao-2.PNG and /dev/null differ
diff --git a/assets/2019/Zhao-3.PNG b/assets/2019/Zhao-3.PNG
deleted file mode 100644
index 8035156..0000000
Binary files a/assets/2019/Zhao-3.PNG and /dev/null differ
diff --git a/assets/2019/banner-small.png b/assets/2019/banner-small.png
deleted file mode 100755
index d01782b..0000000
Binary files a/assets/2019/banner-small.png and /dev/null differ
diff --git a/assets/2019/banner.png b/assets/2019/banner.png
deleted file mode 100755
index e2831a0..0000000
Binary files a/assets/2019/banner.png and /dev/null differ
diff --git a/assets/2019/pdf/Akhundov_2020.pdf b/assets/2019/pdf/Akhundov_2020.pdf
deleted file mode 100755
index 42eaa47..0000000
Binary files a/assets/2019/pdf/Akhundov_2020.pdf and /dev/null differ
diff --git a/assets/2019/pdf/Cheng_2020.pdf b/assets/2019/pdf/Cheng_2020.pdf
deleted file mode 100755
index 8070d03..0000000
Binary files a/assets/2019/pdf/Cheng_2020.pdf and /dev/null differ
diff --git a/assets/2019/pdf/OCallahan_2020.pdf b/assets/2019/pdf/OCallahan_2020.pdf
deleted file mode 100755
index 2de9d03..0000000
Binary files a/assets/2019/pdf/OCallahan_2020.pdf and /dev/null differ
diff --git a/assets/2019/pdf/Zhao_2020.pdf b/assets/2019/pdf/Zhao_2020.pdf
deleted file mode 100755
index a07220a..0000000
Binary files a/assets/2019/pdf/Zhao_2020.pdf and /dev/null differ
diff --git a/assets/icons/download.svg b/assets/icons/download.svg
deleted file mode 100644
index 76767a9..0000000
--- a/assets/icons/download.svg
+++ /dev/null
@@ -1 +0,0 @@
-<svg xmlns="http://www.w3.org/2000/svg" width="24" height="24" viewBox="0 0 24 24" fill="none" stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" class="feather feather-download"><path d="M21 15v4a2 2 0 0 1-2 2H5a2 2 0 0 1-2-2v-4"></path><polyline points="7 10 12 15 17 10"></polyline><line x1="12" y1="15" x2="12" y2="3"></line></svg>
\ No newline at end of file
diff --git a/css/post.css b/css/post.css
index 49d9762..5eb307e 100644
--- a/css/post.css
+++ b/css/post.css
@@ -5,24 +5,6 @@
  *
  * Made By MaterializeCSS.com
  */
-
-.btn-link {
-	display: flex;
-	justify-content: center;
-	padding: 2em;
-}
-.btn-link button {
-  display: flex;
-  flex-direction: row;
-  justify-content: space-evenly;
-  color: black;
-  width: 30%;
-  border-radius: 10px;
-  background-color: transparent;
-  height: 75px;
-}
-
-
 .materialize-red.lighten-5 {
   background-color: #fdeaeb !important; }
 
diff --git a/css/syntax.css b/css/syntax.css
deleted file mode 100644
index 596e408..0000000
--- a/css/syntax.css
+++ /dev/null
@@ -1,209 +0,0 @@
-.highlight table td { padding: 5px; }
-.highlight table pre { margin: 0; }
-.highlight .cm {
-  color: #999988;
-  font-style: italic;
-}
-.highlight .cp {
-  color: #999999;
-  font-weight: bold;
-}
-.highlight .c1 {
-  color: #999988;
-  font-style: italic;
-}
-.highlight .cs {
-  color: #999999;
-  font-weight: bold;
-  font-style: italic;
-}
-.highlight .c, .highlight .ch, .highlight .cd, .highlight .cpf {
-  color: #999988;
-  font-style: italic;
-}
-.highlight .err {
-  color: #a61717;
-  background-color: #e3d2d2;
-}
-.highlight .gd {
-  color: #000000;
-  background-color: #ffdddd;
-}
-.highlight .ge {
-  color: #000000;
-  font-style: italic;
-}
-.highlight .gr {
-  color: #aa0000;
-}
-.highlight .gh {
-  color: #999999;
-}
-.highlight .gi {
-  color: #000000;
-  background-color: #ddffdd;
-}
-.highlight .go {
-  color: #888888;
-}
-.highlight .gp {
-  color: #555555;
-}
-.highlight .gs {
-  font-weight: bold;
-}
-.highlight .gu {
-  color: #aaaaaa;
-}
-.highlight .gt {
-  color: #aa0000;
-}
-.highlight .kc {
-  color: #000000;
-  font-weight: bold;
-}
-.highlight .kd {
-  color: #000000;
-  font-weight: bold;
-}
-.highlight .kn {
-  color: #000000;
-  font-weight: bold;
-}
-.highlight .kp {
-  color: #000000;
-  font-weight: bold;
-}
-.highlight .kr {
-  color: #000000;
-  font-weight: bold;
-}
-.highlight .kt {
-  color: #445588;
-  font-weight: bold;
-}
-.highlight .k, .highlight .kv {
-  color: #000000;
-  font-weight: bold;
-}
-.highlight .mf {
-  color: #009999;
-}
-.highlight .mh {
-  color: #009999;
-}
-.highlight .il {
-  color: #009999;
-}
-.highlight .mi {
-  color: #009999;
-}
-.highlight .mo {
-  color: #009999;
-}
-.highlight .m, .highlight .mb, .highlight .mx {
-  color: #009999;
-}
-.highlight .sb {
-  color: #d14;
-}
-.highlight .sc {
-  color: #d14;
-}
-.highlight .sd {
-  color: #d14;
-}
-.highlight .s2 {
-  color: #d14;
-}
-.highlight .se {
-  color: #d14;
-}
-.highlight .sh {
-  color: #d14;
-}
-.highlight .si {
-  color: #d14;
-}
-.highlight .sx {
-  color: #d14;
-}
-.highlight .sr {
-  color: #009926;
-}
-.highlight .s1 {
-  color: #d14;
-}
-.highlight .ss {
-  color: #990073;
-}
-.highlight .s, .highlight .sa, .highlight .dl {
-  color: #d14;
-}
-.highlight .na {
-  color: #008080;
-}
-.highlight .bp {
-  color: #999999;
-}
-.highlight .nb {
-  color: #0086B3;
-}
-.highlight .nc {
-  color: #445588;
-  font-weight: bold;
-}
-.highlight .no {
-  color: #008080;
-}
-.highlight .nd {
-  color: #3c5d5d;
-  font-weight: bold;
-}
-.highlight .ni {
-  color: #800080;
-}
-.highlight .ne {
-  color: #990000;
-  font-weight: bold;
-}
-.highlight .nf, .highlight .fm {
-  color: #990000;
-  font-weight: bold;
-}
-.highlight .nl {
-  color: #990000;
-  font-weight: bold;
-}
-.highlight .nn {
-  color: #555555;
-}
-.highlight .nt {
-  color: #000080;
-}
-.highlight .vc {
-  color: #008080;
-}
-.highlight .vg {
-  color: #008080;
-}
-.highlight .vi {
-  color: #008080;
-}
-.highlight .nv, .highlight .vm {
-  color: #008080;
-}
-.highlight .ow {
-  color: #000000;
-  font-weight: bold;
-}
-.highlight .o {
-  color: #000000;
-  font-weight: bold;
-}
-.highlight .w {
-  color: #bbbbbb;
-}
-.highlight {
-  background-color: #f8f8f8;
-}
diff --git a/resources/team_photos/arif_photo.jpg b/resources/team_photos/arif_photo.jpg
deleted file mode 100644
index c2c614c..0000000
Binary files a/resources/team_photos/arif_photo.jpg and /dev/null differ
diff --git a/resources/team_photos/danya_photo.png b/resources/team_photos/danya_photo.png
deleted file mode 100644
index 6eb450d..0000000
Binary files a/resources/team_photos/danya_photo.png and /dev/null differ
diff --git a/resources/team_photos/emmy_photo.jpg b/resources/team_photos/emmy_photo.jpg
index 8fd217e..ef96eb6 100644
Binary files a/resources/team_photos/emmy_photo.jpg and b/resources/team_photos/emmy_photo.jpg differ
diff --git a/resources/team_photos/evan_photo.jpg b/resources/team_photos/evan_photo.jpg
deleted file mode 100644
index 5f84c86..0000000
Binary files a/resources/team_photos/evan_photo.jpg and /dev/null differ
diff --git a/resources/team_photos/fiona_photo.jpg b/resources/team_photos/fiona_photo.jpg
deleted file mode 100644
index e761401..0000000
Binary files a/resources/team_photos/fiona_photo.jpg and /dev/null differ
diff --git a/resources/team_photos/yaseen_photo.jpg b/resources/team_photos/yaseen_photo.jpg
deleted file mode 100644
index 4d2fa90..0000000
Binary files a/resources/team_photos/yaseen_photo.jpg and /dev/null differ