Home
News
People
Publications
Vacancies
Contact
Pulp Fictions
Light
Dark
Automatic
1
QuFEM: Fast and Accurate Quantum Readout Calibration Using the Finite Element Method
Quantum readout error turns out to be the most significant error source, which greatly affects the measurement fidelity. Matrix-based …
Siwei Tan
,
Hanyu Zhang
,
Jia Yu
,
Congliang Lang
,
Yongheng Shang
,
Xinkui Zhao
,
Mingshuai Chen
,
Yun Liang
,
Liqiang Lu
,
Jianwei Yin
Cite
PS3: Precise Patch Presence Test Based on Semantic Symbolic Signature
During software development, vulnerabilities have posed a significant threat to users. Applying patches is the most effective way to …
Qi Zhan
,
Xing Hu
,
Zhiyang Li
,
Xin Xia
,
David Lo
,
Shanping Li
Cite
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite …
Kevin Batz
,
Mingshuai Chen
,
Sebastian Junges
,
Benjamin Lucien Kaminski
,
Joost-Pieter Katoen
,
Christoph Matheja
PDF
Cite
DOI
Artifact Evaluated
Exact Probabilistic Inference Using Generating Functions
Probabilistic programs are typically normal-looking programs describing posterior probability distributions. They intrinsically code up …
Lutz Klinkenberg
,
Tobias Winkler
,
Mingshuai Chen
,
Joost-Pieter Katoen
PDF
Cite
Code
Does a Program Yield the Right Distribution?
We study discrete probabilistic programs with potentially unbounded looping behaviors over an infinite state space. We present, to the …
Mingshuai Chen
,
Joost-Pieter Katoen
,
Lutz Klinkenberg
,
Tobias Winkler
PDF
Cite
DOI
Artifact Evaluated
Latticed $k$-Induction with an Application to Probabilistic Programs
We revisit two well-established verification techniques,
$k$-induction
and
bounded model checking
(BMC), in the more general setting of …
Kevin Batz
,
Mingshuai Chen
,
Benjamin Lucien Kaminski
,
Joost-Pieter Katoen
,
Christoph Matheja
,
Philipp Schröer
PDF
Cite
Slides
DOI
Artifact Evaluated
Pulp Fiction
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence …
Qiuye Wang
,
Mingshuai Chen
,
Bai Xue
,
Naijun Zhan
,
Joost-Pieter Katoen
PDF
Cite
Slides
Video
DOI
Artifact Evaluated
Unbounded-Time Safety Verification of Stochastic Differential Dynamics
In this paper, we propose a method for bounding the probability that a stochastic differential equation (SDE) system violates a safety …
Shenghua Feng
,
Mingshuai Chen
,
Bai Xue
,
Sriram Sankaranarayanan
,
Naijun Zhan
PDF
Cite
Slides
Video
DOI
Artifact Evaluated
Pulp Fiction
Learning One-Clock Timed Automata
We present an algorithm for active learning of deterministic timed automata with a single clock. The algorithm is within the framework …
Jie An
,
Mingshuai Chen
,
Bohua Zhan
,
Naijun Zhan
,
Miaomiao Zhang
PDF
Cite
Slides
DOI
Artifact Evaluated
Best Paper Award @ FMAC 2019
Springer High-Impact Paper
NIL: Learning Nonlinear Interpolants
Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model …
Mingshuai Chen
,
Jian Wang
,
Jie An
,
Bohua Zhan
,
Deepak Kapur
,
Naijun Zhan
PDF
Cite
Code
Slides
DOI
»
Cite
×