From Traces to Program Incorrectness: A Type-Theoretic Approach
summary
Claims a type-theoretic, underapproximate correctness method that treats library interactions as traces encoded with symbolic regular expressions and reasoned about via symbolic finite automata; a novel type-inference algorithm composes symbolic finite transducers to witness concrete incorrect behaviors (not just prove safety). The prototype leverages regex derivatives for falsification and offloads qualifiers to an SMT solver; transducers are currently expected from the user. The result is a compositional, trace-guided analysis that produces executable counterexamples when it succeeds.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 1:07Incorrectness types for functional programs
- 3:16Coverage types background
- 7:12Program traces for effects
- 11:48Transducers in type systems
- 15:17Summary and open questions
related talks
56mOn Type-Based Techniques for Program Manipulation
27mTowards Type Debugging using Partial Evaluation
30mA Complementary Approach to Incorrectness Typing
30mType-Checking Heterogeneous Sequences in a Simple Embeddable Type System
30mRecognizing regular patterns in mixed type sequences using Symbolic Finite Automata
46mThe Calculated Typer (Functional Pearl)
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
32mTyped Program Analysis Without Encodings