150 citations · 341 across the 17 of their papers we have counts for
17 papers
Solving QBF with Counterexample Guided Refinement
Mikoláš Janota, William Klieber, Joao Marques-Silva +1
We propose two novel approaches for using Counterexample-Guided Abstraction Refinement (CEGAR) in Quantified Boolean Formula (QBF) solvers. The first approach develops a recursive…
Formal Modeling and Analysis of Pancreatic Cancer Microenvironment
Qinsi Wang, Natasa Miskov-Zivanov, Bing Liu +3
The focus of pancreatic cancer research has been shifted from pancreatic cancer cells towards their microenvironment, involving pancreatic stellate cells that interact with cancer…
Optimizing Solution Quality in Synchronization Synthesis
Pavol Černý, Edmund M. Clarke, Thomas A. Henzinger +4
Given a multithreaded program written assuming a friendly, non-preemptive scheduler, the goal of synchronization synthesis is to automatically insert synchronization primitives to…
From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis
Pavol Černý, Edmund M. Clarke, Thomas A. Henzinger +4
We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedu…
Towards Personalized Prostate Cancer Therapy Using Delta-Reachability Analysis
Bing Liu, Soonho Kong, Sicun Gao +2
Recent clinical studies suggest that the efficacy of hormone therapy for prostate cancer depends on the characteristics of individual patients. In this paper, we develop a computat…
Proof Generation from Delta-Decisions
Sicun Gao, Soonho Kong, Edmund Clarke
We show how to generate and validate logical proofs of unsatisfiability from delta-complete decision procedures that rely on error-prone numerical algorithms. Solving this problem…