11 citations · 21 across the 21 of their papers we have counts for
23 papers
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…
TempoBench: Reasoning Execution Without Causal Attribution Is Just Simulation
Nikolaus Holzer, William Fishell, Baishakhi Ray +1
Current training paradigms, optimized for long-horizon reasoning trace execution, have made Large Language Models (LLMs) excel at pattern matching and forward simulation of reasoni…
Embedding Alignment in Code Generation for Audio
Sam Kouteili, Hiren Madhu, George Typaldos +1
LLM-powered code generation has the potential to revolutionize creative coding endeavors, such as live-coding, by enabling users to focus on structural motifs over syntactic detail…
Research Vision: Multi-Agent Path Planning for Cops And Robbers Via Reactive Synthesis
William Fishell, Andoni Rodriguez, Mark Santolucito
We propose the problem of multi-agent path planning for a generalization of the classic Cops and Robbers game via reactive synthesis. Specifically, through the application of LTLt…
Using a Feedback Loop for LLM-based Infrastructure as Code Generation
Mayur Amarnath Palavalli, Mark Santolucito
Code generation with Large Language Models (LLMs) has helped to increase software developer productivity in coding tasks, but has yet to have significant impact on the tasks of sof…
Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis
William Murphy, Nikolaus Holzer, Feitong Qiao +4
In the past few years, Large Language Models (LLMs) have exploded in usefulness and popularity for code generation tasks. However, LLMs still struggle with accuracy and are unsuita…
Benchmarking LLM Code Generation for Audio Programming with Visual Dataflow Languages
William Zhang, Maria Leon, Ryan Xu +10
Node-based programming languages are increasingly popular in media arts coding domains. These languages are designed to be accessible to users with limited coding experience, allow…
Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control
William Murphy, Nikolaus Holzer, Nathan Koenig +4
Temporal logics are powerful tools that are widely used for the synthesis and verification of reactive systems. The recent progress on Large Language Models (LLMs) has the potentia…
Statically Inferring Usage Bounds for Infrastructure as Code
Feitong Qiao, Aryana Mohammadi, Jürgen Cito +1
Infrastructure as Code (IaC) has enabled cloud customers to have more agility in creating and modifying complex deployments of cloud-provisioned resources. By writing a configurati…
Procedural Adherence and Interpretability Through Neuro-Symbolic Generative Agents
Raven Rothkopf, Hannah Tongxin Zeng, Mark Santolucito
The surge in popularity of large language models (LLMs) has opened doors for new approaches to the creation of interactive agents. However, managing and interpreting the temporal b…
Programming-By-Example by Programming-By-Example: Synthesis of Looping Programs
Shmuel Berman, Mark Santolucito
Program synthesis has seen many new applications in recent years, in large part thanks to the introduction of SyGuS. However, no existing SyGuS solvers have support for synthesizin…
Succinct Explanations With Cascading Decision Trees
Jialu Zhang, Yitan Wang, Mark Santolucito +1
The decision tree is one of the most popular and classical machine learning models from the 1980s. However, in many practical applications, decision trees tend to generate decision…
Grammar Filtering For Syntax-Guided Synthesis
Kairo Morton, William Hallahan, Elven Shum +2
Programming-by-example (PBE) is a synthesis paradigm that allows users to generate functions by simply providing input-output examples. While a promising interaction paradigm, synt…
Synthesizing Functional Reactive Programs
Bernd Finkbeiner, Felix Klein, Ruzica Piskac +1
Functional Reactive Programming (FRP) is a paradigm that has simplified the construction of reactive programs. There are many libraries that implement incarnations of FRP, using ab…
Statically Verifying Continuous Integration Configurations
Mark Santolucito, Jialu Zhang, Ennan Zhai +1
Continuous Integration (CI) testing is a popular software development technique that allows developers to easily check that their code can build successfully and pass tests across…
Vehicle Platooning Simulations with Functional Reactive Programming
Bernd Finkbeiner, Felix Klein, Ruzica Piskac +1
Functional languages have provided major benefits to the verification community. Although features such as purity, a strong type system, and computational abstractions can help gui…
Temporal Stream Logic: Synthesis beyond the Bools
Bernd Finkbeiner, Felix Klein, Ruzica Piskac +1
Reactive systems that operate in environments with complex data, such as mobile apps or embedded controllers with many sensors, are difficult to synthesize. Synthesis tools usually…