{/* Lab intro */}

The ROSE group is part of the{' '} Computer Science Department at{' '} Yale University. We use formal methods and automated reasoning (SAT/SMT, symbolic execution, theorem proving, and cryptography) to analyze systems of every kind, from software and networks to machine-learning and AI models, so that they can be shown to be correct, understood clearly, and held within trustworthy, private, and accountable bounds.

{/* Lab Vision */}

Lab Vision

ROSE builds the frameworks, languages, and tools needed to analyze systems: to guarantee they are correct, to understand and reason about them clearly, and to appropriately constrain how they behave. These systems are often software, but also include networks and AI models, and the analysis often has to preserve privacy along the way.

Two commitments run through everything we do: formal reasoning as the lens we bring to every problem, and privacy as a value the field too often overlooks. The interdisciplinary group works across Yale with colleagues in law, environmental policy, biomedical data science, and beyond.

{/* Research Themes */}

Research Themes

(p.themes || []).includes('privacy') && p.pdf && p.pdf !== '#').sort((a, b) => b.year - a.year).slice(0, 4).map(p => ({ title: p.title, url: p.pdf && p.pdf !== '#' ? p.pdf : '#' }))}> Formal reasoning normally requires seeing everything involved in the task: the program, the inputs, and the specification. Cryptography lets us drop that requirement, so that one party can prove a program satisfies a property while revealing nothing beyond the claim itself, or several parties can check whether their policies conflict and jointly search for a configuration satisfying all of them, without any one of them revealing the details it is trying to protect. The work spans zero-knowledge proof systems for automated reasoning (proving unsatisfiability, SMT theorems, and regular-expression equivalence in zero knowledge) and secure multi-party protocols where mutually distrusting parties jointly solve constraint problems over inputs neither will disclose. Recent directions include privacy-preserving SAT and MaxSAT solving, delegated computation on randomness, and protocols for verifying properties of proprietary AI models without exposing their weights. (p.themes || []).includes('mlai') && p.pdf && p.pdf !== '#').sort((a, b) => b.year - a.year).slice(0, 4).map(p => ({ title: p.title, url: p.pdf }))}> Machine learning and formal methods have complementary blind spots. Formal methods give guarantees but rely on search procedures whose guidance has been hand-tuned for decades: which variable a SAT solver should branch on, which candidate invariant to try next, how to decompose a proof obligation. Learning is good at exactly these decisions, since they are data-rich guesses with no clean theory behind them. Machine learning, in turn, produces artifacts that work well on average but come with no guarantees about any particular input, which is the gap formal reasoning is built to close. We build frameworks where each side supplies what the other lacks, i.e., learning does the guessing, formal reasoning does the checking. (p.themes || []).includes('neuro') && p.pdf && p.pdf !== '#').sort((a, b) => b.year - a.year).slice(0, 4).map(p => ({ title: p.title, url: p.pdf && p.pdf !== '#' ? p.pdf : '#' }))}> Some problems yield to neither pure learning nor pure symbolic reasoning. Neural methods handle perception, ambiguity, and open-ended search, while symbolic methods supply structure, soundness, and explanation. We combine them on problems where both are needed at once, e.g., agentic pipelines that propose environmental data proxies and then produce checkable arguments for why they hold, program synthesis and reachability analysis for models that biologists can trust mathematically, specification mining from execution data, and reasoning systems that carry this approach into law and policy. ((p.themes || []).includes('network') || (p.themes || []).includes('verification') || (p.themes || []).includes('synthesis')) && p.pdf && p.pdf !== '#').sort((a, b) => b.year - a.year).slice(0, 6).map(p => ({ title: p.title, url: p.pdf && p.pdf !== '#' ? p.pdf : '#' }))}> Verification asks whether a program meets its specification; synthesis asks the machine to produce a program that does. Both reduce to hard questions in logic and automated reasoning, and progress comes from better decision procedures, better proof techniques, and better ways of stating what correctness means. Work here includes relational and hyperproperty verification (proving things about pairs of executions rather than single runs), termination and non-termination proofs, separation logic for heap-manipulating programs, reactive and syntax-guided synthesis, program repair, and decision procedures for sets, multisets, and cardinality constraints. The same machinery applies well beyond conventional programs, to firewalls, routing policies, data-plane implementations, cloud service dependencies, and infrastructure-as-code, which are all software in the end, but written in idiosyncratic languages, rarely tested, and catastrophic when misconfigured. (p.themes || []).includes('law') && p.pdf && p.pdf !== '#').sort((a, b) => b.year - a.year).slice(0, 4).map(p => ({ title: p.title, url: p.pdf && p.pdf !== '#' ? p.pdf : '#' }))}> When software decides something consequential the legal system needs to interrogate that decision the way it interrogates a witness. That requires translating legal questions into formal ones. In collaboration with Yale Law School, we build SMT-based oracles that answer counterfactual questions about automated decisions in a form usable as evidence, autoformalization tools that turn statutory and contractual language into logical specifications, and benchmarks probing whether language models can produce the structured reasoning that legitimizes a ruling.

