News

11/08/21

Our paper on a formal foundation for symbolic evaluation will appear at POPL 2022.

03/27/21

Oak gave a talk on Rosette 4.0 at Racketfest.

03/12/21

Released Rosette 4.0: a new runtime and new language features!

03/11/21

Emina and Xi gave a talk on Rosette and Jitterbug at Algorand.

02/19/21
01/19/21
11/12/20

Luke gave a talk on Jitterbug at Brown Systems Seminar.

10/23/20

Emina gave a colloquium talk on Rosette and Jitterbug at the University of Iowa.

10/22/20

Xi gave a talk on Jitterbug at Columbia Systems Seminar.

09/25/20

Xi gave a talk on Jitterbug at Cornell Systems Lunch.

08/31/20

Our paper on noninterference specifications for secure systems appeared in Operating Systems Review.

08/28/20
08/14/20

Our paper on verifying BPF just-in-time compilers in the Linux kernel using Jitterbug will appear at OSDI 2020.

07/21/20

Xi gave a keynote on Serval at VSTTE 2020.

06/19/20

Emina served as the Program Chair for PLDI 2020.

04/05/20

Our paper on synthesizing JIT compilers for in-kernel DSLs will appear at CAV 2020.

02/24/20

Helgi defended his Ph.D.!

11/21/19

Published a technical report on building security monitors on RISC-V and our experience with using the HiFive Unleashed.

11/07/19

Our paper on fixing performance bottlenecks in code under symbolic evaluation will appear at VMCAI 2020.

10/28/19

Our paper on scaling automated verification with Serval won a best paper award and a distinguished artifact award at SOSP 2019.

10/27/19

Luke, Emina, and Xi gave a tutorial on Serval at SOSP 2019.

10/24/19

Published a technical report on our experience with Nickel.

10/18/19
08/20/19

Emina gave a keynote on solver-aided programming at ICFP 2019.

07/25/19
07/22/19

Our paper on scaling automated verification using Serval will appear at SOSP 2019.

07/14/19

Emina gave a tutorial on solver-aided programming at CAV 2019.

05/29/19

James defended his Ph.D.!

03/12/19

Xi received an NSF CAREER Award.

10/26/18
09/10/18

We received an NSF FMitF Award to work on synthesis of OS components.

09/07/18

Our paper on symbolic profiling won a Distinguished Artifact Award at OOPSLA 2018.

08/24/18

Released Rosette 3.0: new performance engineering tools and new solvers!

08/16/18

Our paper on symbolic profiling for solver-aided languages and frameworks will appear at OOPSLA 2018.

07/20/18

Our paper on the Nickel framework for design and verification of information flow control systems will appear at OSDI 2018.

07/16/18

Emina gave a keynote on solver-aided programming at ISSTA 2018.

06/08/18

Bruno won the 2018 Best Senior Thesis Award for his thesis on a crash-safe key-value store using chained copy-on-write B-trees.

05/22/18

Emina gave a two-day course on Rosette at the Eighth Summer School on Formal Techniques (SSFT 2018).

05/11/18

Emina got tenure!

03/26/18

Xi received a 2017 Google Faculty Award.

01/18/18

James received a 2018 Facebook Fellowship.

12/18/17

James was interviewed for the People of Programming Languages series at POPL 2018.

10/06/17

Helgi, Luke, and Xi gave a talk on push-button verification at the 2017 New England Systems Verification Day.

09/19/17

Our paper on push-button verification of an OS kernel will appear at SOSP 2017.

04/13/17

Our paper on synthesizing memory models will appear at PLDI 2017.

03/31/17
02/08/17

Emina received an NSF CAREER Award.

11/01/16

Our paper on push-button verification of file systems won a best paper award at OSDI 2016.

09/18/16
07/30/16

Our paper on push-button verification of file systems will appear at OSDI 2016.

07/22/16
07/12/16

James gave an invited talk at the Programming Languages Mentoring Workshop co-located with PLDI 2016.

04/15/16

Our paper on verifying a radiotherapy machine will appear at CAV 2016.

03/25/16

Released Rosette 2.0: new theories, better performance!

02/28/16
01/28/16

Our paper on file system crash-consistency models will appear at ASPLOS 2016.

01/01/16

Our paper on optimizing synthesis with metasketches will appear at POPL 2016.