3 citations · 12 across the 10 of their papers we have counts for
10 papers
Synthesizing Probabilistic Saturating Counters with Differentially Private Formal Guarantees
Zhiming Chi, Lutan Zhao, Depeng Liu +8
Branch predictors improve instruction-level parallelism in modern processors and are commonly modeled using saturating counters. However, classical saturating counters are determin…
Defensive Design of Saturating Counters Based on Differential Privacy
Depeng Liu, Lutan Zhao, Pengfei Yang +4
The saturating counter is the basic module of the dynamic branch predictor, which involves the core technique to improve instruction level parallelism performance in modern process…
Analyzing FreeRTOS Scheduling Behaviors with the Spin Model Checker
Chen-Kai Lin, Bow-Yaw Wang
FreeRTOS is a real-time operating system with configurable scheduling policies. Its portability and configurability make FreeRTOS one of the most popular real-time operating system…
Verifying Pufferfish Privacy in Hidden Markov Models
Depeng Liu, Bow-yaw Wang, Lijun Zhang
Pufferfish is a Bayesian privacy framework for designing and analyzing privacy mechanisms. It refines differential privacy, the current gold standard in data privacy, by allowing e…
A Spin-based model checking for the simple concurrent program on a preemptive RTOS
Chen-Kai Lin, Ching-Chun, Huang +1
We adapt an existing preemptive scheduling model of RTOS kernel by eChronos from machine-assisted proof to Spin-based model checker. The model we constructed can be automatically v…
An Executable Sequential Specification for Spark Aggregation
Yu-Fang Chen, Chih-Duo Hong, Ondřej Lengál +3
Spark is a new promising platform for scalable data-parallel computation. It provides several high-level application programming interfaces (APIs) to perform parallel data aggregat…
PAC Learning-Based Verification and Model Synthesis
Yu-Fang Chen, Chiao Hsieh, Ondřej Lengál +4
We introduce a novel technique for verification and model synthesis of sequential programs. Our technique is based on learning a regular model of the set of feasible paths in a pro…
Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation
Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang +1
We apply multivariate Lagrange interpolation to synthesize polynomial quantitative loop invariants for probabilistic programs. We reduce the computation of an quantitative loop inv…
A Finite Exact Representation of Register Automata Configurations
Yu-Fang Chen, Bow-Yaw Wang, Di-De Yen
A register automaton is a finite automaton with finitely many registers ranging from an infinite alphabet. Since the valuations of registers are infinite, there are infinitely many…
Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
Wonchan Lee, Yungbum Jung, Bow-yaw Wang +1
We address the predicate generation problem in the context of loop invariant inference. Motivated by the interpolation-based abstraction refinement technique, we apply the interpol…