add FSE paper + other small updates

_config.yml

@@ -82,9 +82,9 @@ analytics:
 author:
   name             : "Kesha Hietala"
   avatar           : "profile.jpg"
-  bio              : "Applied Scientist in Automated Reasoning"
+  bio              : "Computer Science Researcher"
   location         :
-  employer         : "Amazon AWS"
+  employer         : 
   pubmed           :
   googlescholar    : "https://scholar.google.com/citations?user=SXWh3IYAAAAJ&hl=en"
   email            :

_pages/about.md

@@ -7,13 +7,13 @@ redirect_from:
   - /about.html
 ---
 
-Hello! My name is Kesha, and I'm an Applied Scientist in the Automated Reasoning in Identity Group at Amazon AWS.
+Hello! My name is Kesha.
 I'm interested in **compilers**, **program analysis** and **formal verification**.
 I got my PhD in 2022 in [Computer Science at the University of Maryland](https://www.cs.umd.edu/), where I was advised by [Mike Hicks](https://mhicks.me/).
 I did my undergraduate in [Computer Science at the University of Minnesota](https://cse.umn.edu/cs).
 
 For my dissertation, I designed and implemented SQIR, a *small quantum intermediate representation* embedded in the Coq proof assistant, and VOQC, a *verified optimizer for quantum circuits*. You can learn more about SQIR and VOQC in [this blog post](https://blog.sigplan.org/2021/06/02/verifying-a-quantum-compiler/), or you can check out [my dissertation](../files/drafts/khieta-dissertation.pdf).
 
-At Amazon, I work on the [Cedar authorization language](https://www.cedarpolicy.com).
+I spent two years as an Applied Scientist in the Automated Reasoning in Identity Group at Amazon (AWS) where I worked on the [Cedar authorization language](https://www.cedarpolicy.com).
 
 In my free time, I enjoy include puzzles, painting, and spending time with my three cats and husband, [Thomas Rolinger](https://www.researchgate.net/profile/Thomas_Rolinger).

_pages/cv.md

@@ -18,7 +18,7 @@ redirect_from:
   * Minors in Mathematics and Asian Languages and Literatures (Japanese)
 
 ##  Work experience
-I joined AWS full time in July 2022.
+I worked at Amazon (AWS) July 2022 - September 2024.
 
 During my time as a student, I was fortunate enough to have several internships:
 * Microsoft Quantum, Summer 2021
@@ -70,7 +70,7 @@ During my time as a student, I was fortunate enough to have several internships:
 
 ## Academic Service
 * PC member for Coq Workshop 2022, PLanQC 2022 & 2024, CPP 2024, ICFP 2024
-* AEC member & external reviewer for OOPSLA 2024 & 2024
+* AEC member & external reviewer for OOPSLA 2023 & 2024
 * External reviewer for TQC 2020, MFCS 2022, PLDI 2023
 * Sub-reviewer for CCS 2017, Oakland S&P 2017, RC 2019, PLDI 2020, QCTIP 2020, PLDI 2021, OOPSLA 2021
 * Student volunteer at POPL 2020

_publications/cedar-fse24.md

@@ -0,0 +1,14 @@
+---
+title: "How We Built Cedar: A Verification-Guided Approach"
+collection: publications
+permalink: /publications/cedar-fse24
+excerpt: 
+date: 2024-07-10
+venue: 'Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering (FSE)'
+link: 'https://dl.acm.org/doi/abs/10.1145/3663529.3663854'
+paperurl: 'https://arxiv.org/pdf/2407.01688'
+github: 'https://github.com/cedar-policy'
+citation: 'Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, <b>Kesha Hietala</b>, John Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, Andrew Wells. &quot;How We Built Cedar: A Verification-Guided Approach.&quot; <i>Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering (FSE)</i>. 2024.'
+abstract: "This paper presents verification-guided development (VGD), a software engineering process we used to build Cedar, a new policy language for expressive, fast, safe, and analyzable authorization. Developing a system with VGD involves writing an executable model of the system and mechanically proving properties about the model; writing production code for the system and using differential random testing (DRT) to check that the production code matches the model; and using property-based testing (PBT) to check properties of unmodeled parts of the production code. Using VGD for Cedar, we can build fast, idiomatic production code, prove our model correct, and find and fix subtle implementation bugs that evade code reviews and unit testing. While carrying out proofs, we found and fixed 4 bugs in Cedar’s policy validator, and DRT and PBT helped us find and fix 21 additional bugs in various parts of Cedar."
+---
+Industry track paper