18 citations · 37 across the 8 of their papers we have counts for
13 papers
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…
DIRT: Database-Integrated Random Testing
Alperen Keles, Ethan Chou, Harrison Goldstein +1
Database management systems (DBMSs) are notoriously complex, making them difficult to test effectively, especially during early development when many features are incomplete. Tradi…
Etna: An evaluation platform for property-based testing
Alperen Keles, Jessica Shi, Nikhil Kamath +5
Property-based testing is a mainstay of functional programming, boasting a rich literature, an enthusiastic user community, and an abundance of tools~ -- so many, indeed, that new…
Programmable Property-Based Testing
Alperen Keles, Justine Frank, Ceren Mert +2
Property-based testing (PBT) is a popular technique for establishing confidence in software, where users write properties -- i.e., executable specifications -- that can be checked…
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…
Measuring Neural Net Robustness with Constraints
Osbert Bastani, Yani Ioannou, Leonidas Lampropoulos +3
Despite having high accuracy, neural nets have been shown to be susceptible to adversarial examples, where a small perturbation to an input can cause it to become mislabeled. We pr…
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…
Automatic WSDL-guided Test Case Generation for PropEr Testing of Web Services
Leonidas Lampropoulos, Konstantinos Sagonas
With web services already being key ingredients of modern web systems, automatic and easy-to-use but at the same time powerful and expressive testing frameworks for web services ar…