Partially Complete Quantifier Elimination (EGRAPHS 2023 - E-Graph Research, Applications, Practices, and Human-factors Symposium)

Sat 17 - Wed 21 June 2023 Orlando, Florida, United States

Who

Isabel Garcia-Contreras, Hari Govind V K, Sharon Shoham, Arie Gurfinkel

Track

EGRAPHS 2023

Time Zone

The program is currently displayed in (GMT-04:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-04:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Sun 18 Jun 2023 11:40 - 12:00 at Magnolia 18 - EGRAPHS: Verification

Abstract

We present QEL, an algorithm to perform quantifier elimination using egraphs. QEL is fast and complete relative to ground definitions entailed by the formula.

Link to Preprint

https://arxiv.org/abs/2306.10009

File attachments

Slides (EGRAPHS23_slides_export.pdf)	1.84MiB
Extended abstract (qel_egraphs.pdf)	389KiB

Isabel Garcia-Contreras

University of Waterloo

Canada

Hari Govind V K

University of Waterloo

Sharon Shoham

Tel Aviv University

Israel

Arie Gurfinkel

University of Waterloo

Canada

Time Zone

The program is currently displayed in (GMT-04:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-04:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

Sun 18 Jun
Displayed time zone: Eastern Time (US & Canada) change

11:20 - 12:30	EGRAPHS: VerificationEGRAPHS at Magnolia 18 #egraphs-sun-magnolia18

11:20 20m Talk		KestRel: Relational Verification using E-Graphs for Program Alignment EGRAPHS Robert Dickerson Purdue University, Benjamin Delaware Purdue University File Attached
11:40 20m Talk		Partially Complete Quantifier Elimination EGRAPHS Isabel Garcia-Contreras University of Waterloo, Hari Govind V K University of Waterloo, Sharon Shoham Tel Aviv University, Arie Gurfinkel University of Waterloo Pre-print File Attached
12:00 20m Talk		Ensuring the termination of equality saturation for terminating term rewriting systems EGRAPHS Yihong Zhang University of Washington, Oliver Flatt University of Washington Link to publication Pre-print File Attached