Re: [madPL] PL Seminar Tomorrow

[JOHN CYPHERT <jcyphert@xxxxxxxx>]

Reminder,

This is in 5 minutes.

John

---

From: Pl-seminar <pl-seminar-bounces@xxxxxxxxxxx> on behalf of JOHN CYPHERT <pl-seminar-bounces@xxxxxxxxxxx>
Sent: Thursday, October 8, 2020 11:54 AM
To: pl-seminar@xxxxxxxxxxx <pl-seminar@xxxxxxxxxxx>
Subject: [madPL] PL Seminar Tomorrow

 

Hi everyone, 

We will be having a PL seminar tomorrow Oct 9 at 1pm. Jialu will be presenting the PLDI 2020 paper Data-Driven Inference of Representation Invariants.

Here is the abstract for the paper:

A representation invariant is a property that holds of all values of abstract type produced by a module. Representation invariants play important roles in software engineering and program verification. In this paper, we develop a counterexample-driven algorithm for inferring a representation invariant that is sufficient to imply a desired specification for a module. The key novelty is a type-directed notion of visible inductiveness, which ensures that the algorithm makes progress toward its goal as it alternates between weakening and strengthening candidate invariants. The algorithm is parameterized by an example-based synthesis engine and a verifier, and we prove that it is sound and complete for first-order modules over finite types, assuming that the synthesizer and verifier are as well. We implement these ideas in a tool called Hanoi, which synthesizes representation invariants for recursive data types. Hanoi not only handles invariants for first-order code, but higher-order code as well. In its back end, Hanoi uses an enumerative synthesizer called Myth and an enumerative testing tool as a verifier. Because Hanoi uses testing for verification, it is not sound, though our empirical evaluation shows that it is successful on the benchmarks we investigated.

 

See you tomorrow,

John

Join Zoom Meeting
https://uwmadison.zoom.us/j/97079120314?pwd=UFN3c3lDcWlieWdqdjVUNnk4aVZXUT09

Meeting ID: 970 7912 0314
Passcode: 790380
One tap mobile
+19292056099,,97079120314#,,,,,,0#,,790380# US (New York)
+13017158592,,97079120314#,,,,,,0#,,790380# US (Germantown)

Dial by your location
        +1 929 205 6099 US (New York)
        +1 301 715 8592 US (Germantown)
        +1 312 626 6799 US (Chicago)
        +1 669 900 6833 US (San Jose)
        +1 253 215 8782 US (Tacoma)
        +1 346 248 7799 US (Houston)
Meeting ID: 970 7912 0314
Passcode: 790380
Find your local number: https://uwmadison.zoom.us/u/aiMtYuleM

Join by SIP
97079120314@xxxxxxxxxxx

Join by H.323
162.255.37.11 (US West)
162.255.36.11 (US East)
115.114.131.7 (India Mumbai)
115.114.115.7 (India Hyderabad)
213.19.144.110 (Amsterdam Netherlands)
213.244.140.110 (Germany)
103.122.166.55 (Australia)
149.137.40.110 (Singapore)
64.211.144.160 (Brazil)
69.174.57.160 (Canada)
207.226.132.110 (Japan)
Meeting ID: 970 7912 0314
Passcode: 790380