Edmund M. Clarke

Publication Activity (10 Years)

Years Active: 1977-2017
Publications (10 Years): 16

Top Venues

CoRR

CMSB

HLDVT

HSCC

Publications

Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach
From non-preemptive to preemptive scheduling using synchronization synthesis. Formal Methods Syst. Des. 50 (2-3) (2017)
Md. Ariful Islam, Greg Byrne, Soonho Kong, Edmund M. Clarke, Rance Cleaveland, Flavio H. Fenton, Radu Grosu, Paul L. Jones, Scott A. Smolka
Bifurcation Analysis of Cardiac Alternans Using \delta -Decidability. CMSB (2016)
Qinsi Wang, Natasa Miskov-Zivanov, Bing Liu, James R. Faeder, Michael Lotze, Edmund M. Clarke
Formal Modeling and Analysis of Pancreatic Cancer Microenvironment. CMSB (2016)
Natasa Miskov-Zivanov, Paolo Zuliani, Qinsi Wang, Edmund M. Clarke, James R. Faeder
High-level modeling and verification of cellular signaling. HLDVT (2016)
Kyungmin Bae, Peter Csaba Ölveczky, Soonho Kong, Sicun Gao, Edmund M. Clarke
SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems. HSCC (2016)
Qinsi Wang, Edmund M. Clarke
Formal modeling of biological systems. HLDVT (2016)
Md. Ariful Islam, Qinsi Wang, Ramin M. Hasani, Ondrej Balun, Edmund M. Clarke, Radu Grosu, Scott A. Smolka
Probabilistic reachability analysis of the tap withdrawal circuit in caenorhabditis elegans. HLDVT (2016)
Mikolás Janota, William Klieber, João Marques-Silva, Edmund M. Clarke
Solving QBF with counterexample guided refinement. Artif. Intell. 234 (2016)
Md. Ariful Islam, Hyun-Kyung Lim, Nicola Paoletti, Houssam Abbas, Zhihao Jiang, Jacek Cyranka, Rance Cleaveland, Sicun Gao, Edmund M. Clarke, Radu Grosu, Rahul Mangharam, Elizabeth Cherry, Flavio H. Fenton, Richard A. Gray, James Glimm, Shan Lin, Qinsi Wang, Scott A. Smolka
CyberCardia project: Modeling, verification and validation of implantable cardiac devices. BIBM (2016)
Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach
From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis. CoRR (2015)
Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, Edmund M. Clarke
Towards personalized prostate cancer therapy using delta-reachability analysis. HSCC (2015)
Qinsi Wang, Natasa Miskov-Zivanov, Cheryl Telmer, Edmund M. Clarke
Formal Analysis Provides Parameters for Guiding Hyperoxidation in Bacteria using Phototoxic Proteins. ACM Great Lakes Symposium on VLSI (2015)
Qinsi Wang, Paolo Zuliani, Soonho Kong, Sicun Gao, Edmund M. Clarke
SReach: A Probabilistic Bounded Delta-Reachability Analyzer for Stochastic Hybrid Systems. CMSB (2015)
Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach
Optimizing Solution Quality in Synchronization Synthesis. CoRR (2015)
Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach
From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis. CAV (2) (2015)
Soonho Kong, Sicun Gao, Wei Chen, Edmund M. Clarke
dReach: δ-Reachability Analysis for Hybrid Systems. TACAS (2015)
Edmund M. Clarke, Sicun Gao
Model Checking Hybrid Systems - (Invited Talk). ISoLA (2) (2014)
Sicun Gao, Soonho Kong, Wei Chen, Edmund M. Clarke
Delta-Complete Analysis for Bounded Reachability of Hybrid Systems. CoRR (2014)
Sicun Gao, Soonho Kong, Edmund M. Clarke
Revisiting the Complexity of Stability of Continuous and Hybrid Systems. CoRR (2014)
Qinsi Wang, Paolo Zuliani, Soonho Kong, Sicun Gao, Edmund M. Clarke
SReach: Combining Statistical Tests and Bounded Model Checking for Nonlinear Hybrid Systems with Parametric Uncertainty. CoRR (2014)
Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, Edmund M. Clarke
Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions. CoRR (2014)
Radu Grosu, Elizabeth Cherry, Edmund M. Clarke, Rance Cleaveland, Sanjay Dixit, Flavio H. Fenton, Sicun Gao, James Glimm, Richard A. Gray, Rahul Mangharam, Arnab Ray, Scott A. Smolka
Compositional, Approximate, and Quantitative Reasoning for Medical Cyber-Physical Systems with Application to Patient-Specific Cardiac Dynamics and Devices. ISoLA (2) (2014)
Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, Edmund M. Clarke
Parameter Synthesis for Cardiac Cell Hybrid Models Using δ-Decisions. CMSB (2014)
Sicun Gao, Soonho Kong, Edmund M. Clarke
Proof Generation from Delta-Decisions. SYNASC (2014)
Edmund M. Clarke, Qinsi Wang
Years of Model Checking. Ershov Memorial Conference (2014)
Haijun Gong, Tong Tong Wu, Edmund M. Clarke
Pathway-gene identification for pancreatic cancer survival via doubly regularized Cox regression. BMC Syst. Biol. 8 (S-1) (2014)
Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, Edmund M. Clarke
Towards Personalized Cancer Therapy Using Delta-Reachability Analysis. CoRR (2014)
Sicun Gao, Soonho Kong, Edmund M. Clarke
Proof Generation from Delta-Decisions. CoRR (2014)
Edmund M. Clarke
Turing's Computable Real Numbers and Why They Are Still Important Today. SAT (2013)
Sicun Gao, Soonho Kong, Edmund M. Clarke
dReal: An SMT Solver for Nonlinear Theories over the Reals. CADE (2013)
Sicun Gao, Soonho Kong, Edmund M. Clarke
Satisfiability modulo ODEs. FMCAD (2013)
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke
Automatic Abstraction in SMT-Based Unbounded Software Model Checking. CoRR (2013)
Sicun Gao, Soonho Kong, Edmund M. Clarke
Satisfiability Modulo ODEs. CoRR (2013)
Natasa Miskov-Zivanov, Paolo Zuliani, Edmund M. Clarke, James R. Faeder
Studies of biological networks with statistical model checking: application to immune system cells. BCB (2013)
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke
Automatic Abstraction in SMT-Based Unbounded Software Model Checking. CAV (2013)
William Klieber, Mikolás Janota, João Marques-Silva, Edmund M. Clarke
Solving QBF with Free Variables. CP (2013)
Samir Sapra, Marius Minea, Sagar Chaki, Arie Gurfinkel, Edmund M. Clarke
Finding Errors in Python Programs Using Dynamic Symbolic Execution. ICTSS (2013)
Paolo Zuliani, André Platzer, Edmund M. Clarke
Bayesian statistical model checking with application to Stateflow/Simulink verification. Formal Methods Syst. Des. 43 (2) (2013)
Sicun Gao, Jeremy Avigad, Edmund M. Clarke
Delta-Decidability over the Reals CoRR (2012)
Edmund M. Clarke
Computable Real Numbers and Why They Are Still Important Today. ACM-TURING (2012)
Qiusong Yang, Edmund M. Clarke, Anvesh Komuravelli, Mingshu Li
Assumption Generation for Asynchronous Systems by Abstraction Refinement. FACS (2012)
David Henriques, João G. Martins, Paolo Zuliani, André Platzer, Edmund M. Clarke
Statistical Model Checking for Markov Decision Processes. QEST (2012)
Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke
Learning Probabilistic Systems from Tree Samples CoRR (2012)
Sicun Gao, Jeremy Avigad, Edmund M. Clarke
Delta-Complete Decision Procedures for Satisfiability over the Reals CoRR (2012)
Paolo Zuliani, Christel Baier, Edmund M. Clarke
Rare-event verification for stochastic hybrid systems. HSCC (2012)
Mikolás Janota, William Klieber, João Marques-Silva, Edmund M. Clarke
Solving QBF with Counterexample Guided Refinement. SAT (2012)
Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke
Assume-Guarantee Abstraction Refinement for Probabilistic Systems. CAV (2012)
Sicun Gao, Jeremy Avigad, Edmund M. Clarke
Delta-Decidability over the Reals. LICS (2012)
Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke
Learning Probabilistic Systems from Tree Samples. LICS (2012)
Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke
Assume-Guarantee Abstraction Refinement for Probabilistic Systems CoRR (2012)
Sicun Gao, Jeremy Avigad, Edmund M. Clarke
δ-Complete Decision Procedures for Satisfiability over the Reals. IJCAR (2012)
Sicun Gao, André Platzer, Edmund M. Clarke
Quantifier Elimination over Finite Fields Using Gröbner Bases CoRR (2011)
Sicun Gao, André Platzer, Edmund M. Clarke
Quantifier Elimination over Finite Fields Using Gröbner Bases. CAI (2011)
Ying-Chih Wang, Anvesh Komuravelli, Paolo Zuliani, Edmund M. Clarke
Analog circuit verification by statistical model checking. ASP-DAC (2011)
Edmund M. Clarke, Paolo Zuliani
Statistical Model Checking for Cyber-Physical Systems. ATVA (2011)
Edmund M. Clarke, William Klieber, Milos Novácek, Paolo Zuliani
Model Checking and the State Explosion Problem. LASER Summer School (2011)
Haijun Gong, Paolo Zuliani, Qinsi Wang, Edmund M. Clarke
Formal analysis for logical models of pancreatic cancer. CDC/ECC (2011)
Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang
Automated Assume-Guarantee Reasoning through Implicit Learning. CAV (2010)
Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, Lei Zhu
Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. ISoLA (1) (2010)
Håkan L. S. Younes, Edmund M. Clarke, Paolo Zuliani
Statistical Verification of Probabilistic Properties with Unbounded Until. SBMF (2010)
William Klieber, Samir Sapra, Sicun Gao, Edmund M. Clarke
A Non-prenex, Non-clausal QBF Solver with Game-State Learning. SAT (2010)
Sicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, Edmund M. Clarke
Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. FMCAD (2010)
Haijun Gong, Paolo Zuliani, Anvesh Komuravelli, James R. Faeder, Edmund M. Clarke
Analysis and verification of the HMGB1 signaling pathway. BMC Bioinform. 11 (S-7) (2010)
Edmund M. Clarke, Robert P. Kurshan, Helmut Veith
The Localization Reduction and Counterexample-Guided Abstraction Refinement. Essays in Memory of Amir Pnueli (2010)
Haijun Gong, Paolo Zuliani, Anvesh Komuravelli, James R. Faeder, Edmund M. Clarke
Computational Modeling and Verification of Signaling Pathways in Cancer. ANB (2010)
Edmund M. Clarke, Alexandre Donzé, Axel Legay
On simulation-based probabilistic model checking of mixed-analog circuits. Formal Methods Syst. Des. 36 (2) (2010)
Paolo Zuliani, André Platzer, Edmund M. Clarke
Bayesian statistical model checking with application to Simulink/Stateflow verification. HSCC (2010)
Himanshu Jain, Edmund M. Clarke, Orna Grumberg
Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations. Formal Methods Syst. Des. 35 (1) (2009)
Himanshu Jain, Edmund M. Clarke
Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts. DAC (2009)
Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang
Learning Minimal Separating DFA's for Compositional Verification. TACAS (2009)
Sumit Kumar Jha, Edmund M. Clarke, Christopher James Langmead, Axel Legay, André Platzer, Paolo Zuliani
A Bayesian Approach to Model Checking Biological Systems. CMSB (2009)
Edmund M. Clarke
My 27-year Quest to Overcome the State Explosion Problem. LICS (2009)
Edmund M. Clarke, E. Allen Emerson, Joseph Sifakis
Model checking: algorithmic verification and debugging. Commun. ACM 52 (11) (2009)
Edmund M. Clarke
Model Checking - My 27-year Quest to Overcome the State Explosion Problem. NASA Formal Methods (2009)
Anmol Mathur, Masahiro Fujita, Edmund M. Clarke, Pascal Urard
Functional Equivalence Verification Tools in High-Level Synthesis Flows. IEEE Des. Test Comput. 26 (4) (2009)
André Platzer, Edmund M. Clarke
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. FM (2009)
André Platzer, Edmund M. Clarke
Computing differential invariants of hybrid systems as fixedpoints. Formal Methods Syst. Des. 35 (1) (2009)
Edmund M. Clarke, Muralidhar Talupur, Helmut Veith
Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. TACAS (2008)
Edmund M. Clarke, Alexandre Donzé, Axel Legay
Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Delta-Sigma Modulator. Haifa Verification Conference (2008)
Edmund M. Clarke
Model Checking - My 27-Year Quest to Overcome the State Explosion Problem. LPAR (2008)
André Platzer, Edmund M. Clarke
Computing Differential Invariants of Hybrid Systems as Fixedpoints. CAV (2008)
Edmund M. Clarke, James R. Faeder, Christopher James Langmead, Leonard A. Harris, Sumit Kumar Jha, Axel Legay
Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway. CMSB (2008)
Sagar Chaki, Edmund M. Clarke, Natasha Sharygina, Nishant Sinha
Verification of evolving software via component substitutability analysis. Formal Methods Syst. Des. 32 (3) (2008)
Flavio Lerda, James Kapinski, Edmund M. Clarke, Bruce H. Krogh
Verification of Supervisory Control Software Using State Proximity and Merging. HSCC (2008)
Azadeh Farzan, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang
Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. TACAS (2008)
Edmund M. Clarke
The Birth of Model Checking. 25 Years of Model Checking (2008)
Himanshu Jain, Edmund M. Clarke, Orna Grumberg
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. CAV (2008)
Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27 (2) (2008)
Flavio Lerda, James Kapinski, Hitashyam Maka, Edmund M. Clarke, Bruce H. Krogh
Model checking in-the-loop: Finding counterexamples by systematic simulation. ACC (2008)
Edmund M. Clarke, E. Allen Emerson
Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. 25 Years of Model Checking (2008)
Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook
Arithmetic Strengthening for Shape Analysis. SAS (2007)
André Platzer, Edmund M. Clarke
The Image Computation Problem in Hybrid Systems Model Checking. HSCC (2007)
Edmund M. Clarke, Flavio Lerda
Model Checking: Software and Beyond. J. Univers. Comput. Sci. 13 (5) (2007)
Nishant Sinha, Edmund M. Clarke
SAT-Based Compositional Verification Using Lazy Learning. CAV (2007)
Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
VCEGAR: Verilog CounterExample Guided Abstraction Refinement. TACAS (2007)
Sumit Kumar Jha, Bruce H. Krogh, James E. Weimer, Edmund M. Clarke
Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction. HSCC (2007)
Edmund M. Clarke, Himanshu Jain, Daniel Kroening
Verification of SpecC using predicate abstraction. Formal Methods Syst. Des. 30 (1) (2007)
Himanshu Jain, Constantinos Bartzis, Edmund M. Clarke
Satisfiability Checking of Non-clausal Formulas Using General Matings. SAT (2006)
Sagar Chaki, Edmund M. Clarke, Nicholas Kidd, Thomas W. Reps, Tayssir Touili
Verifying Concurrent Message-Passing C Programs with Recursive Calls. TACAS (2006)
Edmund M. Clarke, Muralidhar Talupur, Helmut Veith
Environment Abstraction for Parameterized Verification. VMCAI (2006)

Edmund M. Clarke.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Edmund M. Clarke