activity
20142024
most citedCerberus: A Formal Approach to Secure and Efficient Enclave Memory Sharing

13 citations · 39 across the 14 of their papers we have counts for

collaborators
Showing cs.LOShow all

5 papers · 1 filter

cs.LO2023

An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes

Amar Shah, Federico Mora, Sanjit A. Seshia

Algebraic data types (ADTs) are a construct classically found in functional programming languages that capture data structures like enumerated types, lists, and trees. In recent ye…

cs.LO20222 cited

Automated Conversion of Axiomatic to Operational Models: Theory and Practice

Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia

A system may be modelled as an operational model (which has explicit notions of state and transitions between states) or an axiomatic model (which is specified entirely as a set of…

cs.LO2022

UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis

Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu +6

UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combi…

cs.LO201411 cited

Are There Good Mistakes? A Theoretical Analysis of CEGIS

Susmit Jha, Sanjit A. Seshia

Counterexample-guided inductive synthesis CEGIS is used to synthesize programs from a candidate space of programs. The technique is guaranteed to terminate and synthesize the corre…

cs.LO20142 cited

Speeding Up SMT-Based Quantitative Program Analysis

Daniel J. Fremont, Sanjit A. Seshia

Quantitative program analysis involves computing numerical quantities about individual or collections of program executions. An example of such a computation is quantitative inform…