11 citations · 21 across the 21 of their papers we have counts for
7 papers · 1 filter
Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification
Shuangjie Yao, Nikolaus Holzer, Mark Paul Santolucito +3
Program verification establishes software correctness through machine-checkable proofs constructed in theorem provers. It's a guarantee especially valuable for code generated by la…
Learning GR(1) Specifications from Traces
Sam Nicholas Kouteili, William Fishell, Mark Santolucito +1
Constrained specification mining enables the automatic discovery of desired properties from system traces. Generalized Reactivity of Rank 1, or GR(1), is a fragment of LTL with pol…
Experiential Learning of Runtime Monitoring Using Pachinko
Miles Scharff, Maria Chemodanova, Mark Santolucito
We present documentation of a classroom assignment that teaches runtime monitoring through a creative embedded systems build: an interactive Pachinko game. The assignment centers o…
Lattice Deduction Transformers
Liam Davis, Leopold Haller, Alberto Alfarano +1
We introduce the Lattice Deduction Transformer (LDT), a recurrent transformer that approximates logically sound deduction by projecting its latent state through a lattice between f…
BlindMarket: Enabling Verifiable, Confidential, and Traceable IP Core Distribution in Zero-Trust Settings
Zhaoxiang Liu, Samuel Judson, Raj Dutta +3
We present BlindMarket, an end-to-end zero-trust distribution framework for hardware IP cores. BlindMarket allows two parties, the IP user and the IP vendor, to complete an IP trad…
Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications
Sam Nicholas Kouteili, William Fishell, Christian Scaff +2
Mining specifications from execution traces presents an automated way of capturing characteristic system behaviors. However, existing approaches are largely restricted to Boolean a…
Warm Starting State-Space Models with Automata Learning
William Fishell, Sam Nicholas Kouteili, Mark Santolucito
We prove that Moore machines can be exactly realized as state-space models (SSMs), establishing a formal correspondence between symbolic automata and these continuous machine learn…