research
∙
09/09/2023
Leaf: Modularity for Temporary Sharing in Separation Logic (Extended Version)
In concurrent verification, separation logic provides a strong story for...
share
research
∙
07/17/2023
Quarl: A Learning-Based Quantum Circuit Optimizer
Optimizing quantum circuits is challenging due to the very large search ...
research
∙
04/19/2022
Quartz: Superoptimization of Quantum Circuits (Extended Version)
Existing quantum compilers optimize quantum circuits by applying circuit...
research
∙
12/10/2021
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
We present a PDR/IC3 algorithm for finding inductive invariants with qua...
research
∙
11/22/2021
Quanto: Optimizing Quantum Circuits with Automatic Generation of Circuit Identities
Existing quantum compilers focus on mapping a logical quantum circuit to...
research
∙
06/02/2021
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Various verification techniques for temporal properties transform tempor...
research
∙
01/18/2021
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
We develop a framework for model checking infinite-state systems by auto...
research
∙
09/06/2020
A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs
Data race free (DRF) programs constitute an important class of concurren...
research
∙
04/10/2020
Resources: A Safe Language Abstraction for Money
Smart contracts are programs that implement potentially sophisticated tr...
research
∙
06/12/2019
SPoC: Search-based Pseudocode to Code
We consider the task of mapping pseudocode to long programs that are fun...
research
∙
05/19/2019
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics
Verification of fault-tolerant distributed protocols is an immensely dif...
research
∙
10/24/2017
Bounded Quantifier Instantiation for Checking Inductive Invariants
We consider the problem of checking whether a proposed invariant ϕ expre...
research
∙
10/19/2017