33 citations · 103 across the 24 of their papers we have counts for
14 papers · 1 filter
Trapezoidal Generalization over Linear Constraints
David Greve, Andrew Gacek
We are developing a model-based fuzzing framework that employs mathematical models of system behavior to guide the fuzzing process. Whereas traditional fuzzing frameworks generate…
The JKind Model Checker
Andrew Gacek, John Backes, Mike Whalen +2
JKind is an open-source industrial model checker developed by Rockwell Collins and the University of Minnesota. JKind uses multiple parallel engines to prove or falsify safety prop…
Reasoning about Algebraic Data Types with Abstractions
Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen
Reasoning about functions that operate over algebraic data types is an important problem for a large variety of applications. One application of particular interest is network appl…
Reasoning About Higher-Order Relational Specifications
Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek +1
The logic of hereditary Harrop formulas (HH) has proven useful for specifying a wide range of formal systems. This logic includes a form of hypothetical judgment that leads to dyna…
Relating Nominal and Higher-order Abstract Syntax Specifications
Andrew Gacek
Nominal abstract syntax and higher-order abstract syntax provide a means for describing binding structure which is higher-level than traditional techniques. These approaches have s…
A two-level logic approach to reasoning about computations
Andrew Gacek, Dale Miller, Gopalan Nadathur
Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, typing, and acceptance by non-deterministic mach…