Viktor Kuncak
where else to find them
what they talk about
where they keep going back
- VMCAI3 editions2022–2025
all 4 in the filters
on a stage with
all 8 in the filters
who talks about the same things
- Adam Chlipala23 talks
- Sharon Shoham13 talks
- Alex Aiken8 talks
- Oded Padon11 talks
- Takeshi Tsukada16 talks
- Samuel Gruetter5 talks
| title | conference | date |
|---|---|---|
| Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study | VMCAI 2025 | 2025-01-20 |
Adds a verified Scala backend to ASN1SCC and uses Stainless verifier to prove crash freedom and semantic properties for generated serializers. Builds a Scala… | ||
| Interpolation and Quantifiers in Ortholattices | VMCAI 2024 | 2024-01-15 |
Sequent proof system for quantified orthologic is sound and complete for complete ortholattices, and validity checking runs in quadratic-time decision and… | ||
| Orthologic with Axioms | POPL 2024 | 2024-01-14 |
Presents orthologic extended with axioms and proves a generalized cut‑elimination and subformula property that yields a concrete decision procedure… | ||
| Proving and Disproving Equivalence of Functional Programming Assignments | PLDI 2023 | 2023-06-17 |
A tool implemented on top of the Stainless verifier automatically proves or disproves student Scala submissions by generating inductive equivalence proofs or… | ||
| Generalized Arrays for Stainless Frames | VMCAI 2022 | 2022-01-16 |
Implements a verification pipeline in Stainless (Scala) that encodes dynamic frames without quantifiers by lowering heaps to arrays and emitting Z3’s extended… | ||
| Keynote: Tools for Verified Scala | Scala Days Copenhagen 2017 | 2017-05-30 |
A verification toolchain centered on Stainless (evolved from Leon) analyzes a pure-Scala subset, emits concrete counterexamples, and proves correctness for all… | ||
| nothing matches | ||