4 papers
Tracers for debugging and program exploration
Shardul Chiplunkar, Clément Pit-Claudel
Programmers often use an iterative process of hypothesis generation ("perhaps this function is called twice?") and hypothesis testing ("let's count how many times this breakpoint f…
Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)
Aurèle Barrière, Victor Deng, Clément Pit-Claudel
We present the first mechanized, succinct, practical, complete, and proven-faithful semantics for a modern regular expression language with backtracking semantics. We ensure its fa…
Precise Reasoning About Container-Internal Pointers with Logical Pinning
Yawen Guan, Clément Pit-Claudel
Most separation logics hide container-internal pointers for modularity. This makes it difficult to specify container APIs that temporarily expose those pointers to the outside, and…
Automatic layout of railroad diagrams
Shardul Chiplunkar, Clément Pit-Claudel
Railroad diagrams (also called "syntax diagrams") are a common, intuitive visualization of grammars, but limited tooling and a lack of formal attention to their layout mostly confi…