Edmund M. Clarke

322 papers A* 64A 29B 21C 15Misc 2Journal 91Unranked 87

Year	Rank	Type	Title / Venue / Authors
2018	—	`book`	Handbook of Model Checking. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem
2018	—	`ch.`	Introduction to Model Checking. Handbook of Model Checking Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith
2018	—	`book`	Model checking, 2nd Edition. Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron A. Peled, Helmut Veith
2017	J	`jnl`	From non-preemptive to preemptive scheduling using synchronization synthesis. Formal Methods Syst. Des. Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach
2016	—	`conf`	Bifurcation Analysis of Cardiac Alternans Using \delta -Decidability. CMSB Md. Ariful Islam, Greg Byrne, Soonho Kong, Edmund M. Clarke, Rance Cleaveland, Flavio H. Fenton, Radu Grosu, Paul L. Jones, Scott A. Smolka
2016	—	`conf`	CyberCardia project: Modeling, verification and validation of implantable cardiac devices. BIBM 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
2016	—	`conf`	Formal Modeling and Analysis of Pancreatic Cancer Microenvironment. CMSB Qinsi Wang, Natasa Miskov-Zivanov, Bing Liu, James R. Faeder, Michael Lotze, Edmund M. Clarke
2016	—	`conf`	Formal modeling of biological systems. HLDVT Qinsi Wang, Edmund M. Clarke
2016	—	`conf`	High-level modeling and verification of cellular signaling. HLDVT Natasa Miskov-Zivanov, Paolo Zuliani, Qinsi Wang, Edmund M. Clarke, James R. Faeder
2016	—	`conf`	Probabilistic reachability analysis of the tap withdrawal circuit in caenorhabditis elegans. HLDVT Md. Ariful Islam, Qinsi Wang, Ramin M. Hasani, Ondrej Balun, Edmund M. Clarke, Radu Grosu, Scott A. Smolka
2016	—	`conf`	SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems. HSCC Kyungmin Bae, Peter Csaba Ölveczky, Soonho Kong, Sicun Gao, Edmund M. Clarke
2016	J	`jnl`	Solving QBF with counterexample guided refinement. Artif. Intell. Mikolás Janota, William Klieber, João Marques-Silva, Edmund M. Clarke
2015	—	`conf`	Formal Analysis Provides Parameters for Guiding Hyperoxidation in Bacteria using Phototoxic Proteins. ACM Great Lakes Symposium on VLSI Qinsi Wang, Natasa Miskov-Zivanov, Cheryl Telmer, Edmund M. Clarke
2015	—	`conf`	From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis. CAV (2) Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach
2015	J	`jnl`	From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis. CoRR Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach
2015	J	`jnl`	Optimizing Solution Quality in Synchronization Synthesis. CoRR Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach
2015	—	`conf`	SReach: A Probabilistic Bounded Delta-Reachability Analyzer for Stochastic Hybrid Systems. CMSB Qinsi Wang, Paolo Zuliani, Soonho Kong, Sicun Gao, Edmund M. Clarke
2015	—	`conf`	Towards personalized prostate cancer therapy using delta-reachability analysis. HSCC Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, Edmund M. Clarke
2015	A	`conf`	dReach: δ-Reachability Analysis for Hybrid Systems. TACAS Soonho Kong, Sicun Gao, Wei Chen, Edmund M. Clarke
2014	—	`conf`	2 Ershov Memorial Conference Edmund M. Clarke, Qinsi Wang
2014	—	`conf`	Compositional, Approximate, and Quantitative Reasoning for Medical Cyber-Physical Systems with Application to Patient-Specific Cardiac Dynamics and Devices. ISoLA (2) 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
2014	J	`jnl`	Delta-Complete Analysis for Bounded Reachability of Hybrid Systems. CoRR Sicun Gao, Soonho Kong, Wei Chen, Edmund M. Clarke
2014	—	`conf`	Model Checking Hybrid Systems - (Invited Talk). ISoLA (2) Edmund M. Clarke, Sicun Gao
2014	J	`jnl`	Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions. CoRR Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, Edmund M. Clarke
2014	—	`conf`	Parameter Synthesis for Cardiac Cell Hybrid Models Using δ-Decisions. CMSB Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, Edmund M. Clarke
2014	J	`jnl`	Pathway-gene identification for pancreatic cancer survival via doubly regularized Cox regression. BMC Syst. Biol. Haijun Gong, Tong Tong Wu, Edmund M. Clarke
2014	Misc	`conf`	Proof Generation from Delta-Decisions. SYNASC Sicun Gao, Soonho Kong, Edmund M. Clarke
2014	J	`jnl`	Proof Generation from Delta-Decisions. CoRR Sicun Gao, Soonho Kong, Edmund M. Clarke
2014	J	`jnl`	Revisiting the Complexity of Stability of Continuous and Hybrid Systems. CoRR Sicun Gao, Soonho Kong, Edmund M. Clarke
2014	J	`jnl`	SReach: Combining Statistical Tests and Bounded Model Checking for Nonlinear Hybrid Systems with Parametric Uncertainty. CoRR Qinsi Wang, Paolo Zuliani, Soonho Kong, Sicun Gao, Edmund M. Clarke
2014	J	`jnl`	Towards Personalized Cancer Therapy Using Delta-Reachability Analysis. CoRR Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, Edmund M. Clarke
2013	A*	`conf`	Automatic Abstraction in SMT-Based Unbounded Software Model Checking. CAV Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke
2013	J	`jnl`	Automatic Abstraction in SMT-Based Unbounded Software Model Checking. CoRR Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke
2013	J	`jnl`	Bayesian statistical model checking with application to Stateflow/Simulink verification. Formal Methods Syst. Des. Paolo Zuliani, André Platzer, Edmund M. Clarke
2013	C	`conf`	Finding Errors in Python Programs Using Dynamic Symbolic Execution. ICTSS Samir Sapra, Marius Minea, Sagar Chaki, Arie Gurfinkel, Edmund M. Clarke
2013	J	`jnl`	Satisfiability Modulo ODEs. CoRR Sicun Gao, Soonho Kong, Edmund M. Clarke
2013	B	`conf`	Satisfiability modulo ODEs. FMCAD Sicun Gao, Soonho Kong, Edmund M. Clarke
2013	A	`conf`	Solving QBF with Free Variables. CP William Klieber, Mikolás Janota, João Marques-Silva, Edmund M. Clarke
2013	—	`conf`	Studies of biological networks with statistical model checking: application to immune system cells. BCB Natasa Miskov-Zivanov, Paolo Zuliani, Edmund M. Clarke, James R. Faeder
2013	A	`conf`	Turing's Computable Real Numbers and Why They Are Still Important Today. SAT Edmund M. Clarke
2013	A	`conf`	dReal: An SMT Solver for Nonlinear Theories over the Reals. CADE Sicun Gao, Soonho Kong, Edmund M. Clarke
2012	J	`jnl`	Assume-Guarantee Abstraction Refinement for Probabilistic Systems CoRR Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke
2012	A*	`conf`	Assume-Guarantee Abstraction Refinement for Probabilistic Systems. CAV Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke
2012	—	`conf`	Assumption Generation for Asynchronous Systems by Abstraction Refinement. FACS Qiusong Yang, Edmund M. Clarke, Anvesh Komuravelli, Mingshu Li
2012	—	`conf`	Computable Real Numbers and Why They Are Still Important Today. ACM-TURING Edmund M. Clarke
2012	J	`jnl`	Delta-Complete Decision Procedures for Satisfiability over the Reals CoRR Sicun Gao, Jeremy Avigad, Edmund M. Clarke
2012	J	`jnl`	Delta-Decidability over the Reals CoRR Sicun Gao, Jeremy Avigad, Edmund M. Clarke
2012	A*	`conf`	Delta-Decidability over the Reals. LICS Sicun Gao, Jeremy Avigad, Edmund M. Clarke
2012	J	`jnl`	Learning Probabilistic Systems from Tree Samples CoRR Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke
2012	A*	`conf`	Learning Probabilistic Systems from Tree Samples. LICS Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke
2012	—	`ed.`	Perspectives of Systems Informatics - 8th International Andrei Ershov Memorial Conference, PSI 2011, Novosibirsk, Russia, June 27-July 1, 2011, Revised Selected Papers Ershov Memorial Conference Edmund M. Clarke, Irina B. Virbitskaite, Andrei Voronkov
2012	—	`conf`	Rare-event verification for stochastic hybrid systems. HSCC Paolo Zuliani, Christel Baier, Edmund M. Clarke
2012	A	`conf`	Solving QBF with Counterexample Guided Refinement. SAT Mikolás Janota, William Klieber, João Marques-Silva, Edmund M. Clarke
2012	—	`conf`	Statistical Model Checking for Markov Decision Processes. QEST David Henriques, João G. Martins, Paolo Zuliani, André Platzer, Edmund M. Clarke
2012	A	`conf`	δ-Complete Decision Procedures for Satisfiability over the Reals. IJCAR Sicun Gao, Jeremy Avigad, Edmund M. Clarke
2011	—	`conf`	Analog circuit verification by statistical model checking. ASP-DAC Ying-Chih Wang, Anvesh Komuravelli, Paolo Zuliani, Edmund M. Clarke
2011	—	`conf`	Formal analysis for logical models of pancreatic cancer. CDC/ECC Haijun Gong, Paolo Zuliani, Qinsi Wang, Edmund M. Clarke
2011	—	`conf`	Model Checking and the State Explosion Problem. LASER Summer School Edmund M. Clarke, William Klieber, Milos Novácek, Paolo Zuliani
2011	J	`jnl`	Quantifier Elimination over Finite Fields Using Gröbner Bases CoRR Sicun Gao, André Platzer, Edmund M. Clarke
2011	—	`conf`	Quantifier Elimination over Finite Fields Using Gröbner Bases. CAI Sicun Gao, André Platzer, Edmund M. Clarke
2011	B	`conf`	Statistical Model Checking for Cyber-Physical Systems. ATVA Edmund M. Clarke, Paolo Zuliani
2010	A	`conf`	A Non-prenex, Non-clausal QBF Solver with Game-State Learning. SAT William Klieber, Samir Sapra, Sicun Gao, Edmund M. Clarke
2010	J	`jnl`	Analysis and verification of the HMGB1 signaling pathway. BMC Bioinform. Haijun Gong, Paolo Zuliani, Anvesh Komuravelli, James R. Faeder, Edmund M. Clarke
2010	A*	`conf`	Automated Assume-Guarantee Reasoning through Implicit Learning. CAV Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang
2010	—	`conf`	Bayesian statistical model checking with application to Simulink/Stateflow verification. HSCC Paolo Zuliani, André Platzer, Edmund M. Clarke
2010	—	`conf`	Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. ISoLA (1) Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, Lei Zhu
2010	—	`conf`	Computational Modeling and Verification of Signaling Pathways in Cancer. ANB Haijun Gong, Paolo Zuliani, Anvesh Komuravelli, James R. Faeder, Edmund M. Clarke
2010	B	`conf`	Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. FMCAD Sicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, Edmund M. Clarke
2010	—	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers LPAR (Dakar) Edmund M. Clarke, Andrei Voronkov
2010	J	`jnl`	On simulation-based probabilistic model checking of mixed-analog circuits. Formal Methods Syst. Des. Edmund M. Clarke, Alexandre Donzé, Axel Legay
2010	—	`conf`	Statistical Verification of Probabilistic Properties with Unbounded Until. SBMF Håkan L. S. Younes, Edmund M. Clarke, Paolo Zuliani
2010	—	`conf`	The Localization Reduction and Counterexample-Guided Abstraction Refinement. Essays in Memory of Amir Pnueli Edmund M. Clarke, Robert P. Kurshan, Helmut Veith
2009	—	`conf`	A Bayesian Approach to Model Checking Biological Systems. CMSB Sumit Kumar Jha, Edmund M. Clarke, Christopher James Langmead, Axel Legay, André Platzer, Paolo Zuliani
2009	J	`jnl`	Computing differential invariants of hybrid systems as fixedpoints. Formal Methods Syst. Des. André Platzer, Edmund M. Clarke
2009	J	`jnl`	Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations. Formal Methods Syst. Des. Himanshu Jain, Edmund M. Clarke, Orna Grumberg
2009	A*	`conf`	Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts. DAC Himanshu Jain, Edmund M. Clarke
2009	B	`conf`	Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. FM André Platzer, Edmund M. Clarke
2009	J	`jnl`	Functional Equivalence Verification Tools in High-Level Synthesis Flows. IEEE Des. Test Comput. Anmol Mathur, Masahiro Fujita, Edmund M. Clarke, Pascal Urard
2009	A	`conf`	Learning Minimal Separating DFA's for Compositional Verification. TACAS Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang
2009	—	`conf`	Model Checking - My 27-year Quest to Overcome the State Explosion Problem. NASA Formal Methods Edmund M. Clarke
2009	J	`jnl`	Model checking: algorithmic verification and debugging. Commun. ACM Edmund M. Clarke, E. Allen Emerson, Joseph Sifakis
2009	A*	`conf`	My 27-year Quest to Overcome the State Explosion Problem. LICS Edmund M. Clarke
2008	A*	`conf`	Computing Differential Invariants of Hybrid Systems as Fixedpoints. CAV André Platzer, Edmund M. Clarke
2008	—	`conf`	Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. 25 Years of Model Checking Edmund M. Clarke, E. Allen Emerson
2008	A*	`conf`	Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. CAV Himanshu Jain, Edmund M. Clarke, Orna Grumberg
2008	A	`conf`	Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. TACAS Azadeh Farzan, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang
2008	B	`conf`	Model Checking - My 27-Year Quest to Overcome the State Explosion Problem. LPAR Edmund M. Clarke
2008	C	`conf`	Model checking in-the-loop: Finding counterexamples by systematic simulation. ACC Flavio Lerda, James Kapinski, Hitashyam Maka, Edmund M. Clarke, Bruce H. Krogh
2008	A	`conf`	Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. TACAS Edmund M. Clarke, Muralidhar Talupur, Helmut Veith
2008	—	`conf`	Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway. CMSB Edmund M. Clarke, James R. Faeder, Christopher James Langmead, Leonard A. Harris, Sumit Kumar Jha, Axel Legay
2008	—	`conf`	Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Delta-Sigma Modulator. Haifa Verification Conference Edmund M. Clarke, Alexandre Donzé, Axel Legay
2008	—	`conf`	The Birth of Model Checking. 25 Years of Model Checking Edmund M. Clarke
2008	—	`conf`	Verification of Supervisory Control Software Using State Proximity and Merging. HSCC Flavio Lerda, James Kapinski, Edmund M. Clarke, Bruce H. Krogh
2008	J	`jnl`	Verification of evolving software via component substitutability analysis. Formal Methods Syst. Des. Sagar Chaki, Edmund M. Clarke, Natasha Sharygina, Nishant Sinha
2008	J	`jnl`	Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
2007	B	`conf`	Arithmetic Strengthening for Shape Analysis. SAS Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook
2007	J	`jnl`	Model Checking: Software and Beyond. J. Univers. Comput. Sci. Edmund M. Clarke, Flavio Lerda
2007	—	`conf`	Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction. HSCC Sumit Kumar Jha, Bruce H. Krogh, James E. Weimer, Edmund M. Clarke
2007	A*	`conf`	SAT-Based Compositional Verification Using Lazy Learning. CAV Nishant Sinha, Edmund M. Clarke
2007	—	`conf`	The Image Computation Problem in Hybrid Systems Model Checking. HSCC André Platzer, Edmund M. Clarke
2007	A	`conf`	VCEGAR: Verilog CounterExample Guided Abstraction Refinement. TACAS Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
2007	J	`jnl`	Verification of SpecC using predicate abstraction. Formal Methods Syst. Des. Edmund M. Clarke, Himanshu Jain, Daniel Kroening
2006	B	`conf`	Environment Abstraction for Parameterized Verification. VMCAI Edmund M. Clarke, Muralidhar Talupur, Helmut Veith
2006	A	`conf`	Ranking Attack Graphs. RAID Vaibhav Mehta, Constantinos Bartzis, Haifeng Zhu, Edmund M. Clarke, Jeannette M. Wing
2006	A	`conf`	Satisfiability Checking of Non-clausal Formulas Using General Matings. SAT Himanshu Jain, Constantinos Bartzis, Edmund M. Clarke
2006	—	`ed.`	Verification of Infinite-State Systems with Applications to Security, Proceedings of the NATO Advanced Research Workshop "Verification of Infinite State Systems with Applications to Security VISSAS 2005", Timisoara, Romania, March 17-22, 2005 VISSAS Edmund M. Clarke, Marius Minea, Ferucio Laurentiu Tiplea
2006	A	`conf`	Verifying Concurrent Message-Passing C Programs with Recursive Calls. TACAS Sagar Chaki, Edmund M. Clarke, Nicholas Kidd, Thomas W. Reps, Tayssir Touili
2005	J	`jnl`	An Iterative Framework for Simulation Conformance. J. Log. Comput. Sagar Chaki, Edmund M. Clarke, Somesh Jha, Helmut Veith
2005	A*	`conf`	Automated Assume-Guarantee Reasoning for Simulation Conformance. CAV Sagar Chaki, Edmund M. Clarke, Nishant Sinha, Prasanna Thati
2005	J	`jnl`	Computational challenges in bounded model checking. Int. J. Softw. Tools Technol. Transf. Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman
2005	J	`jnl`	Concurrent software verification with states, events, and deadlocks. Formal Aspects Comput. Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha
2005	B	`conf`	Dynamic Component Substitutability Analysis. FM Natasha Sharygina, Sagar Chaki, Edmund M. Clarke, Nishant Sinha
2005	—	`conf`	Grand Challenge: Model Check Software. VISSAS Edmund M. Clarke, Himanshu Jain, Nishant Sinha
2005	—	`conf`	Model Checking: Back and Forth between Hardware and Software. VSTTE Edmund M. Clarke, Anubhav Gupta, Himanshu Jain, Helmut Veith
2005	—	`conf`	Program Compatibility Approaches. FMCO Edmund M. Clarke, Natasha Sharygina, Nishant Sinha
2005	C	`conf`	Reconsidering CEGAR: Learning Good Abstractions without Refinement. ICCD Anubhav Gupta, Edmund M. Clarke
2005	—	`conf`	Refining Abstractions of Hybrid Systems Using Counterexample Fragments. HSCC Ansgar Fehnker, Edmund M. Clarke, Sumit Kumar Jha, Bruce H. Krogh
2005	A	`conf`	SATABS: SAT-Based Predicate Abstraction for ANSI-C. TACAS Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav
2005	B	`conf`	State/Event Software Verification for Branching-Time Specifications. IFM Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Joël Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith
2005	—	`ch.`	Temporal Logic Model Checking. Handbook of Networked and Embedded Control Systems Edmund M. Clarke, Ansgar Fehnker, Sumit Kumar Jha, Helmut Veith
2005	A*	`conf`	Word level predicate abstraction and refinement for verifying RTL verilog. DAC Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke
2004	A*	`conf`	A SAT-based algorithm for reparameterization in symbolic simulation. DAC Pankaj Chauhan, Edmund M. Clarke, Daniel Kroening
2004	A	`conf`	A Tool for Checking ANSI-C Programs. TACAS Edmund M. Clarke, Daniel Kroening, Flavio Lerda
2004	C	`conf`	Automated, compositional and iterative deadlock detection. MEMOCODE Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina
2004	A	`conf`	Checking consistency of C and Verilog using predicate abstraction and induction. ICCAD Daniel Kroening, Edmund M. Clarke
2004	B	`conf`	Completeness and Complexity of Bounded Model Checking. VMCAI Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman
2004	C	`conf`	Counterexample Guided Abstraction Refinement Via Program Execution. ICFEM Daniel Kroening, Alex Groce, Edmund M. Clarke
2004	J	`jnl`	Efficient Verification of Sequential and Concurrent C Programs. Formal Methods Syst. Des. Sagar Chaki, Edmund M. Clarke, Alex Groce, Joël Ouaknine, Ofer Strichman, Karen Yorav
2004	J	`jnl`	Modular Verification of Software Components in C. IEEE Trans. Software Eng. Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith
2004	J	`jnl`	Predicate Abstraction of ANSI-C Programs Using SAT. Formal Methods Syst. Des. Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav
2004	J	`jnl`	SAT-based counterexample-guided abstraction refinement. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Edmund M. Clarke, Anubhav Gupta, Ofer Strichman
2004	B	`conf`	State/Event-Based Software Model Checking. IFM Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha
2004	C	`conf`	Tutorial: Software Model Checking. ICFEM Edmund M. Clarke, Daniel Kroening
2004	B	`conf`	Verification by Network Decomposition. CONCUR Edmund M. Clarke, Muralidhar Talupur, Tayssir Touili, Helmut Veith
2004	C	`conf`	Verification of SpecC using predicate abstraction. MEMOCODE Himanshu Jain, Daniel Kroening, Edmund M. Clarke
2003	J	`jnl`	Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems. Int. J. Found. Comput. Sci. Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Joël Ouaknine, Olaf Stursberg, Michael Theobald
2003	—	`conf`	Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach. SoftMC@CAV Sagar Chaki, Joël Ouaknine, Karen Yorav, Edmund M. Clarke
2003	A*	`conf`	Behavioral consistency of C and verilog programs using bounded model checking. DAC Edmund M. Clarke, Daniel Kroening, Karen Yorav
2003	J	`jnl`	Bounded model checking. Adv. Comput. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu
2003	C	`conf`	Counterexample-Guided Abstraction Refinement. TIME Edmund M. Clarke
2003	J	`jnl`	Counterexample-guided abstraction refinement for symbolic model checking. J. ACM Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith
2003	—	`conf`	Counterexamples Revisited: Principles, Algorithms, Applications. Verification: Theory and Practice Edmund M. Clarke, Helmut Veith
2003	J	`jnl`	Efficient verification of security protocols using partial-order reductions. Int. J. Softw. Tools Technol. Transf. Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero
2003	—	`conf`	Hardware verification using ANSI-C programs as a reference. ASP-DAC Edmund M. Clarke, Daniel Kroening
2003	C	`conf`	High Level Verification of Control Intensive Systems Using Predicate Abstraction. MEMOCODE Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang
2003	A*	`conf`	Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. CAV Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang
2003	A	`conf`	Model Checking for Dependable Software-Intensive Systems. DSN Edmund M. Clarke, Masahiro Fujita, David P. Gluch
2003	A*	`conf`	Modular Verification of Software Components in C. ICSE Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith
2003	—	`conf`	Predicate Abstraction with Minimum Predicates. CHARME Sagar Chaki, Edmund M. Clarke, Alex Groce, Ofer Strichman
2003	A	`conf`	SAT Based Predicate Abstraction for Hardware Verification. SAT Edmund M. Clarke, Muralidhar Talupur, Helmut Veith, Dong Wang
2003	C	`conf`	SAT-Based Algorithms for Logic Minimization. ICCD Samir Sapra, Michael Theobald, Edmund M. Clarke
2003	A	`conf`	SAT-Based Counterexample Guided Abstraction Refinement in Model Checking. CADE Edmund M. Clarke
2003	C	`conf`	Specifying and Verifying Systems with Multiple Clocks. ICCD Edmund M. Clarke, Daniel Kroening, Karen Yorav
2003	—	`conf`	VeriAgent: an Approach to Integrating UML and Formal Verification Tools. WMF Edjard Mota, Edmund M. Clarke, Alex Groce, Waleska Oliveira, Marcia Falcão, Jorge Y. Kanda
2003	A	`conf`	Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. TACAS Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Olaf Stursberg, Michael Theobald
2002	B	`conf`	Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis. FMCAD Pankaj Chauhan, Edmund M. Clarke, James H. Kukula, Samir Sapra, Helmut Veith, Dong Wang
2002	A*	`conf`	NuSMV 2: An OpenSource Tool for Symbolic Model Checking. CAV Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella
2002	J	`jnl`	Program slicing for VHDL. Int. J. Softw. Tools Technol. Transf. Edmund M. Clarke, Masahiro Fujita, Sreeranga P. Rajan, Thomas W. Reps, Subash Shankar, Tim Teitelbaum
2002	A*	`conf`	SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. CAV Edmund M. Clarke, Anubhav Gupta, James H. Kukula, Ofer Strichman
2002	—	`conf`	SAT-Based Counterexample Guided Abstraction Refinement. SPIN Edmund M. Clarke
2002	A*	`conf`	Tree-Like Counterexamples in Model Checking. LICS Edmund M. Clarke, Somesh Jha, Yuan Lu, Helmut Veith
2002	J	`jnl`	Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function. Formal Methods Syst. Des. Sergey Berezin, Edmund M. Clarke, Armin Biere, Yunshan Zhu
2001	J	`jnl`	Bounded Model Checking Using Satisfiability Solving. Formal Methods Syst. Des. Edmund M. Clarke, Armin Biere, Richard Raimi, Yunshan Zhu
2001	A*	`conf`	Efficient Filtering in Publish-Subscribe Systems Using Binary Decision. ICSE Alexis Campailla, Sagar Chaki, Edmund M. Clarke, Somesh Jha, Helmut Veith
2001	—	`ch.`	Model Checking. Handbook of Automated Reasoning Edmund M. Clarke, Bernd-Holger Schlingloff
2001	—	`book`	Model checking, 1st Edition. Edmund M. Clarke, Orna Grumberg, Doron A. Peled
2001	A	`conf`	Non-linear Quantification Scheduling in Image Computation. ICCAD Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, James H. Kukula, Thomas R. Shiple, Helmut Veith, Dong Wang
2001	Misc	`conf`	Progress on the State Explosion Problem in Model Checking. Informatics Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith
2001	J	`jnl`	The Verus language: representing time efficiently with BDDs. Theor. Comput. Sci. Sérgio Vale Aguiar Campos, Edmund M. Clarke
2001	—	`conf`	Using Combinatorial Optimization Methods for Quantification Scheduling. CHARME Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, James H. Kukula, Helmut Veith, Dong Wang
2001	—	`conf`	Using cutwidth to improve symbolic simulation and Boolean satisfiability. HLDVT Dong Wang, Edmund M. Clarke, Yunshan Zhu, James H. Kukula
2000	B	`conf`	A Theory of Consistency for Modular Synchronous Systems. FMCAD Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel
2000	J	`jnl`	Automatic verification of hardware and software systems. ACM SIGSOFT Softw. Eng. Notes Edmund M. Clarke
2000	A*	`conf`	Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. CAV Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta
2000	A*	`conf`	Counterexample-Guided Abstraction Refinement. CAV Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith
2000	A*	`conf`	Efficient variable ordering using aBDD based sampling. DAC Yuan Lu, Jawahar Jain, Edmund M. Clarke, Masahiro Fujita
2000	B	`conf`	Executable Protocol Specification in ESL. FMCAD Edmund M. Clarke, Steven M. German, Yuan Lu, Helmut Veith, Dong Wang
2000	—	`conf`	Model checking algorithms for the µ-calculus. Proof, Language, and Interaction Sergey Berezin, Edmund M. Clarke, Somesh Jha, Will Marrero
2000	J	`jnl`	NUSMV: A New Symbolic Model Checker. Int. J. Softw. Tools Technol. Transf. Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri
2000	A	`conf`	Partial Order Reductions for Security Protocol Verification. TACAS Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero
2000	J	`jnl`	Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System. Formal Methods Syst. Des. Sérgio Vale Aguiar Campos, Edmund M. Clarke, Orna Grumberg
2000	J	`jnl`	Verification of a safety-critical railway interlocking system with real-time constraints. Sci. Comput. Program. Vicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia
2000	J	`jnl`	Verifying security protocols with Brutus. ACM Trans. Softw. Eng. Methodol. Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero
1999	—	`conf`	Abstract BDDs: A Technique for Using Abstraction in Model Checking. CHARME Edmund M. Clarke, Somesh Jha, Yuan Lu, Dong Wang
1999	J	`jnl`	Analysis and Verification of Real-Time Systems Using Quantitative Symbolic Algorithms. Int. J. Softw. Tools Technol. Transf. Sérgio Vale Aguiar Campos, Edmund M. Clarke
1999	—	`conf`	Combining Local and Global Model Checking. SMC@FLoC Armin Biere, Edmund M. Clarke, Yunshan Zhu
1999	—	`conf`	Model Checking Semi-Continuous Time Models Using BDDs. SMC@FLoC Sérgio Vale Aguiar Campos, Marcio Teixeira, Marius Minea, Andreas Kuehlmann, Edmund M. Clarke
1999	—	`conf`	Multiple State and Single State Tableaux for Combining Local and Global Model Checking. Correct System Design Armin Biere, Edmund M. Clarke, Yunshan Zhu
1999	A*	`conf`	NUSMV: A New Symbolic Model Verifier. CAV Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri
1999	—	`conf`	ProbVerus: Probabilistic Symbolic Model Checking. ARTS Vicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Edmund M. Clarke
1999	—	`conf`	Program Slicing of Hardware Description Languages. CHARME Edmund M. Clarke, Masahiro Fujita, Sreeranga P. Rajan, Thomas W. Reps, Subash Shankar, Tim Teitelbaum
1999	J	`jnl`	State Space Reduction Using Partial Order Techniques. Int. J. Softw. Tools Technol. Transf. Edmund M. Clarke, Orna Grumberg, Marius Minea, Doron A. Peled
1999	A*	`conf`	Symbolic Model Checking Using SAT Procedures instead of BDDs. DAC Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Masahiro Fujita, Yunshan Zhu
1999	A	`conf`	Symbolic Model Checking without BDDs. TACAS Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu
1999	A*	`conf`	Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. CAV Armin Biere, Edmund M. Clarke, Richard Raimi, Yunshan Zhu
1999	J	`jnl`	Verifying the SRT Division Algorithm Using Theorem Proving Techniques. Formal Methods Syst. Des. Edmund M. Clarke, Steven M. German, Xudong Zhao
1998	J	`jnl`	Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation. J. Autom. Reason. Andrej Bauer, Edmund M. Clarke, Xudong Zhao
1998	B	`conf`	Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. FMCAD Sergey Berezin, Armin Biere, Edmund M. Clarke, Yunshan Zhu
1998	—	`conf`	Formal Verification of VHDL ¾ The Model Checker CV. SBCCI David Déharbe, Subash Shankar, Edmund M. Clarke
1998	B	`conf`	Model Checking VHDL with CV. FMCAD David Déharbe, Subash Shankar, Edmund M. Clarke
1998	B	`conf`	Model Checking: Historical Perspective and Example (Extended Abstract). TABLEAUX Edmund M. Clarke, Sergey Berezin
1998	—	`conf`	On the Semantic Foundations of Probabilistic Synchronous Reactive Programs. PROBMIV Christel Baier, Edmund M. Clarke, Vasiliki Hartonas-Garmhausen
1998	A*	`conf`	Symmetry Reductions in Model Checking. CAV Edmund M. Clarke, E. Allen Emerson, Somesh Jha, A. Prasad Sistla
1998	—	`conf`	Using state space exploration and a natural deduction style message derivation engine to verify security protocols. PROCOMET Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero
1998	—	`conf`	Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints. FTCS Vicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia
1997	J	`jnl`	An Improved Algorithm for the Evaluation of Fixpoint Expressions. Theor. Comput. Sci. Anca Browne, Edmund M. Clarke, Somesh Jha, David E. Long, Wilfredo R. Marrero
1997	J	`jnl`	Another Look at LTL Model Checking. Formal Methods Syst. Des. Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi
1997	—	`conf`	Compositional Reasoning in Model Checking. COMPOS Sergey Berezin, Sérgio Vale Aguiar Campos, Edmund M. Clarke
1997	J	`jnl`	Editorial. Formal Methods Syst. Des. Edmund M. Clarke
1997	C	`conf`	Equivalence Checking Using Abstract BDDs. ICCD Somesh Jha, Yuan Lu, Marius Minea, Edmund M. Clarke
1997	—	`conf`	Model Cheking. FSTTCS Edmund M. Clarke
1997	J	`jnl`	Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. Formal Methods Syst. Des. Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, Jerry Chih-Yuan Yang
1997	A*	`conf`	Symbolic Model Checking for Probabilistic Processes. ICALP Christel Baier, Edmund M. Clarke, Vasiliki Hartonas-Garmhausen, Marta Z. Kwiatkowska, Mark Ryan
1997	J	`jnl`	Symbolic Techniques for Formally Verifying Industrial Systems. Sci. Comput. Program. Sérgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea
1997	—	`conf`	Temporal Logic Model Checking (Abstract). ILPS Edmund M. Clarke
1997	—	`conf`	The Verus Language: Representing Time Efficiently with BDDs. ARTS Sérgio Vale Aguiar Campos, Edmund M. Clarke
1997	A*	`conf`	The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems. CAV Sérgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea
1997	J	`jnl`	Verifying Parameterized Networks. ACM Trans. Program. Lang. Syst. Edmund M. Clarke, Orna Grumberg, Somesh Jha
1996	—	`conf`	Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation. AISMC Andrej Bauer, Edmund M. Clarke, Xudong Zhao
1996	A*	`conf`	Deadlock prevention in flexible manufacturing systems using symbolic model checking. ICRA Vasiliki Hartonas-Garmhausen, Edmund M. Clarke, S. Campos
1996	J	`jnl`	Exploiting Symmetry in Temporal Logic Model Checking. Formal Methods Syst. Des. Edmund M. Clarke, Somesh Jha, Reinhard Enders, Thomas Filkorn
1996	J	`jnl`	Formal Methods: State of the Art and Future Directions. ACM Comput. Surv. Edmund M. Clarke, Jeannette M. Wing
1996	—	`conf`	Model checking. NATO ASI DPD Edmund M. Clarke, Orna Grumberg, David E. Long
1996	A*	`conf`	Symbolic Model Checking. CAV Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, Vasiliki Hartonas-Garmhausen
1996	J	`jnl`	Tools and Partial Analysis. ACM Comput. Surv. Edmund M. Clarke, Jeannette M. Wing
1996	B	`conf`	Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking. FMCAD Yirng-An Chen, Edmund M. Clarke, Pei-Hsin Ho, Yatin Vasant Hoskote, Timothy Kam, Manpreet Khaira, John W. O'Leary, Xudong Zhao
1996	A*	`conf`	Verifying the SRT Division Algorithm Using Theorem Proving Techniques. CAV Edmund M. Clarke, Steven M. German, Xudong Zhao
1996	B	`conf`	Word Level Model Checking (Abstract). MFCS Edmund M. Clarke, Xudong Zhao
1996	A*	`conf`	Word Level Model Checking - Avoiding the Pentium FDIV Error. DAC Edmund M. Clarke, Manpreet Khaira, Xudong Zhao
1995	—	`conf`	Automatic verification of industrial designs. WIFT Vicky Hartonas-Garmhausen, Thomas R. Kurfess, Edmund M. Clarke, David E. Long
1995	A*	`conf`	Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. DAC Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao
1995	A	`conf`	Hybrid decision diagrams. ICCAD Edmund M. Clarke, Masahiro Fujita, Xudong Zhao
1995	—	`ch.`	Symmetry and Induction in Model Checking. Computer Science Today Edmund M. Clarke, Somesh Jha
1995	J	`jnl`	Temporal Verification of Real-Time Systems. IEICE Trans. Inf. Syst. Sérgio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, Marius Minea, Hiromi Hiraishi
1995	—	`conf`	Timing analysis of industrial real-time systems. WIFT Sérgio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, Marius Minea
1995	J	`jnl`	Verification of the Futurebus+ Cache Coherence Protocol. Formal Methods Syst. Des. Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness
1995	C	`conf`	Verifying the performance of the PCI local bus using symbolic techniques. ICCD Sérgio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, Marius Minea
1995	—	`conf`	Verus: A Tool for Quantitative Analysis of Finite-State Real-Time Systems. Workshop on Languages, Compilers, & Tools for Real-Time Systems Sérgio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, Marius Minea
1995	B	`conf`	Veryfying Parameterized Networks using Abstraction and Regular Languages. CONCUR Edmund M. Clarke, Orna Grumberg, Somesh Jha
1994	A*	`conf`	An Improved Algorithm for the Evaluation of Fixpoint Expressions. CAV David E. Long, Anca Browne, Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero
1994	A*	`conf`	Another Look at LTL Model Checking. CAV Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi
1994	A*	`conf`	Automatic Verification of Finite-State Concurrent Systems LICS Edmund M. Clarke
1994	—	`conf`	Automatic Verification of Finite-state Concurrent Systems. Application and Theory of Petri Nets Edmund M. Clarke
1994	A	`conf`	Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan. CADE Edmund M. Clarke, Xudong Zhao
1994	A	`conf`	Computing Quantitative Characteristics of Finite-State Real-Time Systems. RTSS Sérgio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, Marius Minea, Hiromi Hiraishi
1994	C	`conf`	Fast Spectrum Computation for Logic Functions using Binary Decision Diagrams. ISCAS Masahiro Fujita, Jerry Chih-Yuan Yang, Edmund M. Clarke, Xudong Zhao, Patrick C. McGeer
1994	J	`jnl`	Model Checking and Abstraction. ACM Trans. Program. Lang. Syst. Edmund M. Clarke, Orna Grumberg, David E. Long
1994	J	`jnl`	Symbolic model checking for sequential circuit verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, David L. Dill
1993	J	`jnl`	A Unified Approch for Showing Language Inclusion and Equivalence Between Various Types of omega-Automata. Inf. Process. Lett. Edmund M. Clarke, I. A. Draghicescu, Robert P. Kurshan
1993	—	`conf`	Automatic Verification of Sequential Circuit Designs. CHDL Edmund M. Clarke
1993	A*	`conf`	Efficient Verification of Parallel Real-Time Systems. CAV Tomohiro Yoneda, Atsufumi Shibayama, Bernd-Holger Schlingloff, Edmund M. Clarke
1993	A*	`conf`	Exploiting Symmetry In Temporal Logic Model Checking. CAV Edmund M. Clarke, Thomas Filkorn, Somesh Jha
1993	J	`jnl`	New and used temporal models: An issue of time. Appl. Intell. Frank D. Anger, Edmund M. Clarke
1993	A*	`conf`	Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. DAC Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, Jerry Chih-Yuan Yang
1993	—	`conf`	Verification Tools for Finite-State Concurrent Systems. REX School/Symposium Edmund M. Clarke, Orna Grumberg, David E. Long
1993	—	`conf`	Verification of the Futurebus+ Cache Coherence Protocol. CHDL Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness
1992	J	`jnl`	A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems. J. Log. Comput. Edmund M. Clarke, Orna Grumberg, Robert P. Kurshan
1992	A	`conf`	Analytica - A Theorem Prover in Mathematica. CADE Edmund M. Clarke, Xudong Zhao
1992	A*	`conf`	Model Checking and Abstraction. POPL Edmund M. Clarke, Orna Grumberg, David E. Long
1992	J	`jnl`	PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. J. Autom. Reason. Soumitra Bose, Edmund M. Clarke, David E. Long, Spiro Michaylov
1992	J	`jnl`	Symbolic Model Checking: 10^20 States and Beyond Inf. Comput. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang
1991	J	`jnl`	A language for compositional specification and verification of finite state hardware controllers. Proc. IEEE Edmund M. Clarke, David E. Long, Kenneth L. McMillan
1991	A*	`ed.`	Computer Aided Verification, 2nd International Workshop, CAV '90, New Brunswick, NJ, USA, June 18-21, 1990, Proceedings CAV Edmund M. Clarke, Robert P. Kurshan
1991	—	`ed.`	Computer-Aided Verification, Proceedings of a DIMACS Workshop 1990, New Brunswick, New Jersey, USA, June 18-21, 1990 CAV (DIMACS/AMS volume) Edmund M. Clarke, Robert P. Kurshan
1991	A*	`conf`	Representing Circuits More Efficiently in Symbolic Model Checking. DAC Jerry R. Burch, Edmund M. Clarke, David E. Long
1991	—	`conf`	Symbolic Model Checking with Partitioned Transistion Relations. VLSI Jerry R. Burch, Edmund M. Clarke, David E. Long
1990	—	`conf`	A Unified Approach For Showing Language Containment And Equivalence Between Various Types Of Omega-Automata. CAAP Edmund M. Clarke, Anca Browne, Robert P. Kurshan
1990	C	`conf`	A parallel algorithm for constructing binary decision diagrams. ICCD Shinji Kimura, Edmund M. Clarke
1990	—	`conf`	Preface. CAV (DIMACS/AMS volume) Edmund M. Clarke, Robert P. Kurshan
1990	A*	`conf`	Sequential Circuit Verification Using Symbolic Model Checking. DAC Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill
1990	A*	`conf`	Symbolic Model Checking: 10^20 States and Beyond LICS Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang
1990	A*	`conf`	Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem. CAV Edmund M. Clarke
1990	—	`conf`	Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem. CAV (DIMACS/AMS volume) Edmund M. Clarke
1989	—	`conf`	A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems. Logic at Botik Edmund M. Clarke, Orna Grumberg, Robert P. Kurshan
1989	A*	`conf`	Compositional Model Checking LICS Edmund M. Clarke, David E. Long, Kenneth L. McMillan
1989	A*	`conf`	PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses LICS Soumitra Bose, Edmund M. Clarke, David E. Long, Spiro Michaylov
1989	J	`jnl`	Reasoning about Networks with Many Identical Finite State Processes Inf. Comput. Michael C. Browne, Edmund M. Clarke, Orna Grumberg
1989	J	`jnl`	Reasoning about Procedures as Parameters in the Language L4 Inf. Comput. Steven M. German, Edmund M. Clarke, Joseph Y. Halpern
1988	J	`jnl`	Characterizing Finite Kripke Structures in Propositional Temporal Logic. Theor. Comput. Sci. Michael C. Browne, Edmund M. Clarke, Orna Grumberg
1988	J	`jnl`	Escher-a geometrical layout system for recursively defined circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Edmund M. Clarke, Yulin Feng
1988	—	`conf`	Expressibility results for linear-time and branching-time logics. REX Workshop Edmund M. Clarke, I. A. Draghicescu
1988	A	`conf`	PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. CADE P. E. Allen, Soumitra Bose, Edmund M. Clarke, Spiro Michaylov
1987	A*	`conf`	Avoiding The State Explosion Problem in Temporal Logic Model Checking. PODC Edmund M. Clarke, Orna Grumberg
1987	—	`conf`	Characterizing Kripke Structures in Temporal Logic. TAPSOFT, Vol.1 Michael C. Browne, Edmund M. Clarke, Orna Grumberg
1987	—	`conf`	The Model Checking Problem for Concurrent Systems with Many Similar Processes. Temporal Logic in Specification Edmund M. Clarke, Orna Grumberg
1986	J	`jnl`	Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Program. Lang. Syst. Edmund M. Clarke, E. Allen Emerson, A. Prasad Sistla
1986	J	`jnl`	Automatic Verification of Sequential Circuits Using Temporal Logic. IEEE Trans. Computers Michael C. Browne, Edmund M. Clarke, David L. Dill, Bud Mishra
1986	J	`jnl`	Compiling Path Expressions Into VLSI Circuits. Distributed Comput. Thomas S. Anantharaman, Edmund M. Clarke, Michael J. Foster, Bud Mishra
1986	J	`jnl`	Distributed Computing Issues in Hardware Design. Distributed Comput. Edmund M. Clarke
1986	A*	`conf`	Escher - a geometrical layout system for recursively defined circuits. DAC Edmund M. Clarke, Yulin Feng
1986	A*	`conf`	Reasoning About Networks With Many Identical Finite-State Processes. PODC Edmund M. Clarke, Orna Grumberg, Michael C. Browne
1986	A*	`conf`	True Relative Completeness of an Axiom System for the Language L4 (Abridged) LICS Steven M. German, Edmund M. Clarke, Joseph Y. Halpern
1985	A*	`conf`	Compiling Path Expressions into VLSI Circuits. POPL Thomas S. Anantharaman, Edmund M. Clarke, Michael J. Foster, Bud Mishra
1985	J	`jnl`	Hierarchical Verification of Asynchronous Circuits Using Temporal Logic. Theor. Comput. Sci. Bhubaneswaru Mishra, Edmund M. Clarke
1985	J	`jnl`	The Complexity of Propositional Linear Temporal Logics J. ACM A. Prasad Sistla, Edmund M. Clarke
1984	J	`jnl`	Can Message Buffers Be Axiomatized in Linear Temporal Logic? Inf. Control. A. Prasad Sistla, Edmund M. Clarke, Nissim Francez, Albert R. Meyer
1984	—	`ed.`	Logics of Programs, Workshop, Carnegie Mellon University, Pittsburgh, PA, USA, June 6-8, 1983, Proceedings Logics of Programs Edmund M. Clarke, Dexter Kozen
1984	—	`conf`	Using Temporal Logic for Automatic Verification of Finite State Systems. Logics and Models of Concurrent Systems Edmund M. Clarke, Michael C. Browne, E. Allen Emerson, A. Prasad Sistla
1983	A*	`conf`	A methodology for verifying request processing protocols. SIGCOMM Christos Nikolaou, Edmund M. Clarke, Nissim Francez, Stephen A. Schuman
1983	—	`conf`	Automatic Verification of Asynchronous Circuits. Logic of Programs Edmund M. Clarke, Bud Mishra
1983	A*	`conf`	Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. POPL Edmund M. Clarke, E. Allen Emerson, A. Prasad Sistla
1983	J	`jnl`	Effective Axiomatizations of Hoare Logics J. ACM Edmund M. Clarke, Steven M. German, Joseph Y. Halpern
1983	—	`conf`	Reasoning About Procedures as Parameters. Logic of Programs Steven M. German, Edmund M. Clarke, Joseph Y. Halpern
1982	A*	`conf`	Can Message Buffers be Characterized in Linear Temporal Logic? PODC A. Prasad Sistla, Edmund M. Clarke, Nissim Francez, Yuri Gurevich
1982	J	`jnl`	Distributed Reconfiguration Strategies for Fault-Tolerant Multiprocessor Systems. IEEE Trans. Computers Edmund M. Clarke, Christos Nikolaou
1982	A*	`conf`	On Effective Axiomatizations of Hoare Logics. POPL Edmund M. Clarke, Steven M. German, Joseph Y. Halpern
1982	A*	`conf`	The Complexity of Propositional Linear Temporal Logics STOC A. Prasad Sistla, Edmund M. Clarke
1982	J	`jnl`	Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Sci. Comput. Program. E. Allen Emerson, Edmund M. Clarke
1981	—	`conf`	Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logic of Programs Edmund M. Clarke, E. Allen Emerson
1981	J	`jnl`	Task Management in Ada-A Critical Evaluation for Real-time Multiprocessors. Softw. Pract. Exp. Eric S. Roberts, Arthur Evans Jr., C. Robert Morgan, Edmund M. Clarke
1980	A*	`conf`	Characterizing Correctness Properties of Parallel Programs Using Fixpoints. ICALP E. Allen Emerson, Edmund M. Clarke
1980	A*	`conf`	Fast Maintenance of Semantic Integrity Assertions Using Redundant Aggregate Data. VLDB Philip A. Bernstein, Barbara T. Blaustein, Edmund M. Clarke
1980	J	`jnl`	Proving Correctness of Coroutines Without History Variables. Acta Informatica Edmund M. Clarke
1980	J	`jnl`	Synthesis of Resource Invariants for Concurrent Programs. ACM Trans. Program. Lang. Syst. Edmund M. Clarke
1979	A*	`conf`	Approximate Algorithms for Optimization of Busy Waiting in Parallel Programs (Preliminary Report) FOCS Edmund M. Clarke, Lishing Liu
1979	J	`jnl`	Program invariants as fixedpoints. Computing Edmund M. Clarke
1979	J	`jnl`	Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems. J. ACM Edmund M. Clarke
1979	A*	`conf`	Synthesis of Resource Invariants for Concurrent Programs. POPL Edmund M. Clarke
1978	—	`conf`	Proving the correctness of coroutines without history variables. ACM-SE Edmund M. Clarke
1977	A*	`conf`	Program Invariants as Fixed Points (Preliminary Reports) FOCS Edmund M. Clarke
1977	A*	`conf`	Programming Language Constructs for Which it is Impossible to Obtain "Good" Hoare-Like Axiom Systems. POPL Edmund M. Clarke
1976	—	`—`	Completeness and Incompleteness Theorems for Hoare-like Axiom Systems. Edmund M. Clarke