18 citations · 37 across the 8 of their papers we have counts for
8 papers · 1 filter
QuickerChick
Ivan Mladenov, Alperen Keles, Leonidas Lampropoulos
Property-based testing (PBT) with QuickChick relies on extracting Rocq programs to OCaml. However, this extraction mechanism, while crucial for QuickChick to function, has signific…
Evaluating Shrinking (Experience Report)
Alperen Keles, George Miao, Leonidas Lampropoulos
Property-based testing frameworks rely on shrinking to turn noisy random failures into counterexamples that developers can debug. Although bug-finding performance is routinely meas…
The Search for Constrained Random Generators
Harrison Goldstein, Hila Peleg, Cassia Torczon +3
Among the biggest challenges in property-based testing (PBT) is the constrained random generation problem: given a predicate on program values, randomly sample from the set of all…
Pantograph: A Fluid and Typed Structure Editor
Jacob Prinz, Henry Blanchette, Leonidas Lampropoulos
Structure editors operate directly on a program's syntactic tree structure. At first glance, this allows for the exciting possibility that such an editor could enforce correctness…
A Formal Model of Checked C
Liyi Li, Yiyun Liu, Deena L. Postol +3
We present a formal model of Checked C, a dialect of C that aims to enforce spatial memory safety. Our model pays particular attention to the semantics of dynamically sized, potent…
Formalizing Stack Safety as a Security Property
Sean Noble Anderson, Roberto Blanco, Leonidas Lampropoulos +2
The term stack safety is used to describe a variety of compiler, run-time, and hardware mechanisms for protecting stack memory. Unlike "the heap," the ISA-level stack does not corr…
Beginner's Luck: A Language for Property-Based Generators
Leonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu +3
Property-based random testing a la QuickCheck requires building efficient generators for well-distributed random data satisfying complex logical predicates, but writing these gener…
Testing Noninterference, Quickly
Catalin Hritcu, Leonidas Lampropoulos, Antal Spector-Zabusky +5
Information-flow control mechanisms are difficult both to design and to prove correct. To reduce the time wasted on doomed proof attempts due to broken definitions, we advocate mod…