{/* Lab News */}

Lab News

Last updated {fmtNewsDate(newsItems.reduce((a, b) => (a.date > b.date ? a : b)).date)}

{newsItems.map((it, i) => (

{fmtNewsDate(it.date)}

{it.tag}

{it.title}

{it.body}

))}

{/* Collaborators */}

Collaborators & Partners

A defining feature of ROSE is how widely it reaches across Yale. The group partners with the Law School, environmental policy through the Yale Environmental Performance Index, Biomedical Informatics and Data Science (BIDS), and the School of Management, alongside longstanding external collaborators.

{[ ['Scott J. Shapiro', 'Yale Law School'], ['Hyunghoon Cho', 'Yale BIDS'], ['Zhong Shao', 'Yale CS'], ['Mariana Raykova', 'Google'], ['Xiao Wang', 'Northwestern'], ['Eran Tromer', 'Boston University'], ['Duc-Hiep Chu', 'Cogent Security'], ['Jakub Szefer', 'Northwestern (CASLAB)'], ['Bettina Könighofer', 'TU Graz'], ['Shafi Goldwasser', 'UC Berkeley / MIT'], ['Byron Cook', 'AWS Automated Reasoning'], ['Jinyang Li', 'New York University'], ['Zhaoguo Wang', 'Shanghai Jiao Tong University'], ['James Zheng', 'Macquarie University'], ['Dana Angluin', 'Yale CS'], ['Bernd Finkbeiner', 'CISPA & Saarland Universit'], ['Ranjit Jhala', 'UC San Diego'], ['Dan Esty', 'Yale EPI'], ['Zach Wendling', 'Yale EPI'], ['Kyle Jensen', 'Yale SOM'], ].sort((a, b) => a[0].split(' ').pop().localeCompare(b[0].split(' ').pop())).map(([name, inst]) => (

{name}

{inst}

))}

{/* Teaching */}

Teaching

{[ [['CPSC 4540 / 5540'], 'Software Analysis and Verification', 'Ruzica Piskac'], [['CPSC 4150 / 5150'], 'Law and Large Language Models', 'Ruzica Piskac & Scott Shapiro'], [['CPSC 4390 / 5390'], 'Software Engineering', 'Timos Antonopoulos'], [['CPSC 4391 / 5391', 'MGT 697'], 'Advanced Software Engineering', 'Timos Antonopoulos'], ].map(([nums, ctitle, who]) => (

{nums.map(n =>

{n}

)}

{ctitle}

{who}

))}

{/* Department line, relocated from sidebar */}

ROSE is a research group in the{' '} Department of Computer Science {' '}at{' '} Yale University.

Lab Vision

Research Themes

Lab News

Collaborators & Partners

Teaching

Publications

Publications

Team

Faculty

Current Lab Members

Alumni

Funding

Lab News