16 citations · 35 across the 15 of their papers we have counts for
3 papers · 1 filter
The Lattice-Theoretic Essence of Property Directed Reachability Analysis
Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata +2
We present LT-PDR, a lattice-theoretic generalization of Bradley's property directed reachability analysis (PDR) algorithm. LT-PDR identifies the essence of PDR to be an ingenious…
Efficient Black-Box Checking via Model Checking with Strengthened Specifications
Junya Shijubo, Masaki Waga, Kohei Suenaga
Black-box checking (BBC)} is a testing method for cyber-physical systems (CPSs) as well as software systems. BBC consists of active automata learning and model checking; a Mealy ma…
Sharper and Simpler Nonlinear Interpolants for Program Verification
Takamasa Okudono, Yuki Nishida, Kensuke Kojima +3
Interpolation of jointly infeasible predicates plays important roles in various program verification techniques such as invariant synthesis and CEGAR. Intrigued by the recent resul…