HATRA 2022
| title | author | length |
|---|---|---|
| Program Synthesis Using Example Propagation | Niek Mulleners | 33m |
A synthesizer called scribe generates expressions for a statically typed functional language with algebraic data types by combining a provided type… | ||
| A Survey of Weak Reasoning Assistants | Matthew Sotoudeh | 32m |
Argues that a practical middle ground between raw LaTeX and fully sound proof assistants exists and is useful, surveying concrete tools: a LaTeX linting… | ||
| Exploring the Verifiability of Code Generated by GitHub Copilot | Dakota Wong, Austin Copic, Patrick Lamb | 30m |
Authors feed six algorithmic problems to GitHub Copilot, add hand‑crafted pre/postconditions and loop invariants, translate generated Python into Dafny, and… | ||
| Holbert: Reading, Writing, Proving and Learning in the Browser | Liam O'Connor | 33m |
Holbert is a browser-based pedagogical proof assistant and online textbook platform that embeds editable proof exercises and rule definitions directly in… | ||
| Some Problems with Properties: A Study on Property-Based Testing in Industry | Harry Goldstein | 26m |
A preliminary interview study with seven interviews finds engineers struggle to write generators (failing to satisfy nontrivial preconditions, bad… | ||
| Discussion | Michael Coblenz, Alan Jeffrey | 01h 01m |
Discussion argues that automated proof generation from LLMs and tools like CoPilot has a roughly 40% chance of working for real verification workflows, but… | ||
| Static Information Flow Control Made Simple | Hannah Gooney, Jonathan Aldrich | 32m |
Proposes a rule-based IFC that unifies confidentiality and integrity by declaring concrete flows between modules, using overrides via lexical scope to allow… | ||
| nothing matches | ||