research
∙
01/24/2023
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
Hoare logics are proof systems that allow one to formally establish prop...
share
research
∙
12/08/2022
Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version)
We provide a framework consisting of tools and metatheorems for the end-...
research
∙
12/05/2022
A Generic Methodology for the Modular Verification of Security Protocol Implementations
Security protocols are essential building blocks of modern IT systems. S...
research
∙
11/15/2022
CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity
Information flow security ensures that the secret data manipulated by a ...
research
∙
10/18/2022
Compositional Reasoning for Side-effectful Iterators and Iterator Adapters
Iteration is a programming operation that traditionally refers to visiti...
research
∙
08/22/2022
Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version)
Bounded verification has proved useful to detect bugs and to increase co...
research
∙
05/26/2022
DT+GNN: A Fully Explainable Graph Neural Network using Decision Trees
We propose the fully explainable Decision Tree Graph Neural Network (DT+...
research
∙
05/23/2022
Sound Automation of Magic Wands (extended version)
The magic wand -* (also called separating implication) is a separation l...
research
∙
05/09/2022
A Comparative Tutorial of Bayesian Sequential Design and Reinforcement Learning
Reinforcement Learning (RL) is a computational approach to reward-driven...
research
∙
12/31/2021
Bayesian Nonparametric Common Atoms Regression for Generating Synthetic Controls in Clinical Trials
The availability of electronic health records (EHR) has opened opportuni...
research
∙
10/26/2021
Flexible Refinement Proofs in Separation Logic
Refinement transforms an abstract system model into a concrete, executab...
research
∙
08/19/2021
Bayesian Semiparametric Hidden Markov Tensor Partition Models for Longitudinal Data with Local Variable Selection
We present a flexible Bayesian semiparametric mixed model for longitudin...
research
∙
05/29/2021
Formally Validating a Practical Verification Condition Generator (extended version)
A program verifier produces reliable results only if both the logic used...
research
∙
05/28/2021
Gobra: Modular Specification and Verification of Go Programs (extended version)
Go is an increasingly-popular systems programming language targeting, es...
research
∙
05/10/2021
Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers
Universal quantifiers occur frequently in proof obligations produced by ...
research
∙
04/20/2021
Modular Verification of Collaborating Smart Contracts
Smart contracts are programs that execute inside blockchains such as Eth...
research
∙
10/14/2020
Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA (Full Paper)
Modern separation logics allow one to prove rich properties of intricate...
research
∙
10/09/2020
Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
Lighthouse projects such as CompCert, seL4, IronFleet, and DeepSpec have...
research
∙
09/14/2020
Bayesian Nonparametric Bivariate Survival Regression for Current Status Data
We consider nonparametric inference for event time distributions based o...
research
∙
08/31/2020
VerifyThis 2019: A Program Verification Competition (Extended Report)
VerifyThis is a series of program verification competitions that emphasi...
research
∙
10/27/2019
A Semi-parametric Bayesian Approach to Population Finding with Time-to-Event and Toxicity Data in a Randomized Clinical Trial
A utility-based Bayesian population finding (BaPoFi) method was proposed...
research
∙
08/16/2019
Modular Verification of Heap Reachability Properties in Separation Logic
The correctness of many algorithms and data structures depends on reacha...
research
∙
03/20/2019
A Bayesian Nonparametric Approach for Evaluating the Effect of Treatment in Randomized Trials with Semi-Competing Risks
We develop a Bayesian nonparametric (BNP) approach to evaluate the effec...
research
∙
07/20/2018
Specification Mining for Smart Contracts with Automatic Abstraction Tuning
Smart contracts are programs that manage digital assets according to a c...
research
∙
07/12/2018
Engineering Collaborative Social Science Toolkits. STS Methods and Concepts as Devices for Interdisciplinary Diplomacy
The smartification of industries is marked by the development of cyber-p...
research
∙
06/07/2018
Scalable Bayesian Nonparametric Clustering and Classification
We develop a scalable multi-step Monte Carlo algorithm for inference und...
research
∙
04/11/2018