Zobrazeno 1 - 10
of 187
pro vyhledávání: '"Clarke, Edmund M."'
Autor:
Wang, Qinsi, Miskov-Zivanov, Natasa, Liu, Bing, Faeder, James R., Lotze, Michael, Clarke, Edmund M.
The focus of pancreatic cancer research has been shifted from pancreatic cancer cells towards their microenvironment, involving pancreatic stellate cells that interact with cancer cells and influence tumor progression. To quantitatively understand th
Externí odkaz:
http://arxiv.org/abs/1606.03138
Autor:
Černý, Pavol, Clarke, Edmund M., Henzinger, Thomas A., Radhakrishna, Arjun, Ryzhyk, Leonid, Samanta, Roopsha, Tarrach, Thorsten
Given a multithreaded program written assuming a friendly, non-preemptive scheduler, the goal of synchronization synthesis is to automatically insert synchronization primitives to ensure that the modified program behaves correctly, even with a preemp
Externí odkaz:
http://arxiv.org/abs/1511.07163
Autor:
Černý, Pavol, Clarke, Edmund M., Henzinger, Thomas A., Radhakrishna, Arjun, Ryzhyk, Leonid, Samanta, Roopsha, Tarrach, Thorsten
We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even
Externí odkaz:
http://arxiv.org/abs/1505.04533
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 computational framework for identifying patient-specific androgen ablation the
Externí odkaz:
http://arxiv.org/abs/1410.7346
A central problem in systems biology is to identify parameter values such that a biological model satisfies some behavioral constraints (\eg, time series). In this paper we focus on parameter synthesis for hybrid (continuous/discrete) models, as many
Externí odkaz:
http://arxiv.org/abs/1407.1524
In this paper we describe a new tool, SReach, which solves probabilistic bounded reachability problems for two classes of stochastic hybrid systems. The first one is (nonlinear) hybrid automata with parametric uncertainty. The second one is probabili
Externí odkaz:
http://arxiv.org/abs/1404.7206
Software model checkers based on under-approximations and SMT solvers are very successful at verifying safety (i.e. reachability) properties. They combine two key ideas -- (a) "concreteness": a counterexample in an under-approximation is a counterexa
Externí odkaz:
http://arxiv.org/abs/1306.1945
Publikováno v:
LICS, pp. 441-450, IEEE, 2012
We consider the problem of learning a non-deterministic probabilistic system consistent with a given finite set of positive and negative tree samples. Consistency is defined with respect to strong simulation conformance. We propose learning algorithm
Externí odkaz:
http://arxiv.org/abs/1207.5091
Publikováno v:
CAV, vol. 7358 of LNCS, pp. 310-326. Springer-Verlag. 2012
We describe an automated technique for assume-guarantee style checking of strong simulation between a system and a specification, both expressed as non-deterministic Labeled Probabilistic Transition Systems (LPTSes). We first characterize counterexam
Externí odkaz:
http://arxiv.org/abs/1207.5086